nLab interval type

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Idea

The interval type is an axiomatization of the cellular interval object in the context of homotopy type theory.

Definition

As a higher inductive type, the interval is given by

Inductive Interval : Type
  | left : Interval
  | right : Interval
  | segment : Id Interval left right

This says that the type is inductive constructed from two terms in the interval, whose interpretation is as the endpoints of the interval, together with a term in the identity type of paths between these two terms, which interprets as the 1-cell of the interval

leftsegmentright. left \stackrel{segment}{\to} right \,.

Induction principle

The induction principle for the interval II says that for any P:ITypeP:I\to Type equipped with point left:P(left)left' : P(left) and right:P(right)right' : P(right) and a dependent identification segment:left= P segmentrightsegment':left'=_P^{segment} right', there is f: (x:I)P(x)f:\prod_{(x:I)} P(x) such that:

f(left)=leftf(right)=rightapd f(segment)=segmentf(left)=left' \qquad f(right)=right' \qquad apd_f(segment) = segment'

and for every y:Ig: (x:I)P(x)y:I \vdash g:\prod_{(x:I)} P(x) such that

y:Ig(y)(left)=lefty:Ig(y)(right)=righty:Iapd g(y)(segment)=segmenty:I \vdash g(y)(left)=left' \qquad y:I \vdash g(y)(right)=right' \qquad y:I \vdash apd_{g(y)}(segment) = segment'

there is an identification y:If=g(y)y:I \vdash f = g(y).

As a special case, its recursion principle says that given any type II with points x:Xx:X and y:Xy:X and an identification p:x=yp:x=y, there is f:IXf:I \to X with

f(left)=xf(right)=yap f(segment)=pf(left)=x\qquad f(right)=y\qquad ap_f(segment)=p

Syntax

The interval type is defined by the following rules:

Formation rules for the interval type:

ΓctxΓ𝕀type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{I} \; \mathrm{type}}

Introduction rules for the interval type:

ΓctxΓ0:𝕀ΓctxΓ1:𝕀ΓctxΓp:0= 𝕀1\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{I}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 1:\mathbb{I}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash p:0 =_\mathbb{I} 1}

Elimination rules for the interval type:

Γ,x:𝕀C(x)typeΓc 0:C(0)Γc 1:C(1)Γc p:c 0= C pc 1Γ,x:𝕀ind 𝕀 C(c 0,c 1,c p)(x):C(x)\frac{\Gamma, x:\mathbb{I} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_1:C(1) \quad \Gamma \vdash c_p:c_0 =_C^p c_1}{\Gamma, x:\mathbb{I} \vdash \mathrm{ind}_\mathbb{I}^C(c_0, c_1, c_p)(x):C(x)}

Computation rules for the interval type:

  • judgmental computational rules
    Γ,x:𝕀C(x)typeΓc 0:C(0)Γc 1:C(1)Γc p:c 0= C pc 1Γind 𝕀 C(c 0,c 1,c p)(0)c 0:C(0)\frac{\Gamma, x:\mathbb{I} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_1:C(1) \quad \Gamma \vdash c_p:c_0 =_C^p c_1}{\Gamma \vdash \mathrm{ind}_\mathbb{I}^{C}(c_0, c_1, c_p)(0) \equiv c_0:C(0)}
Γ,x:𝕀C(x)typeΓc 0:C(0)Γc 1:C(1)Γc p:c 0= C pc 1Γind 𝕀 C(c 0,c 1,c p)(1)c 1:C(1)\frac{\Gamma, x:\mathbb{I} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_1:C(1) \quad \Gamma \vdash c_p:c_0 =_C^p c_1}{\Gamma \vdash \mathrm{ind}_\mathbb{I}^{C}(c_0, c_1, c_p)(1) \equiv c_1:C(1)}
Γ,x:𝕀C(x)typeΓc 0:C(0)Γc 1:C(1)Γc p:c 0= C pc 1Γapd C(ind 𝕀 C(c 0,c 1,c p),0,1,p)c p:c 0= C pc 1\frac{\Gamma, x:\mathbb{I} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_1:C(1) \quad \Gamma \vdash c_p:c_0 =_C^p c_1}{\Gamma \vdash \mathrm{apd}_C(\mathrm{ind}_\mathbb{I}^{C}(c_0, c_1, c_p), 0, 1, p) \equiv c_p:c_0 =_C^p c_1}
  • propositional computation rules
    Γ,x:𝕀C(x)typeΓc 0:C(0)Γc 1:C(1)Γc p:c 0= C pc 1Γβ 𝕀 0(c 0,c 1,c p):ind 𝕀 C(c 0,c 1,c p)(0)= C(0)c 0\frac{\Gamma, x:\mathbb{I} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_1:C(1) \quad \Gamma \vdash c_p:c_0 =_C^p c_1}{\Gamma \vdash \beta_\mathbb{I}^{0}(c_0, c_1, c_p): \mathrm{ind}_\mathbb{I}^{C}(c_0, c_1, c_p)(0) =_{C(0)} c_0}
