Kubus

9. Higher inductive types

A higher inductive type has path constructors as well as point constructors. A path constructor takes interval arguments, and its boundary says what it is on the faces.

The circle

The circle has a point base and a loop that starts and ends at base:

lib/circle.ktt
✓data S1 : U := base | loop (i : I) [i = 0 -> base, i = 1 -> base]
✓def loopP : Path S1 base base := \i -> loop i

loop takes an interval argument; loopP packages it as a path.

import loopspace
#check loopP
loopP : Path S1 base base
#eval loop 0
base
  : S1

Functions out of the circle

A function out of a higher inductive type has a clause for each constructor. The clause for a path constructor must agree with the clauses for its boundary, which Kubus checks. To map the circle to itself, send base somewhere and loop i to a loop there:

✓def double : S1 -> S1
| base => base
| loop i => trans loopP loopP i

A clause that does not respect the boundary is rejected:

expected to fail
def broken : S1 -> Int
| base => pos zero
| loop i => negsuc zero
clause for loop does not agree with its boundary:
  clause gives: negsuc zero
  boundary:     pos zero
context:
  i : I

The universal cover and winding numbers

The universal cover of the circle sends base to the integers and loop to the path Int = Int given by the successor equivalence (sucPathInt, made with ua). Transporting pos zero along the lift of a loop counts how often the loop winds around the circle:

lib/circle.ktt
✓def helix : S1 -> U
| base => Int
| loop i => sucPathInt i
✓def winding (p : Path S1 base base) : Int := transport (\i -> helix (p i)) (pos zero)

and because ua computes, so does winding:

#eval winding loopP
pos (suc zero)
  : Int
#eval winding (trans loopP (trans loopP loopP))
pos (suc (suc (suc zero)))
  : Int
#eval winding (trans (sym loopP) (sym loopP))
negsuc (suc zero)
  : Int
#eval winding (\i -> double (loop i))
pos (suc (suc zero))
  : Int

The loop space of the circle is the integers

lib/loopspace.ktt proves that the type of loops at base is equal to Int, by an encode-decode argument and isoToPath:

#check loopSpaceS1
loopSpaceS1 : Path U (Path S1 base base) Int
#eval transport loopSpaceS1 (trans loopP loopP)
pos (suc (suc zero))
  : Int

Transport along this path in the other direction turns an integer into a loop (again with sym^1, chapter 10):

#eval transport (sym^1 loopSpaceS1) (negsuc zero)
λ i → hcomp k S1 [i = 0 -> base, i = 1 -> base] (hcomp k S1 [i = 0 -> base, i = 1 -> base] (loop ~i))
  : Path S1 base base

Truncations and suspensions

Higher inductive types can have parameters. The propositional truncation of A has the elements of A and a path between any two elements; the suspension of A has two points and a path between them for every element of A:

lib/hits.ktt
✓data Trunc (A : U) : U :=
| inc (a : A)
| squash (x y : Trunc A) (i : I) [i = 0 -> x, i = 1 -> y]
✓def truncIsProp (A : U) : isProp (Trunc A) := \x y i -> squash x y i
✓def truncRec {A B : U} (h : isProp B) (f : A -> B) : Trunc A -> B
| inc a => f a
| squash x y i => h (truncRec h f x) (truncRec h f y) i
✓data Susp (A : U) : U :=
| north
| south
| merid (a : A) (i : I) [i = 0 -> north, i = 1 -> south]

Functions on parameterized higher inductive types are defined the same way:

import hits
✓def boolToSusp : Bool -> Susp Bool
| false => north
| true => south
#check suspMap not
suspMap not : Susp Bool → Susp Bool

Kubus does not yet support boundaries that apply functions to the constructor's arguments, so pushouts and general colimits cannot be declared directly yet.