nLab higher observational type theory

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
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit 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 setinternal homfunction type
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian productdependent productdependent product type
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijectionisomorphism/adjoint equivalenceequivalence of types
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

What is called higher observational type theory (HOTT) is a flavor of intensional type theory that is a higher homotopy version of observational type theory (OTT).

It may be regarded as a homotopy type theory (HoTT): the propositions of OTT correspond to the h-propositions of HoTT, the sets in OTT correspond to h-sets in HoTT, and so forth. The notion of equality on HOTT in a type universe is based on one-to-one correspondences, but is usually defined as a primitive identity type for types outside a universe. Since equality is defined type-by-type, HOTT enjoys function extensionality.

There are a few technical differences (e.g. proofs of types in a universe are definitionally equal in HOTT, whereas proofs of types in a universe are only propositionally equal in HoTT) but on the whole HoTT looks a lot like HOTT.

Overview

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= AB ς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:Af: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 one-to-one 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

Higher observational type theory was introduced in

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