Γ,x:𝕀C(x)typeΓc 0:C(0)Γc 1:C(1)Γc p:c 0= C pc 1Γβ 𝕀 1(c 0,c 1,c p):ind 𝕀 C(c 0,c 1,c p)(1)= C(1)c 1\frac{\Gamma, x:\mathbb{I} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_1:C(1) \quad \Gamma \vdash c_p:c_0 =_C^p c_1}{\Gamma \vdash \beta_\mathbb{I}^{1}(c_0, c_1, c_p):\mathrm{ind}_\mathbb{I}^{C}(c_0, c_1, c_p)(1) =_{C(1)} c_1}
Γ,x:𝕀C(x)typeΓc 0:C(0)Γc 1:C(1)Γc p:c 0= C pc 1Γβ 𝕀 p(c 0,c 1,c p):apd C(ind 𝕀 C(c 0,c 1,c p),0,1,p)= c 0= C pc 1c p\frac{\Gamma, x:\mathbb{I} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_1:C(1) \quad \Gamma \vdash c_p:c_0 =_C^p c_1}{\Gamma \vdash \beta_\mathbb{I}^{p}(c_0, c_1, c_p):\mathrm{apd}_C(\mathrm{ind}_\mathbb{I}^{C}(c_0, c_1, c_p), 0, 1, p) =_{c_0 =_C^p c_1} c_p}

Uniqueness rules for the interval type:

Γ,x:𝕀C(x)typeΓ,x:𝕀c:C(x)Γ,x:𝕀η 𝕀(c):c= C(x)ind 𝕀 C(c(0),c(1),apd C(p,c))\frac{\Gamma, x:\mathbb{I} \vdash C(x) \; \mathrm{type} \quad \Gamma, x:\mathbb{I} \vdash c:C(x)}{\Gamma, x:\mathbb{I} \vdash \eta_\mathbb{I}(c):c =_{C(x)} \mathrm{ind}_\mathbb{I}^{C}(c(0), c(1), \mathrm{apd}_C(p, c))}

The elimination rules and the propositional computation and uniqueness rules for the interval type state that the interval type satisfy the dependent universal property of the interval type. If the dependent type theory also has dependent sum types and product types, allowing one to define the uniqueness quantifier, the dependent universal property of the interval type could be simplified to the following rule:

Γ,x:𝕀C(x)typeΓc 0:C(0)Γc 1:C(1)Γc p:c 0= C pc 1Γup 𝕀 C(c 0,c 1,c p):!c: x:𝕀C(x).(c(0)= C(0)c 0)×(c(1)= C(1)c 1)×(apd x:𝕀.C(x)(c,c 0,c 1,c p)= c 0= C pc 1c p)\frac{\Gamma, x:\mathbb{I} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_1:C(1) \quad \Gamma \vdash c_p:c_0 =_C^p c_1}{\Gamma \vdash \mathrm{up}_\mathbb{I}^C(c_0, c_1, c_p):\exists!c:\prod_{x:\mathbb{I}} C(x).(c(0) =_{C(0)} c_0) \times (c(1) =_{C(1)} c_1) \times (\mathrm{apd}_{x:\mathbb{I}.C(x)}(c, c_0, c_1, c_p) =_{c_0 =_C^p c_1} c_p)}

In type theories with a separate type judgment where not all types are elements of universes, one has to additionally add the following elimination and computation rules:

Elimination rules:

ΓAtypeΓBtypeΓe:ABΓ,x:Ityperec 𝕀 A,B(e,i)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma, x:\mathrm{I} \vdash \mathrm{typerec}_{\mathbb{I}}^{A, B}(e, i) \; \mathrm{type}}

Computation rules:

  • judgmental computation rules
    ΓAtypeΓBtypeΓe:ABΓtyperec 𝕀 A,B(e,0)Atype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \mathrm{typerec}_{\mathbb{I}}^{A, B}(e, 0) \equiv A \; \mathrm{type}}
ΓAtypeΓBtypeΓe:ABΓtyperec 𝕀 A,B(e,1)Btype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \mathrm{typerec}_{\mathbb{I}}^{A, B}(e, 1) \equiv B \; \mathrm{type}}
ΓAtypeΓBtypeΓe:ABΓtransport typerec 𝕀 A,B(e)(0,1,p 𝕀)e:AB\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \mathrm{transport}_{\mathrm{typerec}_{\mathbb{I}}^{A, B}(e)}(0, 1, p_\mathbb{I}) \equiv e:A \simeq B}
  • typal computation rules
    ΓAtypeΓBtypeΓe:ABΓβ I 0,A,B(e):typerec 𝕀 A,B(e,0)A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \beta_{\mathrm{I}}^{0, A, B}(e):\mathrm{typerec}_{\mathbb{I}}^{A, B}(e, 0) \simeq A}
ΓAtypeΓBtypeΓe:ABΓβ I 1,A,B(e):typerec 𝕀 A,B(e,1)B\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \beta_{\mathrm{I}}^{1, A, B}(e):\mathrm{typerec}_{\mathbb{I}}^{A, B}(e, 1) \simeq B}
ΓAtypeΓBtypeΓe:ABΓβ I p I,A,B(e):β I 1,A,B(e)transport typerec 𝕀 A,B(e)(0,1,p 𝕀)β I 0,A,B(e) 1= ABe\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \beta_{\mathrm{I}}^{p_\mathrm{I}, A, B}(e):\beta_{\mathrm{I}}^{1, A, B}(e) \circ \mathrm{transport}_{\mathrm{typerec}_{\mathbb{I}}^{A, B}(e)}(0, 1, p_\mathbb{I}) \circ \beta_{\mathrm{I}}^{0, A, B}(e)^{-1} =_{A \simeq B} e}

Using a function from the boolean domain

The interval type is defined by the following rules:

Formation rules for the interval type:

ΓctxΓ𝕀type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{I} \; \mathrm{type}}

Introduction rules for the interval type:

Γa:𝟚Γj(a):𝕀Γ0:𝟚Γ1:𝟚Γp:j(0)= 𝕀j(1)\frac{\Gamma \vdash a:\mathbb{2}}{\Gamma \vdash j(a):\mathbb{I}} \qquad \frac{\Gamma \vdash 0:\mathbb{2} \quad \Gamma \vdash 1:\mathbb{2}}{\Gamma \vdash p:j(0) =_\mathbb{I} j(1)}

