Notes 0407 #22
Notes 0407 #22
Conversation
|
|
||
| Nevertheless, there are two differences between the two operators. | ||
| First, the underlying type of a face may change along coercion, but it is not the case for homogeneous composition (as already remarked in Sect.~\ref{HomogeneousComposition}). | ||
| Oh the other hand, we may specify faces other than a cap of a box for homogeneous composition (see Sect.~\ref{HomogeneousComposition}), but it is not the case for coercion. |
| \hypo{\oftype{M}{\dfuntype{x}{A}{B}}} | ||
| \hypo{\oftype{r}{\mathbb{I}}} | ||
| \infer2{\eqterm{\mathtt{transp}^i\,\parens{\dfuntype{x}{A}{B}}\,r\,M} | ||
| {\lam{x}[A]{\mathtt{transp}^i\,B[x \mapsto \text{\texttt{transp-fill}}^{\texttildelow i}\,A\,r\,x]\,r\,\parens{\app{M}{\parens{\text{\texttt{transp-fill}}^1\,A\,r\,x}}}}} |
There was a problem hiding this comment.
The second transp-fill^1 should be the reversed transp.
|
|
||
| \subsection{Positive Types} | ||
|
|
||
| Coercion simply ``just works'' for inductive types: |
There was a problem hiding this comment.
Technically, this would not work for List(A) or A+B. You need to push the coercion inside the constructors.
| \infer2{\eqterm{\mathtt{transp}^i\,A\,\varphi\,M}{M}{A}} | ||
| \end{prooftree*} | ||
|
|
||
| Homogeneous composition, on the other hand, requires a bit of a trick; since $N$ might not be constant (i.e., $N[i\mapsto0]\equiv N[i\mapsto1]$ might not hold). Here, $\mathtt{hcomp}$ adds additional values to the type; since type declarations only define an inductive type that's generated by a certain description, this is acceptable. Furthermore, the new values commute with elimination, which makes these new values aren't really ``stuck terms.'' |
There was a problem hiding this comment.
The reason is not because N is not constant (it is constant). The reason is that even if there is a path between two elements of N under some context, they are not provably judgmentally equal in our setting.
|
|
||
| %To make homogeneous composition useful in type theory, we extend it to boxes with multiple missing faces. | ||
| Let us remark that as long as the cap of a box is present we can apply homogeneous composition to the box \emph{even if the other faces are absent}. | ||
| Also, to apply homogeneous composition, the faces of a box must share the \emph{same} type; this point explains the terminology \emph{homogeneous} composition. |
There was a problem hiding this comment.
The faces might still have different types. The composition is homogeneous because the type is not changing along the composition dimension, but it can still be changing in other dimensions.
|
|
||
| Because of the unit type's simple structure, nothing particularly interesting can happen here. | ||
|
|
||
| \subsection{Empty} |
There was a problem hiding this comment.
Did you mean the unit type or the empty type? BTW, the empty type should be done in the same way as other inductively defined types.
|
Overall the note looks good. Please see the above comments! :-) |
No description provided.