Higher Inductive Types

Higher inductive types generalize ordinary inductive types. Various homotopy colimits of types and other constructions such as truncations are higher inductive types. A specific homotopy structure of a higher inductive type can be defined by means of conditions in data definitions.

Conditions

If con is a constructor of an inductive type D, then an expression of the form con a_1 … a_n does not reduce any further unless the definition of D contains conditions on con. A condition on a constructor is a rule that says how such an expression might be reduced. For example, one can define integers as a data type with two constructors: one for positive, and one for negative integers, and a condition on the second constructor telling positive and negative zero have to be computationally equal:

\data Int
  | pos Nat
  | neg Nat \with {
    | zero => pos zero
  }

Conditions are imposed on a constructor by defining it as a function by pattern matching. The only differences are that it is not required that all cases are covered and that pattern matching on constructors left and right of the interval type I is allowed. The general syntax is the same as for ordinary pattern matching. Either \with { | c_1 | … | c_m } or \elim x_1, … x_n { | c_1 | … | c_m } can be added after parameters of the constructor, where | c_1 | … | c_m is a list of clauses.

A constructor with conditions evaluates if its arguments match the specification in the same way as a function defined by pattern matching. This means that a function over a data type with conditions must respect the conditions, this is checked by the typechecker. For example, a function of type Int -> X must map positive and negative zero to the same value. Thus, one cannot define the following function:

\func f (x : Int) : Nat
  | pos n => n
  | neg n => suc n

Higher inductive types

A higher inductive type (HIT) is a data type with a constructor that has conditions of the form | left => e and | right => e’. Let us give a few examples:

-- Circle
\data S1
  | base
  | loop I \with {
    | left => base
    | right => base
  }

-- Suspension
\data Susp (A : \Type)
  | north
  | south
  | merid A (i : I) \elim i {
    | left => north
    | right => south
  }

-- Propositional truncation
\data Trunc (A : \Type)
  | inT A
  | truncT (x y : Trunc A) (i : I) \elim i {
    | left => x
    | right => y
  }

-- Set quotient
\data Quotient (A : \Type) (R : A -> A -> \Type)
  | inQ A
  | equivQ (x y : A) (R x y) (i : I) \elim i {
    | left => inQ x
    | right => inQ y
  }
  | truncQ (a a' : Quotient A R) (p p' : a = a') (i j : I) \elim i, j {
    | i, left  => p @ i
    | i, right => p' @ i
    | left,  _ => a
    | right, _ => a'
  }

If X is a proposition, then, to define a function of type Trunc A -> X, it is enough to specify its value for inT a. The same works for any higher inductive type and any level. For example, to define a function Quotient A R -> X, it is enough to specify its value for inQ a and equivQ x y r i if X is a set and only for inQ a if it is a proposition. This also works for several arguments. For example, if X is a set, then, to define a function Quotient A R -> Quotient A R -> X, it is enough to specify its value for inQ a, inQ a’, inQ a, equivQ x y r i, and equivQ x y r i, inQ a.

Another syntax for HITs

There is a special syntax for defining higher inductive types. Instead of writing down conditions explicitly, they can be specified by giving the type of the constructor. The type of each constructor must be an iterated path type in the data itself. The endpoints of these path types specify the conditions. The examples above can be rewritten in this syntax as follows:

-- Circle
\data S1
  | base
  | loop : base = base

-- Suspension
\data Susp (A : \Type)
  | north
  | south
  | merid A : north = south

-- Propositional truncation
\data Trunc (A : \Type)
  | inT A
  | truncT (x y : Trunc A) : x = y

-- Set quotient
\data Quotient (A : \Type) (R : A -> A -> \Type)
  | inQ A
  | equivQ (x y : A) (R x y) : inQ x = inQ y
  | truncQ (a a' : Quotient A R) (p p' : a = a') : Path (\lam i => p i = p' i) idp idp

Pattern matching on HITs

There is also a special syntax for pattern matching on HITs. In this syntax, the interval variables can be omitted and the right hand side should be a path. Then the typechecker will insert missing variables and apply the right hand side to them.

For example, function double below is equivalent to double’.

\func double (x : S1) : S1
  | base => base
  | loop => loop *> loop

\func double' (x : S1) : S1
  | base => base
  | loop i => (loop *> loop) i

Here, *> is the path concatenation function.