Elimination rules for the interval type:

Γ,x:𝕀CtypeΓ,a:𝟚c:C[j(a)/x]Γ0:𝟚Γ1:𝟚Γc p:c[j(0)/x]= C pc[j(1)/x]Γ,x:𝕀,a:𝟚ind 𝕀 C(c[j(a)/x],c p):C\frac{\Gamma, x:\mathbb{I} \vdash C \; \mathrm{type} \quad \Gamma, a:\mathbb{2} \vdash c:C[j(a)/x] \quad \Gamma \vdash 0:\mathbb{2} \quad \Gamma \vdash 1:\mathbb{2} \quad \Gamma \vdash c_p:c[j(0)/x] =_C^p c[j(1)/x]}{\Gamma, x:\mathbb{I}, a:\mathbb{2} \vdash \mathrm{ind}_\mathbb{I}^C(c[j(a)/x], c_p):C}

Computation rules for the interval type:

Γ,x:𝕀CtypeΓ,a:𝟚c:C[j(a)/x]Γ0:𝟚Γ1:𝟚Γc p:c[j(0)/x]= C pc[j(1)/x]Γ,a:𝟚β 𝕀 j:ind 𝕀 C(c[j(a)/x],c p)[j(a)/x]= C[j(a)/x]c[j(a)/x]\frac{\Gamma, x:\mathbb{I} \vdash C \; \mathrm{type} \quad \Gamma, a:\mathbb{2} \vdash c:C[j(a)/x] \quad \Gamma \vdash 0:\mathbb{2} \quad \Gamma \vdash 1:\mathbb{2} \quad \Gamma \vdash c_p:c[j(0)/x] =_C^p c[j(1)/x]}{\Gamma, a:\mathbb{2} \vdash \beta_\mathbb{I}^{j}:\mathrm{ind}_\mathbb{I}^{C}(c[j(a)/x], c_p)[j(a)/x] =_{C[j(a)/x]} c[j(a)/x]}
Γ,x:𝕀CtypeΓ,a:𝟚c:C[j(a)/x]Γ0:𝟚Γ1:𝟚Γc p:c[j(0)/x]= C pc[j(1)/x]Γ,a:𝟚,β 𝕀 p:apd C p(ind 𝕀 C(c[j(a)/x],c p))= c[j(0)/x]= C pc[j(1)/x]c p\frac{\Gamma, x:\mathbb{I} \vdash C \; \mathrm{type} \quad \Gamma, a:\mathbb{2} \vdash c:C[j(a)/x] \quad \Gamma \vdash 0:\mathbb{2} \quad \Gamma \vdash 1:\mathbb{2} \quad \Gamma \vdash c_p:c[j(0)/x] =_C^p c[j(1)/x]}{\Gamma, a:\mathbb{2}, \vdash \beta_\mathbb{I}^{p}:\mathrm{apd}_C^p(\mathrm{ind}_\mathbb{I}^{C}(c[j(a)/x], c_p)) =_{c[j(0)/x] =_C^p c[j(1)/x]} c_p}

Uniqueness rules for the interval type:

Properties

  • An interval type is provably contractible. Conversely, any contractible type satisfies the rules of an interval type up to typal equality.

  • An interval type is a suspension type of the unit type, and the suspension of an interval type is a 2-globe type.

  • An interval type is a cone type of the unit type.

  • An interval type is a cubical type? 1\Box^1.

Induction principle without heterogeneous identifications

There is a version of the induction principle which uses a type CC and a function f:C𝕀f:C \to \mathbb{I} instead of a type family P(x)P(x) indexed by x:𝕀x:\mathbb{I}. It has the benefit of not requiring that one has first defined heterogeneous identification types, whether as an inductive family of types or by using transport.

The induction principle of the interval type says that given a type CC and a function f:C𝕀f:C \to \mathbb{I}, as well as

  • elements c 0:Cc_0:C and c 1:Cc_1:C

  • identifications c p:c 0= Cc 1c_p:c_0 =_C c_1, q 0:f(c 0)= 𝕀0q_0:f(c_0) =_\mathbb{I} 0 and q 1:f(c q)= 𝕀1q_1:f(c_q) =_\mathbb{I} 1 such that ap f(c p)\mathrm{ap}_f(c_p), q 0q_0, q 1q_1, and pp form a square

f(c 0) =ap f(c p) f(c 1) q 0 q 1 0 =p 1 \begin{array}{c} & f(c_0) & \overset{\mathrm{ap}_{f}(c_p)}= & f(c_1) & \\ q_0 & \Vert & & \Vert & q_1\\ & 0 & \underset{p}= & 1 & \\ \end{array}
  • an identification saying that the square commutes
q p:ap f(c p)q 1= f(c 0)= 𝕀f(c 1)q 0pq_p:\mathrm{ap}_f(c_p) \bullet q_1 =_{f(c_0) =_\mathbb{I} f(c_1)} q_0 \bullet p

one can construct

  • a function
g:𝕀Cg:\mathbb{I} \to C
  • a homotopy witnessing that gg is a section of ff:
sec g: x:𝕀f(g(x))= 𝕀x\mathrm{sec}_g:\prod_{x:\mathbb{I}} f(g(x)) =_\mathbb{I} x

such that

