Higher inductive types in cubical type theory.
from 'On Higher Inductive Types' Coquand, Huber & Mörtberg 3.3
Circle and Spheres (Z)
| Formation |
| |
 S1 |
|
(Z) |
|
|
|
The circle has two constructors:
| Introduction |
|
r: |
| loop r :S1 |
|
() |
|
|
| Elimination |
| x :S1P(x) |
|
b:P(base) |
|
l :Pathi P(loop i)b b |
|
u:S1 |
|
S1 -elimx.p b l u : P(u) |
|
() |
|
where:
Pathi is a dependant path type
| From CubicalTT |
data S1 = base
| loop [ (i=0) -> base
, (i=1) -> base] |
Torus
| From CubicalTT |
data Torus = ptT
| pathOneT [ (i=0) -> ptT, (i=1) -> ptT ]
| pathTwoT [ (i=0) -> ptT, (i=1) -> ptT ]
| squareT [ (i=0) -> pathOneT {Torus} @ j
, (i=1) -> pathOneT {Torus} @ j
, (j=0) -> pathTwoT {Torus} @ i
, (j=1) -> pathTwoT {Torus} @ i ]
-- Torus = S1 * S1 proof
-- pathTwoT x
-- ________________
-- | |
-- pathOneT y | squareT x y | pathOneT y
-- | |
-- | |
-- ________________
-- pathTwoT x
-- pathOneT is (loop,refl)
-- pathTwoT is (refl,loop) |
n-sphere (Suspensions)
| From CubicalTT |
-- Suspension. Definition of the circle as the suspension of bool and
-- a proof that this is equal to the standard HIT representation of
-- the circle.
data susp (A : U) = north
| south
| merid (a : A) [ (i=0) -> north
, (i=1) -> south ]
-- n-spheres
sphere : nat -> U = split
zero -> bool
suc n -> susp (sphere n) |
Propositional Truncation
| From CubicalTT |
data pTrunc (A : U)
= inc (a : A)
| inh (x y : pTrunc A) [(i=0) -> x, (i=1) -> y] |
Pushouts
