nLab interval type localization

Contents

Idea

The principle of interval type localization states that for all types AA, AA is 𝕀\mathbb{I}-local, or equivalently that the function

const A,𝕀≑λx:A.Ξ»i:mathbbI.x:Aβ†’(𝕀→A)\mathrm{const}_{A, \mathbb{I}} \equiv \lambda x:A.\lambda i:mathbb{I}.x:A \to (\mathbb{I} \to A)

is an equivalence of types.

There is also a definitional interval type localization which says that the function

const A,𝕀≑λx:A.Ξ»i:mathbbI.x:Aβ†’(𝕀→A)\mathrm{const}_{A, \mathbb{I}} \equiv \lambda x:A.\lambda i:mathbb{I}.x:A \to (\mathbb{I} \to A)

is a definitional isomorphism. The usual notion of interval type localization can be called propositional interval type localization.

One has the following analogies between localization at a specific type and the type theoretic letter rule that it proves:

localization ruletype theoretic letter rule
𝕀 \mathbb{I} -localizationJ-rule
S 1 S^1 -localizationK-rule

Axiom of interval type localization

In Martin-LΓΆf type theory, interval type localization is a provable statement from the J-rule and the recursion principle of the interval type. However, in other dependent type theories where identity types are defined in terms of the interval type, interval type localization can be added as a separate axiom to the type theory as an alternative to the J-rule, because it implies the J-rule.

Suppose that one has an interval type 𝕀\mathbb{I}, with elements 0:𝕀0:\mathbb{I} and 1:𝕀1:\mathbb{I}.

Ξ“ctxΞ“βŠ’π•€type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{I} \; \mathrm{type}}
Ξ“ctxΞ“βŠ’0:𝕀ΓctxΞ“βŠ’1:𝕀\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{I}} \quad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 1:\mathbb{I}}

Usually, the recursion principle of the interval type is interpreted as a way to construct, from elements x:Ax:A and y:Ay:A and identification p:x= Ayp:x =_A y, paths p:𝕀→Ap:\mathbb{I} \to A, aka functions from the interval type to AA. Interpreted another way, the recursion principle of the interval type are the negative elimination and computation rules for identity types, allowing one to define identity types as negative types.

  • The formation rule of identity types state that given a type AA and elements x:Ax:A and y:Ay:A, one can form the identity type x= Ayx =_A y. Syntactically, this is given by the following inference rules:
Ξ“βŠ’AtypeΞ“,x:A,y:A⊒x= Aytype\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A, y:A \vdash x =_A y \; \mathrm{type}}
  • The introduction rule of identity types state that given a type AA and a path p:𝕀→Ap:\mathbb{I} \to A, one can construct an identification toId A(f):f(0)= Af(1)\mathrm{toId}_A(f):f(0) =_A f(1). Syntactically, this is given by the following inference rules:
Ξ“βŠ’AtypeΞ“βŠ’f:𝕀→AΞ“βŠ’toId A(f):f(0)= Af(1)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash f:\mathbb{I} \to A}{\Gamma \vdash \mathrm{toId}_A(f):f(0) =_A f(1)}

Normally, this would be function application to the canonical identification 𝓅:0= 𝕀1\mathcal{p}:0 =_\mathbb{I} 1, but here we haven’t defined 𝓅\mathcal{p} yet since we haven’t defined the identity type yet, and with this rule one can define said identification to be the identification of the identity function on the interval type

𝓅≑toId 𝕀(id 𝕀):0= 𝕀1\mathcal{p} \equiv \mathrm{toId}_\mathbb{I}(\mathrm{id}_\mathbb{I}):0 =_\mathbb{I} 1

In addition, reflexivity of an element x:Ax:A is given by sending the constant path of x:Ax:A to its equality

refl A(x)≑toId A(Ξ»i:𝕀.x):x= Ax\mathrm{refl}_A(x) \equiv \mathrm{toId}_{A}(\lambda i:\mathbb{I}.x):x =_A x
  • The elimination rule of identity types state that given a type AA, elements x:Ax:A and y:Ay:A, and identification p:x= Ayp:x =_A y, one can construct a path topath 𝕀 A(x,y,p):𝕀→A\mathrm{topath}_\mathbb{I}^A(x, y, p):\mathbb{I} \to A. Syntactically, this is given by the following inference rules:
Ξ“βŠ’AtypeΞ“βŠ’x:AΞ“βŠ’y:AΞ“βŠ’p:x= AyΞ“βŠ’topath 𝕀 A(x,y,p):𝕀→A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:A \quad \Gamma \vdash y:A \quad \Gamma \vdash p:x =_A y}{\Gamma \vdash \mathrm{topath}_\mathbb{I}^A(x, y, p):\mathbb{I} \to A}