g(0)c 0sec g(0)q 0g(1)c 1sec g(1)q 1ap g(p)c pg(0) \equiv c_0 \quad \mathrm{sec}_g(0) \equiv q_0 \quad g(1) \equiv c_1 \quad \mathrm{sec}_g(1) \equiv q_1 \quad \mathrm{ap}_{g}(p) \equiv c_p
ind =(λx:𝕀.refl f(g(x))= 𝕀x(sec g(x)),0,1,p)q p\mathrm{ind}_{=}\left(\lambda x:\mathbb{I}.\mathrm{refl}_{f(g(x)) =_\mathbb{I} x}(\mathrm{sec}_g(x)), 0, 1, p\right) \equiv q_p

The last condition needs some explanation. Since gg is a section of ff, the composite fgf \circ g is the identity function on the interval type, up to identification. Now, given any identity function on the interval type i:𝕀𝕀i:\mathbb{I} \to \mathbb{I} with homotopy

j: x:𝕀i(x)= 𝕀xj:\prod_{x:\mathbb{I}} i(x) =_\mathbb{I} x

we have the following square for all x:𝕀x:\mathbb{I}, y:𝕀y:\mathbb{I}, and q:x= 𝕀yq:x =_\mathbb{I} y:

i(x) =ap i(q) i(y) j(x) j(y) x =q y \begin{array}{c} & i(x) & \overset{\mathrm{ap}_{i}(q)}= & i(y) & \\ j(x) & \Vert & & \Vert & j(y)\\ & x & \underset{q}= & y & \\ \end{array}

This square commutes via the J rule: it suffices to construct an element of

ap i(refl 𝕀(x))j(x)= i(x)= 𝕀xj(x)refl 𝕀(x)\mathrm{ap}_{i}(\mathrm{refl}_\mathbb{I}(x)) \bullet j(x) =_{i(x) =_\mathbb{I} x} j(x) \bullet \mathrm{refl}_\mathbb{I}(x)

But ap i(refl 𝕀(x))j(x)\mathrm{ap}_{i}(\mathrm{refl}_\mathbb{I}(x)) \bullet j(x) reduces down to j(x)j(x) via

ap i(refl 𝕀(x))j(x)refl 𝕀(i(x))j(x)j(x)\mathrm{ap}_{i}(\mathrm{refl}_\mathbb{I}(x)) \bullet j(x) \equiv \mathrm{refl}_\mathbb{I}(i(x)) \bullet j(x) \equiv j(x)

and similarly j(x)refl 𝕀(x)j(x) \bullet \mathrm{refl}_\mathbb{I}(x) reduces down to j(x)j(x), so just take reflexivity of j(x)j(x).

So the naturality square is inductively defined by

ind =(λx:𝕀.refl i(x)= 𝕀x(j(x)),x,y,q):ap i(q)j(y)= i(x)= 𝕀yj(x)q\mathrm{ind}_{=}\left(\lambda x:\mathbb{I}.\mathrm{refl}_{i(x) =_\mathbb{I} x}(j(x)), x, y, q\right):\mathrm{ap}_{i}(q) \bullet j(y) =_{i(x) =_\mathbb{I} y} j(x) \bullet q

When ifgi \coloneqq f \circ g, jsec gj \coloneqq \mathrm{sec}_g, x0x \coloneqq 0, y1y \coloneqq 1, and qpq \coloneqq p, this results in the identification

ind =(λx:𝕀.refl f(g(x))= 𝕀x(sec g(x)),0,1,p)\mathrm{ind}_{=}\left(\lambda x:\mathbb{I}.\mathrm{refl}_{f(g(x)) =_\mathbb{I} x}(\mathrm{sec}_g(x)), 0, 1, p\right)

which is of the same type as q pq_p due to the judgmental equalities in the other computation rules.

One gets back the usual induction principle of the interval type when C x:𝕀P(x)C \equiv \sum_{x:\mathbb{I}} P(x) and fπ 1f \equiv \pi_1 the first projection function of the dependent sum type, and one gets back the recursion principle of the interval type when C𝕀×PC \equiv \mathbb{I} \times P and fπ 1f \equiv \pi_1 the first projection function of the product type.

Path types and identity types

In general, functions from 𝕀\mathbb{I} to a type AA can be thought of as the paths in AA in Martin-Löf type theory, and the function type 𝕀A\mathbb{I} \to A can be thought of as the path types of AA, similar to how in topology paths in a (topological) space AA are (continuous) functions from the unit interval, and how in cubical type theory the cubical paths are a kind of function type out of the pre-defined interval pre-type.

The recursion principle of the interval type allows for paths to be defined from a given identification, and function application to identifications allows for identifications to be defined from a given path:

Theorem

Every identification q:a= Abq:a =_A b between two terms a:Aa:A and b:Ab:A of a type AA has an associated path rec 𝕀(a,b,p):𝕀A\mathrm{rec}_{\mathbb{I}}(a, b, p):\mathbb{I} \to A, recursively defined by

  • β 𝕀 0(a,b,q):rec 𝕀(a,b,q)(0)= Aa\beta_\mathbb{I}^0(a, b, q):\mathrm{rec}_{\mathbb{I}}(a, b, q)(0) =_A a
  • β 𝕀 1(a,b,q):rec 𝕀(a,b,q)(1)= Ab\beta_\mathbb{I}^1(a, b, q):\mathrm{rec}_{\mathbb{I}}(a, b, q)(1) =_A b
  • β 𝕀 p(a,b,q):ap rec 𝕀(a,b,q)(p)= f(0)= Af(1)β 𝕀 0(a,b,q)qβ 𝕀 p(a,b,q) 1\beta_\mathbb{I}^p(a, b, q):\mathrm{ap}_{\mathrm{rec}_{\mathbb{I}}(a, b, q)}(p) =_{f(0) =_A f(1)} \beta_\mathbb{I}^0(a, b, q) \bullet q \bullet \beta_\mathbb{I}^p(a, b, q)^{-1}

where

