Search

• < Previous
• 1
• Next >

Canonicity and homotopy canonicity for cubical type theory

Cubical type theory provides a constructive justification of homotopy type theory. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices. We present in this article two canonicity&nbsp;[&hellip;]