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

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?

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