ap rec 𝕀(a,b,q):(0= 𝕀1)(f(0)= Af(1))\mathrm{ap}_{\mathrm{rec}_{\mathbb{I}}(a, b, q)}:(0 =_\mathbb{I} 1) \to (f(0) =_A f(1))

is the function application to identities,

()():(a= Ab)×(b= Ac)(a= Ac)(-)\bullet(-):(a =_A b) \times (b =_A c) \to (a =_A c)

is concatenation of identities (i.e. transitivity), and

() 1:(a= Ab)(b= Aa)(-)^{-1}:(a =_A b) \to (b =_A a)

is the inverse of identities (i.e. symmetry).

Theorem

Given a path q:𝕀Aq:\mathbb{I} \to A and terms a:Aa:A and b:Ab:A with identities δ a:q(0)= Aa\delta_a:q(0) =_A a and δ b:q(1)= Ab\delta_b:q(1) =_A b, there is an identity

δ a 1ap q(p)δ b:a= Ab\delta_a^{-1} \bullet \mathrm{ap}_{q}(p) \bullet \delta_b:a =_{A} b

The path version of reflexivity of an element x:Ax:A is represented by the constant function λi:𝕀.x:𝕀A\lambda i:\mathbb{I}.x:\mathbb{I} \to A. By definition of function application to identifications, one has

ap λi:𝕀.x(i,j,q)refl A(x)\mathrm{ap}_{\lambda i:\mathbb{I}.x}(i, j, q) \equiv \mathrm{refl}_A(x)

for all i,j:𝕀i, j:\mathbb{I} and q:i= 𝕀jq:i =_\mathbb{I} j.

This allows us to posit versions of path induction using functions from the interval type, which states that:

Theorem

Given a type AA, a type family C(z)C(z) indexed by z:𝕀Az:\mathbb{I} \to A, and a family of elements t: x:AC(λi:𝕀.x)t:\prod_{x:A} C(\lambda i:\mathbb{I}.x), one could construct a dependent function f(t): z:𝕀AC(z)f(t):\prod_{z:\mathbb{I} \to A} C(z) such that f(t,λi:𝕀.x)t:C(λi:𝕀.x)f(t, \lambda i:\mathbb{I}.x) \equiv t:C(\lambda i:\mathbb{I}.x).

ΓAtypeΓ,z:𝕀AC(z)t: x:AC(λi:𝕀.x)Γind 𝕀A(t): z:𝕀AC(z)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, z:\mathbb{I} \to A \vdash C(z) \quad t:\prod_{x:A} C(\lambda i:\mathbb{I}.x)}{\Gamma \vdash \mathrm{ind}_{\mathbb{I} \to A}(t):\prod_{z:\mathbb{I} \to A} C(z)}
ΓAtypeΓ,z:𝕀AC(z)t: x:AC(λi:𝕀.x)Γ,x:Aind 𝕀A(t,λi:𝕀.x)t:C(λi:𝕀.x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, z:\mathbb{I} \to A \vdash C(z) \quad t:\prod_{x:A} C(\lambda i:\mathbb{I}.x)}{\Gamma, x:A \vdash \mathrm{ind}_{\mathbb{I} \to A}(t, \lambda i:\mathbb{I}.x) \equiv t:C(\lambda i:\mathbb{I}.x)}

The alternate induction principle of the path type, which uses functions into the path type rather than families indexed by the path type, is given by:

Theorem

Given any type CC and function f:C(𝕀A)f:C \to (\mathbb{I} \to A) into the path type in AA, and given a function c:ACc:A \to C and a homotopy

p: x:Af(c(x))= 𝕀Aλi:𝕀.xp:\prod_{x:A} f(c(x)) =_{\mathbb{I} \to A} \lambda i:\mathbb{I}.x

which states that the composite of ff and cc is the canonical function which takes elements of AA to constant paths into AA, one can construct a function g:(𝕀A)Cg:\left(\mathbb{I} \to A\right) \to C and a homotopy witnessing that gg is a section of ff:

sec g: z:𝕀Af(g(z))= 𝕀Az\mathrm{sec}_g:\prod_{z:\mathbb{I} \to A} f(g(z)) =_{\mathbb{I} \to A} z

such that for all x:Ax:A, g(λi:𝕀.x)c(x)g(\lambda i:\mathbb{I}.x) \equiv c(x) and sec g(λi:𝕀.x)p(x)\mathrm{sec}_g(\lambda i:\mathbb{I}.x) \equiv p(x).

elimination rules for path induction:

ΓAtypeΓCtypeΓf:C(𝕀A) Γc:ACΓp: x:Af(c(x))= 𝕀Aλi:𝕀.x Γ,z:𝕀Aind 𝕀A C(f,c,p,z):C\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to (\mathbb{I} \to A) \\ \Gamma \vdash c:A \to C \quad \Gamma \vdash p:\prod_{x:A} f(c(x)) =_{\mathbb{I} \to A} \lambda i:\mathbb{I}.x \\ \end{array} }{\Gamma, z:\mathbb{I} \to A \vdash \mathrm{ind}_{\mathbb{I} \to A}^{C}(f, c, p, z):C}
ΓAtypeΓCtypeΓf:C(𝕀A) Γc:ACΓp: x:Af(c(x))= 𝕀Aλi:𝕀.x Γ,z:𝕀Aindsec Unit C(f,c,p,z):f(ind Unit C(f,c,p,z))= 𝕀Az\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to (\mathbb{I} \to A) \\ \Gamma \vdash c:A \to C \quad \Gamma \vdash p:\prod_{x:A} f(c(x)) =_{\mathbb{I} \to A} \lambda i:\mathbb{I}.x \\ \end{array} }{\Gamma, z:\mathbb{I} \to A \vdash \mathrm{indsec}_\mathrm{Unit}^{C}(f, c, p, z):f(\mathrm{ind}_\mathrm{Unit}^{C}(f, c, p, z)) =_{\mathbb{I} \to A} z}

