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" (where $1_{\mathbb F}$ means the truth):
$$ \cfrac{\Gamma,\phi\vdash \psi\equiv 1_{\mathbb F} \quad \Gamma,\psi\vdash \phi\equiv 1_{\mathbb F}}{\Gamma\vdash \phi\equiv\psi} $$$$ \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?