Cubical Type Theory, Canonicity, and the Computational¶
Job: develop the cubical type theory (interval \(I\), Kan composition), the canonicity / normalization, the HITs in cubical, and the computational univalence — with the cubical \(S^1\) / Kan composition as the worked example.
Core¶
The cubical type theory¶
| Cubical / interval \(I\) / Kan / computational | Description |
|---|---|
| Cubical TT (Cohen–Coquand–Huber–Mörtberg) | interval \(I\), Kan composition / filling, the computational univalence (the foundations) |
| Kan composition | \(h\)-composition, \(h\)-filling (the foundations) |
The canonicity and the normalization¶
| Canonicity / normalization / cubical | Description |
|---|---|
| Canonicity | cubical \(\Rightarrow\) canonicity (closed terms normalize to numerals, the foundations) |
| Normalization | cubical normalization (decidable equality for some fragments) |
The HITs and the cubical¶
| HITs / \(S^1\) / suspension / pushout | Description |
|---|---|
| HITs in cubical | \(S^1\), suspension, pushout, quotients — path constructors compute via Kan (the foundations) |
| Cubical \(S^1\) | \(S^1 = I/\partial I\) the quotient, \(\mathsf{base}\), \(\mathsf{loop}\) (the foundations) |
The computational and the decidable¶
| Computational / decidable / univalence | Description |
|---|---|
| Computational univalence | \(\mathsf{ua}\) computes (the foundations) |
| Decidable | cubical fragments with decidable equality (the foundations) |
See it¶
Cubical \(S^1\) via the interval and the Kan composition / computational univalence. The cubical \(S^1\): the \(\mathsf{base}\), the \(\mathsf{loop}\) (the interval \(I\), the \(S^1=I/\partial I\) the quotient, the foundations). The Kan: the composition the filling (the \(h\)-comp, the \(h\)-fill, the foundations). The computational univalence: the \(\mathsf{ua}\) the computational (the foundations). The key point: the cubical \(S^1\) the interval, the Kan the composition, the computational univalence.
Check¶
Explain the cubical interval \(I\) and the Kan composition, and the computational univalence.
The interval \(I\): the \(i:I\) (the de Morgan algebra \(0,1,\wedge,\vee,\neg\), the foundations). The Kan composition: the \(h\)-comp (the \(\mathrm{comp}^i_A[\varphi\mapsto u](t)\) the composition along \(i\), the foundations). The Kan filling: the \(h\)-fill (the \(\mathrm{fill}^i_A[\varphi\mapsto u](t)\) the filling, the foundations). The computational univalence: the \(\mathsf{ua}(e)\) computes (the \(\mathsf{ua}\) the function, the foundations, the cubical the canonicity). So the \(I\) the interval, the Kan the comp / fill, the \(\mathsf{ua}\) the computational.
Explain the canonicity and the normalization in cubical type theory.
The canonicity: the cubical \(\Rightarrow\) the canonicity (the closed terms \(n:\mathbb{N}\) normalize to the numerals \(0\) / \(\mathsf{suc}\), the foundations, the cubical the canonicity). The normalization: the cubical normalization (the decidable equality for the h-sets / the fragments, the foundations, the Huber–Mörtberg). The cubical: the \(I\) the interval, the Kan the comp (the foundations). So the canonicity the numerals, the normalization the decidable.
Pitfalls¶
- The interval \(I\) the de Morgan (\(0,1,\wedge,\vee,\neg\), the foundations) — the \(I\) the interval, the Kan the comp.
- The canonicity the cubical (the numerals, the foundations) — the cubical the canonicity, the plain MLTT + univalence the not-canonicity.
- The computational univalence (the \(\mathsf{ua}\) computes, the foundations) — the computational the cubical, the axiomatic the not.
- The normalization the fragments (the h-sets, the foundations) — the normalization the decidable, the full the open.
Refs¶
- Cohen–Coquand–Huber–Mörtberg, "Cubical type theory: a constructive interpretation of the univalence axiom" (2016)
- Huber, "Canonicity for cubical type theory" (2017); the canonicity
- Voevodsky, "Univalent foundations" (2009–); the univalence (the foundations)
- Mortberg, "Normalization in cubical type theory" (2020); the normalization
Next¶
HoTT index · Foundations · Synthetic Homotopy · Models & Semantics · Univalent Categories · Infinity-topoi