computation rules for path induction:

ΓAtypeΓCtypeΓf:C(𝕀A) Γc:ACΓp: x:Af(c(x))= 𝕀Aλi:𝕀.x Γ,x:Aind 𝕀A C(f,c,p,λi:𝕀.x)c(x):C\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to (\mathbb{I} \to A) \\ \Gamma \vdash c:A \to C \quad \Gamma \vdash p:\prod_{x:A} f(c(x)) =_{\mathbb{I} \to A} \lambda i:\mathbb{I}.x \\ \end{array} }{\Gamma, x:A \vdash \mathrm{ind}_{\mathbb{I} \to A}^{C}(f, c, p, \lambda i:\mathbb{I}.x) \equiv c(x):C}
ΓAtypeΓCtypeΓf:C(𝕀A) Γc:ACΓp: x:Af(c(x))= 𝕀Aλi:𝕀.x Γ,x:Aindsec 𝕀A C(f,c,p,λi:𝕀.x)p(x):f(ind 𝕀A C(f,c,p,z))= 𝕀Az\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to (\mathbb{I} \to A) \\ \Gamma \vdash c:A \to C \quad \Gamma \vdash p:\prod_{x:A} f(c(x)) =_{\mathbb{I} \to A} \lambda i:\mathbb{I}.x \\ \end{array} }{\Gamma, x:A \vdash \mathrm{indsec}_{\mathbb{I} \to A}^{C}(f, c, p, \lambda i:\mathbb{I}.x) \equiv p(x):f(\mathrm{ind}_{\mathbb{I} \to A}^{C}(f, c, p, z)) =_{\mathbb{I} \to A} z}

Theorem

Suppose that path induction for function types out of the interval type is true.

Then the J-rule is true: given a type AA and given a type family C(x,y,p)C(x, y, p) indexed by x:Ax:A, y:Ay:A, and p:x= Ayp:x =_A y, and a dependent function t: x:AC(x,x,refl A(x))t:\prod_{x:A} C(x, x, \mathrm{refl}_A(x)), one can construct a dependent function

ind =,A(t): x:A y:A p:x= AyC(x,y,p)\mathrm{ind}_{=, A}(t):\prod_{x:A} \prod_{y:A} \prod_{p:x =_A y} C(x, y, p)

such that for all x:Ax:A,

J(t,x,x,refl A(x))t(x)J(t, x, x, \mathrm{refl}_A(x)) \equiv t(x)

Proof

By path induction on the type family C(f(0),f(1),toId A(f))C(f(0), f(1), \mathrm{toId}_A(f)) indexed by f:𝕀Af:\mathbb{I} \to A, we can construct a dependent function

ind 𝕀A(t): f:𝕀AC(f(0),f(1),toId A(f))\mathrm{ind}_{\mathbb{I} \to A}(t):\prod_{f:\mathbb{I} \to A} C(f(0), f(1), \mathrm{toId}_A(f))

such that for all x:Ax:A,

ind 𝕀A(t,λi:𝕀.x)t(x):C(λi:𝕀.x)\mathrm{ind}_{\mathbb{I} \to A}(t, \lambda i:\mathbb{I}.x) \equiv t(x):C(\lambda i:\mathbb{I}.x)

since by definition of constant function and reflexivity, one has

(λi:𝕀.x)(0)x(λi:𝕀.x)(1)xap λi:𝕀.x(𝓅)refl A(x)(\lambda i:\mathbb{I}.x)(0) \equiv x \quad (\lambda i:\mathbb{I}.x)(1) \equiv x \quad \mathrm{ap}_{\lambda i:\mathbb{I}.x}(\mathcal{p}) \equiv \mathrm{refl}_A(x)

We define

J(t,x,y,p)ind 𝕀A(t,rec 𝕀 A(x,y,p))J(t, x, y, p) \equiv \mathrm{ind}_{\mathbb{I} \to A}(t, \mathrm{rec}_\mathbb{I}^A(x, y, p))

since by interval recursion one has a path rec 𝕀 A(x,y,p):𝕀A\mathrm{rec}_\mathbb{I}^A(x, y, p):\mathbb{I} \to A such that

rec 𝕀 A(x,y,p)(0)xrec 𝕀 A(x,y,p)(1)yap rec 𝕀 A(x,y,p)(0,1,𝓅)p\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)(0) \equiv x \quad \mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)(1) \equiv y \quad \mathrm{ap}_{\mathrm{rec}_\mathbb{I}^{A}(x, y, p)}(0, 1, \mathcal{p}) \equiv p

Relation to dependent identity types

Given a type AA, a dependent type x:AB(x)x:A \vdash B(x), terms a 0:Aa_0:A and a 1:Aa_1:A, identity q:a 0= Aa 1q:a_0 =_A a_1, terms b 0:B(a 0)b_0:B(a_0) and b 1:B(a 1)b_1:B(a_1), and dependent identity r:b 0= B qb 1r:b_0 =_B^q b_1, let us inductively define the family of elements x:𝕀f(x):B(x)x:\mathbb{I} \vdash f(x):B(x) by

  • β f 0:f(0)= B(a 0)b 0\beta_f^0:f(0) =_{B(a_0)} b_0
  • β f 1:f(1)= B(a 1)b 1\beta_f^1:f(1) =_{B(a_1)} b_1
  • β f p:apd f(p)= f(0)= B qf(1)concat trans B q(f(0)),b 1,f(1)(concat trans B q(f(0)),trans B q(b 0),b 1(apd trans B q(β f 0),r),inv f(1),b(β f 1))\beta_f^p:\mathrm{apd}_f(p) =_{f(0) =_B^q f(1)} \mathrm{concat}_{\mathrm{trans}_B^q(f(0)), b_1, f(1)}(\mathrm{concat}_{\mathrm{trans}_B^q(f(0)), \mathrm{trans}_B^q(b_0), b_1}(\mathrm{apd}_{\mathrm{trans}_B^q}(\beta_f^0), r), \mathrm{inv}_{f(1), b}(\beta_f^1))

