Both the cubical coverage code and the implementation of the cubical primitives construct applications of the cubical primitives (e.g. the De Morgan operations, but also transp and hcomp) as literal Def-headed terms. This ends up generating big and ugly terms that the rest of the elaborator has to cope with, e.g. this subterm of a generated clause for J on the inductive identity:
(JPx1(comp(λi→x≡x2i)(λi''→primPOri0(~i'∨((~(~i0)∨~i0)∨i')∨φ)(λ.o1→x0)(primPOr(~i')(((~(~i0)∨~i0)∨i')∨φ)(λ.o1→Agda.Builtin.Equality.transpX-_≡_(λh→x2(i''∧h∨~i0))((φ∨~i'')∨~i0)(Agda.Builtin.Equality.transpX-_≡_(λh→x2(i''∧h∧~i0))((φ∨~i'')∨~(~i0))x0))(λ.o1→Agda.Builtin.Equality.transpX-_≡_(λh→x2(i''∧h))(φ∨~i'')x0)))x0))These could be cleaned up in construction time by writing smart constructors for applications of primIMin, etc., which apply the 'cheap' De Morgan laws. This should hopefully get rid of the need to normalize generated clauses.
Both the cubical coverage code and the implementation of the cubical primitives construct applications of the cubical primitives (e.g. the De Morgan operations, but also transp and hcomp) as literal `Def`-headed terms. This ends up generating big and ugly terms that the rest of the elaborator has to cope with, e.g. this subterm of a generated clause for `J` on the inductive identity:
```agda
(J P x1
(comp (λ i → x ≡ x2 i)
(λ i'' →
primPOr i0 (~ i' ∨ ((~ (~ i0) ∨ ~ i0) ∨ i') ∨ φ) (λ .o1 → x0)
(primPOr (~ i') (((~ (~ i0) ∨ ~ i0) ∨ i') ∨ φ)
(λ .o1 →
Agda.Builtin.Equality.transpX-_≡_ (λ h → x2 (i'' ∧ h ∨ ~ i0))
((φ ∨ ~ i'') ∨ ~ i0)
(Agda.Builtin.Equality.transpX-_≡_ (λ h → x2 (i'' ∧ h ∧ ~ i0))
((φ ∨ ~ i'') ∨ ~ (~ i0)) x0))
(λ .o1 →
Agda.Builtin.Equality.transpX-_≡_ (λ h → x2 (i'' ∧ h)) (φ ∨ ~ i'')
x0)))
x0))
```
These could be cleaned up in construction time by writing smart constructors for applications of `primIMin`, etc., which apply the 'cheap' De Morgan laws. This should hopefully get rid of the need to `normalize` generated clauses.