Homotopy Type Theory higher observational type theory > history (changes)

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

Showing changes from revision #15 to #16: Added | Removed | Changed

Contents

< higher observational type theory

category: redirected to nlab

Idea

Higher observational type theory involves a different definition of identity types where the identity types are defined recursively for each type former rather than uniformly across all types in intensional Martin-Loef type theory.

ap is a primitive in higher observational type theory, rather than being derived from path induction? of path types as in intensional Martin-Loef type theory.

Definitions

We are working in a dependent type theory.

Telescopes

Telescopes represent lists of terms in the context.

Rules for the empty telescope
ϵtel\frac{}{\epsilon\ \mathrm{tel}}

Rules for telescopes given a telescope and a type
ΔtelΔ⊢Atype(Δ,x:A)tel\frac{\Delta\ \mathrm{tel} \quad \Delta \vdash A \mathrm{type}}{(\Delta,x:A)\ \mathrm{tel}}

Rules for the empty context in a telescope
():ϵ\frac{}{():\epsilon}

Rules for …
δ:ΔΔ⊢Atypea:A[δ](δ,a):(Δ,x:A)\frac{\delta:\Delta \quad \Delta \vdash A \mathrm{type} \quad a:A[\delta]}{(\delta,a):(\Delta,x:A)}

…
Δ⊢a:Aδ:Δa[δ]:A[δ]\frac{\Delta \vdash a:A \quad \delta:\Delta}{a[\delta]:A[\delta]}

Identity telescopes
Δtelδ:Δδ ′:Δδ= Δδ ′tel\frac{\Delta\ \mathrm{tel} \quad \delta:\Delta \quad \delta^{'}:\Delta}{\delta =_\Delta \delta^{'}\ \mathrm{tel}}

…
()= ϵ()≡ϵ() =_\epsilon () \equiv \epsilon

…
(δ,a)= Δ,x:A(δ ′,a ′)≡(ς:δ= Δδ ′,α:a= Δ.A ςa ′)(\delta,a) =_{\Delta,x:A} (\delta^{'},a^{'}) \equiv \left(\varsigma:\delta =_\Delta \delta^{'}, \alpha:a =_{\Delta.A}^\varsigma a^{'}\right)

Dependent identity types
ς:δ= Δδ ′δ⊢Atypea:A[δ]a ′:A[δ ′]a= Δ.A ςa ′type\frac{\varsigma:\delta =_\Delta \delta^{'} \quad \delta \vdash A\ \mathrm{type} \quad a:A[\delta] \quad a^{'}:A[\delta^{'}]}{a =_{\Delta.A}^\varsigma a^{'}\ \mathrm{type}}

The identity types in higher observational type theory is defined as
a= Aa ′≡a= ϵ.A ()a ′a =_A a^{'} \equiv a =_{\epsilon.A}^{()} a^{'}

Computation rules are defend for pair types:
(s= A×B ςt)≡(π 1(s)= A ςπ 1(t))×(π 2(s)= B ςπ 2(t))(s =_{A \times B}^\varsigma t) \equiv (\pi_1(s) =_A^\varsigma \pi_1(t)) \times (\pi_2(s) =_B^\varsigma \pi_2(t))

Computation rules are defined for function types:
(f= A→B ςg)≡∏ a:A∏ b:A∏ q:(a= Ab)(f(a)= B ςg(b))(f =_{A \to B}^\varsigma g) \equiv \prod_{a:A} \prod_{b:A} \prod_{q:(a =_A b)} (f(a) =_B^\varsigma g(b))

Computation rules are defend for dependent pair types:
(s= ∑ x:AB(x) ςt)≡∑ p:(π 1(s)= A ςπ 1(t))(π 2(s)= B ς,pπ 2(t))(s =_{\sum_{x:A} B(x)}^\varsigma t) \equiv \sum_{p:(\pi_1(s) =_A^\varsigma \pi_1(t))} (\pi_2(s) =_{B}^{\varsigma,p} \pi_2(t))

Computation rules are defend for dependent pair types:
(f= ∏ x:AB(x) ςg)≡∏ a:A∏ b:A∏ p:(a= A ςb)(f(a)= B ς,pg(b))(f =_{\prod_{x:A} B(x)}^\varsigma g) \equiv \prod_{a:A} \prod_{b:A} \prod_{p:(a =_{A}^\varsigma b)} (f(a) =_{B}^{\varsigma,p} g(b))

Dependent Ap

…

With universes

We are working in a dependent type theory with Tarski-style universes.

The identity types in a universe in higher observational type theory have the following formation rule:
A:𝒰a:𝒯 𝒰(A)b:𝒯 𝒰(A)id A(a,b):𝒰\frac{A:\mathcal{U} \quad a:\mathcal{T}_\mathcal{U}(A) \quad b:\mathcal{T}_\mathcal{U}(A)}{\mathrm{id}_A(a, b):\mathcal{U}}

We define a general congruence term called ap
x:A⊢f:Bp:id A(a,a ′)ap x.f(p):id B(f[a/x],f[a ′/x])\frac{x:A \vdash f:B \quad p:\mathrm{id}_A(a, a^{'})}{\mathrm{ap}_{x.f}(p):\mathrm{id}_B(f[a/x], f[a^{'}/x])}

