Cube Category

Example of a model category for Homotopy Type Theory.
Must have:

• Constants $0,1:{\square }^1$.
• Boundary inclusions from ${\square }^n\to {\square }^{n+1}$
• Projection maps ${\square }^{n+1}\to {\square }^n$
• Truncation $|\_|:\square \to \mathrm{NiceTop}$.
• Diagonal maps ${\square }^1\to {\square }^2$.
• Symmetries ${\square }^2\to {\square }^2$
• Connections $\wedge ,\vee :{\square }^2\to {\square }^1$.
• Reversal $:{\square }^1\to {\square }^1$

Properties

Is an Affine Logic.
Gives a constructive model of Homotopy Type Theory.
Gives cubical type theory with Canonicity. (Simon Huber)
Leads to type theoretic model structures on presheaves on some cube category ($Psh(\square )$).
Always monoidal categories - day convolution, free monoidal by adding dimensions.

Examples

BCH

This preserves CWF Morphism.

Satisfies DeMorgan laws.

Write successor between pre-sheaf models as $\forall$.

This is the basis of higher observational type theory.

CCHM

For $|\_|$ faithful it needs to satisfy the Kleene Law

We want Thomason Model Structure ~ Psh $\square$ ~ NiceTop.

Remarks

Cartesian cubical type theory exists, but isn’t used in practice — why?

Open questions

Conjecture: Any cube category can model infinity topoi
Is there a version of cubical agda that includes the DeMorgan laws?
Is there a version of cubical type theory that computes over the dedekind operator?

Sources

Ulrik Buchholtz