I am reading many referential materials and I want to find a proper way to implement it. Suppose the syntax is ${\sf transp}~A~\psi:A~0\to A~1$, where (let's call it "the condition") $A:\mathbb I \to \mathcal U$ is constant when $\psi=1$. I am looking for a criterion to check "the condition". For example, if $i\land j\lor k \land (\neg l)=1$, then what? What should I do to $A$? My guesses are as follows:
- I understand how to deal with the simplest case, where $\psi$ is a constant or just a variable. Those cases are obvious.
- If $\psi=i\land j$, I guess this will decompose "the condition" into the problems "when $i=1$, is $A$ constant?" and "$j=1$, is $A$ constant?", am I right?
- If $\psi=\neg i$, this is probably the same as $\psi=i$, but I'm also unsure.
- What to do when $\psi=i \lor j$?
I have checked some papers:
- In Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types, the rules for type checking are omitted, and is discussed informally.
- In A CUBICAL TYPE THEORY FOR HIGHER INDUCTIVE TYPES, they wrote $\Gamma,i:\mathbb I,\psi \vdash A=A(i/0)$. Does this imply $\Gamma,\psi\vdash A(i/0)=A(i/1)$? Also, how to implement $\Gamma,\psi\vdash a=b$ for any term $a, b$ in general?
- In On Higher Inductive Types in Cubical Type Theory, "the condition" is described as $\psi\Rightarrow \forall(i:\mathbb I)A(0)=A(i)$ (I paraphrased the notation for consistency), and that essentially leads me to the same confusion as for hcomp.pdf.
Answers I'm expecting:
- Pointers to particular sections/page number of papers. I may miss some information while reading these papers.
- A few sentences like 'you traverse the syntax tree of $\psi$, and in case of this you substitute this to this and in case of that you substitute this to this, and then perform a MLTT conversion check between this and this'. This would greatly help me.
- Links to specific functions in implemented de Morgan cubical type theory. Existing codebases are large, and it's very easy to get lost.