This repository has been archived by the owner on Oct 24, 2021. It is now read-only.
Added notes for April 14th #21
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
favonia
reviewed
Apr 27, 2020
| For some $A : \U$ and constraint $\phi$, then: $$ \coerce^i \; \U \; \phi \; A \equiv A $$ | ||
| This means that we can just do nothing, similar to how we handled coercion for inductive types. | ||
|
|
||
| The other two issues are more involved and require the introduction of the '\texttt{Glue}' types. \texttt{Glue} types are similar to other compositions, except that the walls are eqivalences instead of paths. The \texttt{Glue} type for some $A : \U$ and $\phi \vdash E : T \simeq A$ is written as: $$ \Glue \; [\phi \mapsto (T, E)] \; A$$ This can also be thought of as using univalence to get a path from the equivalence $E$ and then composing a new type using that path as the walls in the composition. |
There was a problem hiding this comment.
In LaTeX, single quotes should be like `this'.
|
The notes are great. I appreciate the drawing. My only suggestion is to make the picture float or move it before the paragraph so that people know what (1), (2), and (3) refer to. It might also be great to partition those long paragraphs describing the algorithms into smaller ones. |
favonia
reviewed
May 5, 2020
| \newpage | ||
|
|
||
| \section{Composition of Glue Types} | ||
| We will also need to define the Kan operators for the \texttt{Glue} types. For the homogeneous composition we can construct a 3-cube where the top face has the first \texttt{Glue} type on the front edge (M) and the second \texttt{Glue} type as the left wall (N). This means that the corresponding edges on the bottom face will have the total elements retrieved by applying the eliminator on the two \texttt{Glue} types. To get the result of the homogeneous composition, we need to call hfill on M (1). This will give a line that we can use for the right wall of the top face. By applying \texttt{unglue} to this result, we can get the entire right face (2), at which point we have enough information to perform homogeneous composition on the bottom face of the cube (3). This will give us a \texttt{Glue} type in the back face, since we have the two points on top as well as the bottom edge. |
There was a problem hiding this comment.
This is the one of the longer paragraphs. The picture can be made floating or put before this paragraph.
favonia
reviewed
May 5, 2020
| \end{prooftree*} | ||
| This means that if we have a type $A : \U$ and this type is equivalent to the partial type $T$ under the constraint $\phi$, we can construct a \texttt{Glue} type that is judgementally equal to the type $T$ under the constraint $\phi$. \\ | ||
|
|
||
| The introduction rule defines the only constructor for the \texttt{Glue} type called '\texttt{glue}'. It is as follows: |
favonia
reviewed
May 5, 2020
| \end{prooftree*} | ||
| This rule takes two arguments: an element of the partial type $T$ and a total element of the type $A$ which agrees with the image of $t$ judgementally. \\ | ||
|
|
||
| The eliminator for a \texttt{Glue} type is called '\texttt{unglue}' and returns the base type that is equivalent to the partial element. More formally: |
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Notes by Jack and Dawn for lecture on April 14th