Higher inductive types in cubical type theory.
from 'On Higher Inductive Types' Coquand, Huber & Mörtberg 3.3
Circle and Spheres (Z)
Formation 

S^{1} 

(Z_{}) 



The circle has two constructors:
Introduction 

r: 
loop r :S^{1} 

() 


Elimination 
x :S^{1} P(x) 

b:P(base) 

l :Path^{i} P(loop i)b b 

u:S^{1} 

S^{1} elim_{x.p} b l u : P(u) 

() 

where:
Path^{i} 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) 
nsphere (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 ]
 nspheres
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