This is just another name for the recursor of the interval type rec 𝕀 A(x,y,p)≑topath 𝕀 A(x,y,p):𝕀→A\mathrm{rec}_\mathbb{I}^A(x, y, p) \equiv \mathrm{topath}_\mathbb{I}^A(x, y, p):\mathbb{I} \to A.

  • The three computation rules of identity types state that given a type AA, elements x:Ax:A and y:Ay:A, and identification p:x= Ayp:x =_A y,
    topath 𝕀 A(x,y,p)(0)≑xtopath 𝕀 A(x,y,p)(1)≑ytoId A(topath 𝕀 A(x,y,p))≑p\mathrm{topath}_\mathbb{I}^A(x, y, p)(0) \equiv x \quad \mathrm{topath}_\mathbb{I}^A(x, y, p)(1) \equiv y \quad \mathrm{toId}_{A}(\mathrm{topath}_\mathbb{I}^A(x, y, p)) \equiv p

    Syntactically, this is given by the following inference rules:

Ξ“βŠ’AtypeΞ“βŠ’x:AΞ“βŠ’y:AΞ“βŠ’p:x= AyΞ“βŠ’topath 𝕀 A(x,y,p)(0)≑x:A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:A \quad \Gamma \vdash y:A \quad \Gamma \vdash p:x =_A y}{\Gamma \vdash \mathrm{topath}_\mathbb{I}^A(x, y, p)(0) \equiv x:A}
Ξ“βŠ’AtypeΞ“βŠ’x:AΞ“βŠ’y:AΞ“βŠ’p:x= AyΞ“βŠ’topath 𝕀 A(x,y,p)(1)≑y:A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:A \quad \Gamma \vdash y:A \quad \Gamma \vdash p:x =_A y}{\Gamma \vdash \mathrm{topath}_\mathbb{I}^A(x, y, p)(1) \equiv y:A}
Ξ“βŠ’AtypeΞ“βŠ’x:AΞ“βŠ’y:AΞ“βŠ’p:x= AyΞ“βŠ’toId A(topath 𝕀 A(x,y,p))≑p:x= Ay\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:A \quad \Gamma \vdash y:A \quad \Gamma \vdash p:x =_A y}{\Gamma \vdash \mathrm{toId}_{A}(\mathrm{topath}_\mathbb{I}^A(x, y, p)) \equiv p:x =_A y}
  • The uniqueness rule of identity types state that given a type AA and a path p:𝕀→Ap:\mathbb{I} \to A,
    topath 𝕀 A(p(0),p(1),toId A(p))≑p\mathrm{topath}_\mathbb{I}^A(p(0), p(1), \mathrm{toId}_A(p)) \equiv p

Syntactically, this is given by the following inference rules:

Ξ“βŠ’AtypeΞ“βŠ’f:𝕀→AΞ“βŠ’topath 𝕀 A(f(0),f(1),toId A(f))≑f:𝕀→A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash f:\mathbb{I} \to A}{\Gamma \vdash \mathrm{topath}_\mathbb{I}^A(f(0), f(1), \mathrm{toId}_A(f)) \equiv f:\mathbb{I} \to A}

Then I\mathrm{I}-localization is given by the following axiom:

∏ A:typeβˆ‘ g:(𝕀→A)β†’A(∏ x:Ag(Ξ»i:𝕀.x)= Ax)Γ—(∏ p:𝕀→AΞ»i:𝕀.g(p)= 𝕀→Ap)\prod_{A:\mathrm{type}} \sum_{g:(\mathbb{I} \to A) \to A} \left(\prod_{x:A} g(\lambda i:\mathbb{I}.x) =_A x\right) \times \left(\prod_{p:\mathbb{I} \to A} \lambda i:\mathbb{I}.g(p) =_{\mathbb{I} \to A} p\right)

While this states that const A,𝕀\mathrm{const}_{A, \mathbb{I}} is only a quasi-invertible function, it is well known that every quasi-invertible function can be made into a coherently invertible function by constructing a new section or retraction which satisfies a suitable family of naturality squares.

If the dependent type theory does not have type universes, then the axiom of I\mathrm{I}-localization needs to be expressed as an inference rule:

Ξ“βŠ’AtypeΞ“βŠ’βˆ‘ g:(𝕀→A)β†’A(∏ x:Ag(Ξ»i:𝕀.x)= Ax)Γ—(∏ p:𝕀→AΞ»i:𝕀.g(p)= 𝕀→Ap)\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \sum_{g:(\mathbb{I} \to A) \to A} \left(\prod_{x:A} g(\lambda i:\mathbb{I}.x) =_A x\right) \times \left(\prod_{p:\mathbb{I} \to A} \lambda i:\mathbb{I}.g(p) =_{\mathbb{I} \to A} p\right)}

and if the dependent type theory does not have dependent sum types, then this would have to be expressed as three separate rules:

Ξ“βŠ’AtypeΞ“,p:𝕀→A⊒const A,I βˆ’1(p):A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, p:\mathbb{I} \to A \vdash \mathrm{const}_{A, \mathrm{I}}^{-1}(p):A}
Ξ“βŠ’AtypeΞ“,x:A⊒β 𝕀→A(x):const A,I βˆ’1(Ξ»i:𝕀.x)= Ax\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A \vdash \beta_{\mathbb{I} \to A}(x):\mathrm{const}_{A, \mathrm{I}}^{-1}(\lambda i:\mathbb{I}.x) =_{A} x}
Ξ“βŠ’AtypeΞ“,p:𝕀→A⊒η 𝕀→A(p):Ξ»i:𝕀.const A,I βˆ’1(p)= 𝕀→Ap\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, p:\mathbb{I} \to A \vdash \eta_{\mathbb{I} \to A}(p):\lambda i:\mathbb{I}.\mathrm{const}_{A, \mathrm{I}}^{-1}(p) =_{\mathbb{I} \to A} p}

Definitional I\mathrm{I}-localization is given by the following rules:

Ξ“βŠ’AtypeΞ“,p:𝕀→A⊒const A,I βˆ’1(p):A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, p:\mathbb{I} \to A \vdash \mathrm{const}_{A, \mathrm{I}}^{-1}(p):A}
Ξ“βŠ’AtypeΞ“,x:A⊒const A,I βˆ’1(Ξ»i:𝕀.x)≑x:A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A \vdash \mathrm{const}_{A, \mathrm{I}}^{-1}(\lambda i:\mathbb{I}.x) \equiv x:A}
Ξ“βŠ’AtypeΞ“,p:𝕀→A⊒λi:𝕀.const A,I βˆ’1(p)≑p:𝕀→A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, p:\mathbb{I} \to A \vdash \lambda i:\mathbb{I}.\mathrm{const}_{A, \mathrm{I}}^{-1}(p) \equiv p:\mathbb{I} \to A}

This makes const A,𝕀\mathrm{const}_{A, \mathbb{I}} into a definitional isomorphism, which is always a coherently invertible function.

Interval type localization implies the J-rule

The function application to identifications can be defined without the use of path induction:

Theorem

Given types AA and BB, a a function f:A→Bf:A \to B, elements x:Ax:A and y:Ay:A and an identification p:x= Ayp:x =_A y, one can construct the identification ap f(x,y,p):f(x)= Bf(y)\mathrm{ap}_f(x, y, p):f(x) =_B f(y).

This is defined through the inference rules for identity types and function composition:

ap f(x,y,p)≑toId B(f∘rec 𝕀 A(x,y,p)):f(x)= Bf(y)\mathrm{ap}_f(x, y, p) \equiv \mathrm{toId}_B(f \circ \mathrm{rec}_\mathbb{I}^A(x, y, p)):f(x) =_B f(y)

Theorem

Suppose that every type AA is definitionally 𝕀\mathbb{I}-local.

Then path induction for function types out of the interval type holds: given any type AA, and any type family C(p)C(p) indexed by paths p:𝕀→Ap:\mathbb{I} \to A in AA, and given any dependent function t:∏ x:AC(Ξ»i:𝕀.x)t:\prod_{x:A} C(\lambda i:\mathbb{I}.x) which says that for all elements x:Ax:A, there is an element of the type defined by substituting the constant path of x:Ax:A into CC, C(Ξ»i:𝕀.x)C(\lambda i:\mathbb{I}.x), one can construct a dependent function ind 𝕀→A(t):∏ z:𝕀→AC(z)\mathrm{ind}_{\mathbb{I} \to A}(t):\prod_{z:\mathbb{I} \to A} C(z) 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).

Proof

ind 𝕀→A(t)\mathrm{ind}_{\mathbb{I} \to A}(t) is defined to be

ind 𝕀→A(t)≑λp:𝕀→A.t(const A,I βˆ’1(p))\mathrm{ind}_{\mathbb{I} \to A}(t) \equiv \lambda p:\mathbb{I} \to A.t(\mathrm{const}_{A, \mathrm{I}}^{-1}(p))

and by the computation rules of path types as negative copies, one has that for all x:Ax:A,

const A,I βˆ’1(Ξ»i:𝕀.x)≑x\mathrm{const}_{A, \mathrm{I}}^{-1}(\lambda i:\mathbb{I}.x) \equiv x

and so by definition of ind 𝕀→A(t)\mathrm{ind}_{\mathbb{I} \to A}(t) and the judgmental congruence rules for substitution, one has

ind 𝕀→A(t,Ξ»i:𝕀.x)≑t(const A,I βˆ’1(Ξ»i:𝕀.x))≑t(x)\mathrm{ind}_{\mathbb{I} \to A}(t, \lambda i:\mathbb{I}.x) \equiv t(\mathrm{const}_{A, \mathrm{I}}^{-1}(\lambda i:\mathbb{I}.x)) \equiv t(x)

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

Last revised on May 17, 2024 at 12:34:46. See the history of this page for a list of all contributions to it.