and the reflexivity terms:
a:Arefl a:id A(a,a)\frac{a:A}{\mathrm{refl}_{a}:\mathrm{id}_A(a, a)}

and computation rules for identity functions
ap x.x(p)≡p\mathrm{ap}_{x.x}(p) \equiv p

and for constant functions yy
ap x.y(p)≡refl y\mathrm{ap}_{x.y}(p) \equiv \mathrm{refl}_{y}

Thus, ap is a higher dimensional explicit substitution. There are definitional equalities
ap x.f(refl a)≡refl f[a/x]\mathrm{ap}_{x.f}(\mathrm{refl}_{a}) \equiv \mathrm{refl}_{f[a/x]}
ap y.g(ap x.f(p))≡ap x.g[f/y](p)\mathrm{ap}_{y.g}(\mathrm{ap}_{x.f}(p)) \equiv \mathrm{ap}_{x.g[f/y]}(p)
ap x.t(p)≡refl t\mathrm{ap}_{x.t}(p) \equiv \mathrm{refl}_{t}

for constant term tt.

Identity types for universes

Let A≅ 𝒰BA \cong_\mathcal{U} B be the type of bijective correspondences between two terms of a universe A:𝒰A:\mathcal{U} and B:𝒰B:\mathcal{U}, and let id 𝒰(A,B)\mathrm{id}_\mathcal{U}(A, B) be the identity type between two terms of a universe A:𝒰A:\mathcal{U} and B:𝒰B:\mathcal{U}. Then there are rules
R:A≅ 𝒰BΔ(R):id 𝒰(A,B)P:id 𝒰(A,B)∇(P):A≅ 𝒰BR:A≅ 𝒰B∇(Δ(R))≡R\frac{R:A \cong_\mathcal{U} B}{\Delta(R):\mathrm{id}_\mathcal{U}(A, B)} \qquad \frac{P:\mathrm{id}_\mathcal{U}(A, B)}{\nabla(P):A \cong_\mathcal{U} B} \qquad \frac{R:A \cong_\mathcal{U} B}{\nabla(\Delta(R)) \equiv R}

Identity types in universes and singleton contractibility

Given a term of a universe A:𝒰A:\mathcal{U}
id 𝒯 𝒰(A)≡π 1(∇(refl A))\mathrm{id}_{\mathcal{T}_\mathcal{U}(A)} \equiv \pi_1(\nabla(\mathrm{refl}_A))

