6.3 The interval

The interval, which we denote I, is perhaps an even simpler higher inductive type than the circle. It is generated by:

  • β€’

    a point 0I:I,

  • β€’

    a point 1I:I, and

  • β€’

    a path π—Œπ–Ύπ—€:0I=I1I.

The recursion principle for the interval says that given a type B along with

  • β€’

    a point b0:B,

  • β€’

    a point b1:B, and

  • β€’

    a path s:b0=b1,

there is a function f:Iβ†’B such that f⁒(0I)≑b0, f⁒(1I)≑b1, and f(π—Œπ–Ύπ—€)=s. The inductionMathworldPlanetmath principle says that given P:I→𝒰 along with

  • β€’

    a point b0:P⁒(0I),

  • β€’

    a point b1:P⁒(1I), and

  • β€’

    a path s:b0=π—Œπ–Ύπ—€Pb1,

there is a function f:∏(x:I)P⁒(x) such that f⁒(0I)≑b0, f⁒(1I)≑b1, and 𝖺𝗉𝖽f(π—Œπ–Ύπ—€)=s.

Regarded purely up to homotopyMathworldPlanetmath, the interval is not really interesting:

Lemma 6.3.1.

The type I is contractible.


We prove that for all x:I we have x=I1I. In other words we want a function f of type ∏(x:I)(x=I1I). We begin to define f in the following way:

f⁒(0I) :β‰‘π—Œπ–Ύπ—€ :0I =I1I,
f⁒(1I) :≑𝗋𝖾𝖿𝗅1I :1I =I1I.

It remains to define 𝖺𝗉𝖽f(π—Œπ–Ύπ—€), which must have type π—Œπ–Ύπ—€=π—Œπ–Ύπ—€Ξ»β’x.x=I1I𝗋𝖾𝖿𝗅1I. By definition this type is π—Œπ–Ύπ—€*(π—Œπ–Ύπ—€)=1I=I1I𝗋𝖾𝖿𝗅1I, which in turn is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to π—Œπ–Ύπ—€-1⁒\centerdotβ’π—Œπ–Ύπ—€=𝗋𝖾𝖿𝗅1I. But there is a canonical element of that type, namely the proof that path inversesPlanetmathPlanetmathPlanetmathPlanetmath are in fact inverses. ∎

However, type-theoretically the interval does still have some interesting features, just like the topological interval in classical homotopy theory. For instance, it enables us to give an easy proof of function extensionality. (Of course, as in Β§4.9 (http://planetmath.org/49univalenceimpliesfunctionextensionality), for the duration of the following proof we suspend our overall assumptionPlanetmathPlanetmath of the function extensionality axiom.)

Lemma 6.3.2.

If f,g:Aβ†’B are two functions such that f⁒(x)=g⁒(x) for every x:A, then f=g in the type Aβ†’B.


Let’s call the proof we have p:∏(x:A)(f(x)=g(x)). For all x:A we define a function p~x:Iβ†’B by

p~x⁒(0I) :≑f(x),
p~x⁒(1I) :≑g(x),
p~x(π—Œπ–Ύπ—€) :=p⁒(x).

We now define q:I→(A→B) by


Then q⁒(0I) is the function λ⁒x.p~x⁒(0I), which is equal to f because p~x⁒(0I) is defined by f⁒(x). Similarly, we have q⁒(1I)=g, and hence

Title 6.3 The interval