In (CHM/CCHM) cubical type theory, how to conversion-check face formulae?

Question

In my impression (also according to Amelia in her discord server), some non-syntactically equal face formulae should be definitionally-equal (denoted $\equiv$):

• $(a = 1 \land b = 1) \equiv (b = 1 \land a = 1)$
• $(a = 1 \land (b = 1 \lor c = 1)) \equiv ((c = 1\lor b = 1) \land a = 1)$

(Are face formulae cofibrations? I see people define a face formula as a sequence of conjunction of cofibrations (which are pure disjunctions) like in ABCFHL, but I also see people exemplifying a cofibration with things like $a = 1 \lor b = 1 \land c = 1$, which is very confusing)

I'm wondering what's the general rule of checking the (complete) definitional equality of cofibrations? My conjecture for now is very similar to "propositional extensionality":

$$ \cfrac{\Gamma,\phi\vdash \psi\text{ holds} \quad \Gamma,\psi\vdash \phi\text{ holds}}{\Gamma\vdash \phi\equiv\psi} $$

Am I right? Is it complete? Am I understanding face formulae correctly?

Answer 1

CHM/CCHM face formulae are indeed the same thing as cofibrations in the ABCFHL terminology.

Whether cofibrations support propositional extensionality, is up to design choice. ABCFHL says that "propositional univalence" for cofibrations, which means that inter-provable cofibrations are definitionally equal, is necessary for supporting the Martin-Löf identity type with strict $\beta$-rule (Section 2.16). As far as I know, in CHM/CCHM we don't need propositional univalence for strict identity types.

So in CHM/CCHM propositional univalence is a convenience feature. As to how to implement it, one way would be to compute cofibrations to a suitable normal form during conversion checking, and compare those. A less efficient way is to just check inter-provability. This should be available in any implementation, because we have to decide $\phi \vdash \psi$ anyway in computations, e.g. when computing "systems".