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 $0_{I}:I$ ,
•

a point $1_{I}:I$ , and
•

a path $\mathsf{seg}:0_{I}=_{I}1_{I}$ .

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

•

a point $b_{0}:B$ ,
•

a point $b_{1}:B$ , and
•

a path $s:b_{0}=b_{1}$ ,

there is a function $f:I\to B$ such that $f(0_{I})\equiv b_{0}$ , $f(1_{I})\equiv b_{1}$ , and ${f}\mathopen{}\left({\mathsf{seg}}\right)\mathclose{}=s$ . The induction principle says that given $P:I\to\mathcal{U}$ along with

•

a point $b_{0}:P(0_{I})$ ,
•

a point $b_{1}:P(1_{I})$ , and
•

a path $s:b_{0}=^{P}_{\mathsf{seg}}b_{1}$ ,

there is a function $f:\mathchoice{\prod_{x:I}\,}{\mathchoice{{\textstyle\prod_{(x:I)}}}{\prod_{(x:% I)}}{\prod_{(x:I)}}{\prod_{(x:I)}}}{\mathchoice{{\textstyle\prod_{(x:I)}}}{% \prod_{(x:I)}}{\prod_{(x:I)}}{\prod_{(x:I)}}}{\mathchoice{{\textstyle\prod_{(x% :I)}}}{\prod_{(x:I)}}{\prod_{(x:I)}}{\prod_{(x:I)}}}P(x)$ such that $f(0_{I})\equiv b_{0}$ , $f(1_{I})\equiv b_{1}$ , and $\mathsf{apd}_{f}\mathopen{}\left(\mathsf{seg}\right)\mathclose{}=s$ .

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

Lemma 6.3.1.

The type $I$ is contractible.

Proof.

We prove that for all $x : I$ we have $x=_{I}1_{I}$ . In other words we want a function $f$ of type $\mathchoice{\prod_{x:I}\,}{\mathchoice{{\textstyle\prod_{(x:I)}}}{\prod_{(x:I)% }}{\prod_{(x:I)}}{\prod_{(x:I)}}}{\mathchoice{{\textstyle\prod_{(x:I)}}}{\prod% _{(x:I)}}{\prod_{(x:I)}}{\prod_{(x:I)}}}{\mathchoice{{\textstyle\prod_{(x:I)}}% }{\prod_{(x:I)}}{\prod_{(x:I)}}{\prod_{(x:I)}}}(x=_{I}1_{I})$ . We begin to define $f$ in the following way:

	$\displaystyle f(0_{I})$	$\displaystyle:\!\!\equiv\mathsf{seg}$	$\displaystyle:0_{I}$	$\displaystyle=_{I}1_{I},$
	$\displaystyle f(1_{I})$	$\displaystyle:\!\!\equiv\mathsf{refl}_{1_{I}}$	$\displaystyle:1_{I}$	$\displaystyle=_{I}1_{I}.$

It remains to define $\mathsf{apd}_{f}\mathopen{}\left(\mathsf{seg}\right)\mathclose{}$ , which must have type $\mathsf{seg}=_{\mathsf{seg}}^{{\lambda}x.\,x=_{I}1_{I}}\mathsf{refl}_{1_{I}}$ . By definition this type is ${\mathsf{seg}}_{*}\mathopen{}\left({\mathsf{seg}}\right)\mathclose{}=_{1_{I}=_% {I}1_{I}}\mathsf{refl}_{1_{I}}$ , which in turn is equivalent to $\mathord{{\mathsf{seg}}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{seg}=\mathsf{refl}_{1_{I}}$ . But there is a canonical element of that type, namely the proof that path inverses 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 assumption of the function extensionality axiom.)

Lemma 6.3.2.

If $f,g:A\to{}B$ are two functions such that $f(x)=g(x)$ for every $x : A$ , then $f=g$ in the type $A\to{}B$ .

Proof.

Let’s call the proof we have $p:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}(f(x)=g(x))$ . For all $x : A$ we define a function $\widetilde{p}_{x}:I\to{}B$ by

	$\displaystyle\widetilde{p}_{x}(0_{I})$	$\displaystyle:\!\!\equiv f(x),$
	$\displaystyle\widetilde{p}_{x}(1_{I})$	$\displaystyle:\!\!\equiv g(x),$
	$\displaystyle{\widetilde{p}_{x}}\mathopen{}\left({\mathsf{seg}}\right)% \mathclose{}$	$\displaystyle:=p(x).$

We now define $q:I\to(A\to{}B)$ by

q(i):\!\!\equiv({\lambda}x.\,\widetilde{p}_{x}(i))

Then $q(0_{I})$ is the function ${\lambda}x.\,\widetilde{p}_{x}(0_{I})$ , which is equal to $f$ because $\widetilde{p}_{x}(0_{I})$ is defined by $f(x)$ . Similarly, we have $q(1_{I})=g$ , and hence

{q}\mathopen{}\left({\mathsf{seg}}\right)\mathclose{}:f=_{(A\to{}B)}g\qed

Title	6.3 The interval
\metatable