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
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

Where the idea of (non-higher) observational type theory is to equip all type formation rules (notably dependent functions, dependent pairs and inductive constructions) with their dedicated notion of structure preserving definitional equality — namely: component-wise, ie. homo-morphic, hence: “observational” —; the idea of higher observational type theory is to do the same for propositional equality hence for identification types used in homotopy type theory (where types behave like *higher* homomotopy types, whence the qualifier “higher”).

Concretely:

  • the “observational” principle for identification of dependent functions is to say that these are dependent functions of identifications of arguments and values (a statement otherwise known as function extensionality),

  • the “observational” principle for identifications of dependent pairs is to say that these are dependent pairs of identifications of factors,

and in ordinary univalent homotopy type theory this form of the “structure identity principle” follows as a type equivalence between identification types:

The idea of higher observational type theory is to make these and analogous structural characterizations of identification types be part of their definitional inference rules, thus building the structure identity principle right into the rewrite rules of the type theory.

In such a higher observational theory, in particular also the univalence axiom would be a definitional equality and hence would “compute”.

This most desirable property of any homotopy type theory has previously been accomplished only by cubical type theories. However, cubical type theories achieve this only by adding syntax for auxiliary/spurious interval types with rewrite rules which encode technical detail that has no abstract motivation other than making the univalence axiom compute and which one would rather keep out of the syntactic logic and instead relegate to the construction of categorical semantics.

The hope is therefore that higher observational type theory would provide a type system which achieves both:

  1. its syntax is as logically clean as that of Martin-Löf dependent type theory equipped with the univalence axiom;

  2. its inference rules for identification types make the univalence axiom be a computable function as it is in cubical type theories.

To which extent this hope is being realized would ideally be elucidated by the references below.

Details

This section does not quite get to the key points across and may need to be largely rewritten from scratch.

We are working in a dependent type theory with judgmental equality.

Telescopes

telescope types contain lists of iteratively dependent terms

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 defined 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 defined for dependent function 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))

Computation rules are defined 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))

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 as joint work of Thorsten Altenkirch, Ambrus Kaposi and Michael Shulman, first presented in:

The following article is about a fragment of higher observational type theory:

The authors of the above article write:

We presented a type theory with internal parametricity, a presheaf model and a canonicity proof. It can be seen as a baby version of higher observational type theory (HOTT). To obtain HOTT, we plan to add the following additional features to our theory:

  • a bridge type which can be seen as an indexed version of \forall,
  • Reedy fibrancy, which replaces spans by relations,
  • a strictification construction which turns the isomorphism for Π\Pi types into a definitional equality (in case of bridge, we also need the same for Σ\Sigma),
  • Kan fibrancy, which adds transport and turns the bridge type into a proper identity type. This would also change the correspondence between U\forall U and spans into U\forall U and equivalences.

Last revised on October 24, 2023 at 21:18:36. See the history of this page for a list of all contributions to it.