with terms representing singleton contractibility.
π 1(π 2(∇(refl A)):∏ a:𝒯 𝒰(A)isContr(∑ b:𝒯 𝒰(A)id 𝒯 𝒰(A)(a,b))\pi_1(\pi_2(\nabla(\mathrm{refl}_A)):\prod_{a:\mathcal{T}_\mathcal{U}(A)} \mathrm{isContr}\left(\sum_{b:\mathcal{T}_\mathcal{U}(A)} \mathrm{id}_{\mathcal{T}_\mathcal{U}(A)}(a, b)\right)
π 2(π 2(∇(refl A))):∏ b:𝒯 𝒰(A)isContr(∑ a:𝒯 𝒰(A)id 𝒯 𝒰(A)(a,b))\pi_2(\pi_2(\nabla(\mathrm{refl}_A))):\prod_{b:\mathcal{T}_\mathcal{U}(A)} \mathrm{isContr}\left(\sum_{a:\mathcal{T}_\mathcal{U}(A)} \mathrm{id}_{\mathcal{T}_\mathcal{U}(A)}(a, b)\right)

Dependent identity types in universes

Given a term of a universe A:𝒰A:\mathcal{U}, a judgment z:𝒯 𝒰(A)⊢B:𝒰z:\mathcal{T}_\mathcal{U}(A) \vdash B:\mathcal{U}, terms x:𝒯 𝒰(A)x:\mathcal{T}_\mathcal{U}(A) and y:𝒯 𝒰(A)y:\mathcal{T}_\mathcal{U}(A), and an identity p:id 𝒯 𝒰(A)(x,y)p:\mathrm{id}_{\mathcal{T}_\mathcal{U}(A)}(x,y), we have
ap z.B(p):id 𝒰(B(x),B(y))\mathrm{ap}_{z.B}(p):\mathrm{id}_\mathcal{U}(B(x),B(y))

and
(u,v):𝒯 𝒰(B(x))×𝒯 𝒰(B(y))⊢π 1(∇(ap z.B(p)))(u,v):𝒰(u,v):\mathcal{T}_\mathcal{U}(B(x)) \times \mathcal{T}_\mathcal{U}(B(y)) \vdash \pi_1(\nabla(\mathrm{ap}_{z.B}(p)))(u,v):\mathcal{U}

We could define a dependent identity type as
id 𝒯 𝒰(z.B) p(u,v)≔π 1(∇(ap z.B(p)))(u,v)\mathrm{id}_{\mathcal{T}_\mathcal{U}(z.B)}^{p}(u, v) \coloneqq \pi_1(\nabla(\mathrm{ap}_{z.B}(p)))(u, v)

There is a rule
A:𝒰z:𝒯 𝒰(A)⊢B:𝒰a:𝒯 𝒰(A)id 𝒯 𝒰(z.B) refl a(u,v)≡id 𝒯 𝒰(B[a/z])(u,v)\frac{A:\mathcal{U} \quad z:\mathcal{T}_\mathcal{U}(A) \vdash B:\mathcal{U} \quad a:\mathcal{T}_\mathcal{U}(A)}{\mathrm{id}_{\mathcal{T}_\mathcal{U}(z.B)}^{\refl_{a}}(u, v) \equiv \mathrm{id}_{\mathcal{T}_\mathcal{U}(B[a/z])}(u, v)}

and for constant families B:𝒰B:\mathcal{U}
id 𝒯 𝒰(z.B) p(u,v)≡id 𝒯 𝒰(B)(u,v)\mathrm{id}_{\mathcal{T}_\mathcal{U}(z.B)}^{p}(u, v) \equiv \mathrm{id}_{\mathcal{T}_\mathcal{U}(B)}(u, v)

See also

References

category: not redirected to nlab yet

Last revised on June 19, 2022 at 18:26:34. See the history of this page for a list of all contributions to it.

EditDiscussPrevious revisionHide changesHistory (15 revisions) Print Source