How to implement the type checking of `transp` in de Morgan cubical type theory?

Question

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.

Answer 1

For example, if $i∧j∨k∧(¬l)=1$, then what? What should I do to $A$?

As Trebor said, for $ i_1 ∧ i_2 ∧ … ∧ i_n = 1 $ we should perform n substitutions and check that $ A(i_1/1, i_2/1, …, i_n/1) = A(i_1/1, i_2/1, …, i_n/1, i/0) $. Further, each $ i ∨ j = 1 $ splits into two cases: $ i = 1 $ and $ j = 1 $; and for $ ¬i = 1 $ you should check $ i = 0 $.

But for cases like $ (i ∨ j) ∧ k = 1 $ it is tricky in general to do some checks directly this way, so in cubicaltt formulas are first converted by invFormula (weird name) to DNF stored as list of maps (each map represents conjunction in the form $ (i_1 = j_1) ∧ (i_2 = j_2) ∧ … ∧ (i_n = j_n) $, where $i_k$ are some variables and $ j_k ∈ \{0,1\} $). Then checker simply iterates over these maps simultaneously replacing each $i_k$ with $j_k$ and checking required condition. But notice that unlike Cubical Agda dimension variables in cubicaltt are special kind of syntax, so there can be no face like $(w.1 = 0)$ for some $w : \mathbb{I} × \mathbb{I}$ at all.

Cubical Agda works about the same: equalTermOnFace calls compareTermOnFace, compareTermOnFace calls compareTermOnFace', compareTermOnFace' calls forallFaceMaps, forallFaceMaps checks some conditions for each conjunct obtained from decomposeInterval (which seems) analogous to invFormula in cubicaltt, only with the difference that it is necessary to handle faces like $(w.1 = 0)$.

In A CUBICAL TYPE THEORY FOR HIGHER INDUCTIVE TYPES, they wrote $Γ,i:I,ψ⊢A=A(i/0)$. Does this imply $Γ,ψ⊢A(i/0)=A(i/1)$?

We have $A = A(i/0)$ for each $i : I$, so isn’t it obvious that then $A(i/1) = (A(i/0))(i/1) = A(i/0)$? Also notice that converse doesn’t hold.

Also, how to implement $Γ,ψ⊢a=b$ for any term $a,b$ in general?

Obviously, described things can be generalized from $A = A(i/0)$ to arbitrary $a = b$.