10
$\begingroup$

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:

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.
$\endgroup$
1
  • $\begingroup$ Naïvely this should work: If $\neg i = 1$, then substitute $i \mapsto 0$; if $i \vee j = 1$, then substitute $i \mapsto 1$ and $j \mapsto 1$ simultaneously; if $i \wedge j = 1$, then split into two cases where $i = 1$ and $j = 1$, respectively. $\endgroup$
    – Trebor
    Apr 13 at 5:11

1 Answer 1

4
$\begingroup$

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$.

$\endgroup$
1
  • $\begingroup$ Thanks very much! I'm very happy to hear that cubicaltt uses NDF because I'm also experimenting with DNF... $\endgroup$
    – ice1000
    Apr 25 at 14:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.