where trans B q:B(a 0)B(a 1)\mathrm{trans}_B^q:B(a_0) \to B(a_1) is transport, ap f:(0= 𝕀1)(f(0)= Af(1))\mathrm{ap}_f:(0 =_\mathbb{I} 1) \to (f(0) =_A f(1)) is the function application to identities, concat a,b,c:(a= Ab)×(b= Ac)(a= Ac)\mathrm{concat}_{a, b, c}:(a =_A b) \times (b =_A c) \to (a =_A c) is concatenation of identities (i.e. transitivity), and inv a,b:(a= Ab)(b= Aa)\mathrm{inv}_{a, b}:(a =_A b) \to (b =_A a) is the inverse of identities (i.e. symmetry).

Let AA and BB be types, and let e:ABe:A \simeq B be an equivalence between AA and BB. Then there is a type family x:𝕀C(x)typex:\mathbb{I} \vdash C(x) \; \mathrm{type} defined by C(0)AC(0) \coloneqq A, C(1)BC(1) \coloneqq B, and trans C pe:AB\mathrm{trans}_C^p \coloneqq e:A \simeq B.

Relation to function extensionality

Postulating an interval type with judgmental computation rules for the point constructors of the interval type implies function extensionality. (Shulman).

The proof assumes a typal uniqueness rule for function types. First it constructs a function k:A(𝕀B)k:A \to (\mathbb{I} \to B) from a dependent function h: x:Af(x)= Bg(x)h:\prod_{x:A} f(x) =_B g(x), inductively defined by

  • β k(x) 0:k(x)(0)= Bf(x)\beta_{k(x)}^0:k(x)(0) =_B f(x)
  • β k(x) 1:k(x)(1)= Bg(x)\beta_{k(x)}^1:k(x)(1) =_B g(x)
  • β k(x) p:ap k(x)(p)= k(x)(0)= Bk(x)(1)β k(x) 0h(x)(β k(x) 1) 1\beta_{k(x)}^p:\mathrm{ap}_{k(x)}(p) =_{k(x)(0) =_B k(x)(1)} \beta_{k(x)}^0 \bullet h(x) \bullet (\beta_{k(x)}^1)^{-1}

Then it uses the properties of function types, product types, currying, uncurrying, and the symmetry of products A×BB×AA \times B \simeq B \times A, to construct a function k:𝕀(AB)k':\mathbb{I} \to (A \to B), inductively defined by

  • β k 0(x):k(0)(x)= Bf(x)\beta_{k'}^0(x):k'(0)(x) =_B f(x)
  • β k 1(x):k(1)(x)= Bg(x)\beta_{k'}^1(x):k'(1)(x) =_B g(x)
  • β k p(x):ap k(p)(x)= k(0)(x)= Bk(1)(x)β k 0(x)h(x)(β k 1(x)) 1)\beta_{k'}^p(x):\mathrm{ap}_{k'}(p)(x) =_{k'(0)(x) =_B k'(1)(x)} \beta_{k'}^0(x) \bullet h(x) \bullet (\beta_{k'}^1(x))^{-1})

If the interval type has judgmental computation rules for the point constructors, then k(x)(0)f(x)k'(x)(0) \equiv f(x) and k(x)(1)g(x)k'(x)(1) \equiv g(x) for all x:Ax:A, which implies that k(0)(x)f(x)k'(0)(x) \equiv f(x) and k(1)(x)g(x)k'(1)(x) \equiv g(x) for all x:Ax:A, and subsequently that k(0)fk'(0) \equiv f and k(1)gk'(1) \equiv g. This means that there are identities β k 0:k(0)= ABf\beta_{k'}^0:k'(0) =_{A \to B} f and β k 1:k(1)= ABg\beta_{k'}^1:k'(1) =_{A \to B} g, and an identity

(β k 0) 1ap k(p)β k 1:f= ABg(\beta_{k'}^0)^{-1} \bullet \mathrm{ap}_{k'}(p) \bullet \beta_{k'}^1:f =_{A \to B} g

thus proving function extensionality.

An interval type with only typal computation rules for the point constructors does not imply function extensionality. This is because the proof with the judgmental computation rules uses the fact that k(0)(x)f(x)k'(0)(x) \equiv f(x) and k(1)(x)g(x)k'(1)(x) \equiv g(x) for all x:Ax:A implies that k(0)fk'(0) \equiv f and k(1)gk'(1) \equiv g. However, if the computation rules are typal, then the equivalent statement is that having identities β k 0(x):k(0)(x)= Bf(x)\beta_{k'}^0(x):k'(0)(x) =_B f(x) and β k 1(x):k(1)(x)= Bg(x)\beta_{k'}^1(x):k'(1)(x) =_B g(x) for all x:Ax:A implies that there are identities β k 0:k(0)= ABf\beta_{k'}^0:k'(0) =_{A \to B} f and β k 1:k(1)= ABg\beta_{k'}^1:k'(1) =_{A \to B} g, which is precisely function extensionality, and so cannot be used to prove function extensionality.

 Relation to propositional truncations

An interval type is the propositional truncation of the boolean domain 𝟚\mathbb{2}. We use the definition of an interval type using a function from 𝟚\mathbb{2}. Since the interval type has identities

  • refl 𝕀(j(0)):j(0)= 𝕀j(0)\mathrm{refl}_\mathbb{I}(j(0)):j(0) =_\mathbb{I} j(0),
  • p:j(0)= 𝕀j(1)p:j(0) =_\mathbb{I} j(1),
  • inv j(0),j(1)(p):j(1)= 𝕀j(0)\mathrm{inv}_{j(0), j(1)}(p):j(1) =_\mathbb{I} j(0),
  • refl 𝕀(j(1)):j(1)= 𝕀j(1)\mathrm{refl}_\mathbb{I}(j(1)):j(1) =_\mathbb{I} j(1),

there is a dependent function

f: a:𝟚 b:𝟚j(a)= 𝕀j(b)f:\prod_{a:\mathbb{2}} \prod_{b:\mathbb{2}} j(a) =_\mathbb{I} j(b)

inductively defined by the identities

β f(0,0):f(0)(0)= j(0)= 𝕀j(0)refl 𝕀(j(0))\beta_{f}(0, 0):f(0)(0) =_{j(0) =_\mathbb{I} j(0)} \mathrm{refl}_\mathbb{I}(j(0))
β f(0,1):f(0)(1)= j(0)= 𝕀j(1)p\beta_{f}(0, 1):f(0)(1) =_{j(0) =_\mathbb{I} j(1)} p
β f(1,0):f(1)(0)= j(1)= 𝕀j(0)inv j(0),j(1)(p)\beta_{f}(1, 0):f(1)(0) =_{j(1) =_\mathbb{I} j(0)} \mathrm{inv}_{j(0), j(1)}(p)
β f(1,1):f(1)(1)= j(1)= 𝕀j(1)refl 𝕀(j(1))\beta_{f}(1, 1):f(1)(1) =_{j(1) =_\mathbb{I} j(1)} \mathrm{refl}_\mathbb{I}(j(1))

If dependent product types have judgmental computation rules, then the above becomes

f(0)(0)refl 𝕀(j(0)):j(0)= 𝕀j(0)f(0)(0) \equiv \mathrm{refl}_\mathbb{I}(j(0)):j(0) =_\mathbb{I} j(0)
f(0)(1)p:j(0)= 𝕀j(1)f(0)(1) \equiv p:j(0) =_\mathbb{I} j(1)
f(1)(0)inv j(0),j(1)(p):j(1)= 𝕀j(0)f(1)(0) \equiv \mathrm{inv}_{j(0), j(1)}(p):j(1) =_\mathbb{I} j(0)
f(1)(1)refl 𝕀(j(1)):j(1)= 𝕀j(1)f(1)(1) \equiv \mathrm{refl}_\mathbb{I}(j(1)):j(1) =_\mathbb{I} j(1)

Both show that the interval type is the propositional truncation of the boolean domain.

The converse is true as well: the propositional truncation of the boolean domain is the interval type. Recall that [𝟚]\left[\mathbb{2}\right] is inductively generated by a function j:𝟚[𝟚]j:\mathbb{2} \to \left[\mathbb{2}\right] and a dependent function

f: a:𝟚 b:𝟚j(a)= [𝟚]j(b)f:\prod_{a:\mathbb{2}} \prod_{b:\mathbb{2}} j(a) =_{\left[\mathbb{2}\right]} j(b)

which makes [𝟚]\left[\mathbb{2}\right] into an h-proposition. By definition of an h-proposition, for each element a:𝟚a:\mathbb{2} and b:𝟚b:\mathbb{2}, the identity type j(a)= [𝟚]j(b)j(a) =_{\left[\mathbb{2}\right]} j(b) is a contractible type. In particular, by induction on 𝟚\mathbb{2}, this means that there are identities

β f(0,0):f(0)(0)= j(0)= [𝟚]j(0)refl [𝟚](j(0))\beta_{f}(0, 0):f(0)(0) =_{j(0) =_{\left[\mathbb{2}\right]} j(0)} \mathrm{refl}_{\left[\mathbb{2}\right]}(j(0))
β f(1,1):f(1)(1)= j(1)= [𝟚]j(1)refl [𝟚](j(1))\beta_{f}(1, 1):f(1)(1) =_{j(1) =_{\left[\mathbb{2}\right]} j(1)} \mathrm{refl}_{\left[\mathbb{2}\right]}(j(1))

and for every identity p:0= [𝟚]1p:0 =_{\left[\mathbb{2}\right]} 1, there are identities

β f(0,1):f(0)(1)= j(0)= [𝟚]j(1)p\beta_{f}(0, 1):f(0)(1) =_{j(0) =_{\left[\mathbb{2}\right]} j(1)} p
β f(1,0):f(1)(0)= j(1)= [𝟚]j(0)inv j(0),j(1)(p)\beta_{f}(1, 0):f(1)(0) =_{j(1) =_{\left[\mathbb{2}\right]} j(0)} \mathrm{inv}_{j(0), j(1)}(p)

Thus, one could simply take j(0)j(0) and j(1)j(1) as the term constructors and f(0)(1)f(0)(1) as the identity constructor of the interval type.

If both propositional truncations and the boolean domain have judgmental computation rules, the the interval type also has judgmental computation rules. See (this file)

References

Proofs of function extensionality using an interval type with judgmental computation rules for point constructors could be found here

  • Carlo Angiuli, Univalence implies function extensionality (blog, pdf)

Last revised on December 31, 2023 at 20:56:34. See the history of this page for a list of all contributions to it.