Homotopy Type Theory higher observational type theory > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Contents

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.

Definitions

We are working in a dependent type theory with universes.

The identity types in higher observational type theory have the following formation rule:

A: 𝒰 typea:𝒯 𝒰(A)b:𝒯 𝒰(A)id A(a,= Ab): 𝒰 type \frac{A:\mathcal{U} \frac{A\ \mathrm{type} \quad a:\mathcal{T}_\mathcal{U}(A) a:A \quad b:\mathcal{T}_\mathcal{U}(A)}{\mathrm{id}_A(a, b:A}{(a b):\mathcal{U}} =_A b)\ \mathrm{type}}

We define a general congruence term called ap

x:Af:Bp:id A(a,= Aa )ap x , .f(p):id B(f[a/x],f[a /x]) \frac{x:A \vdash f:B \quad p:\mathrm{id}_A(a, p:(a a^{'})}{\mathrm{ap}_{x,f}(p):\mathrm{id}_B(f[a/x], =_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,= Aa) \frac{a:A}{\mathrm{refl}_{a}:\mathrm{id}_A(a, \frac{a:A}{\mathrm{refl}_{a}:(a =_A a)}

and computation rules for identity functions

ap x , .x(p)p \mathrm{ap}_{x,x}(p) \mathrm{ap}_{x.x}(p) \equiv p

and for constant functions yy

ap x , .y(p)refl y \mathrm{ap}_{x,y}(p) \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}) \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)) \mathrm{ap}_{y.g}(\mathrm{ap}_{x.f}(p)) \equiv \mathrm{ap}_{x,g[f/y]}(p) \mathrm{ap}_{x.g[f/y]}(p)
ap x , .t(p)refl t \mathrm{ap}_{x,t}(p) \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 𝒰BR^:id 𝒰(A,B)\frac{R:A \cong_\mathcal{U} B}{\widehat{R}:\mathrm{id}_\mathcal{U}(A, B)}
P:id 𝒰(A,B)Pˇ:A 𝒰B\frac{P:\mathrm{id}_\mathcal{U}(A, B)}{\widecheck{P}:A \cong_\mathcal{U} B}
R:A 𝒰BR^ˇR\frac{R:A \cong_\mathcal{U} B}{\widecheck{\widehat{R}} \equiv R}

Identity types for product types

Computation rules are defend for product types:

id A×B(s,= A×Bt)id A(π 1(s),= Aπ 1(t))×id B(π 2(s),= Bπ 2(t)) \mathrm{id}_{A (s =_{A \times B}(s, B} t) \equiv \mathrm{id}_{A}(\pi_1(s), (\pi_1(s) =_A \pi_1(t)) \times \mathrm{id}_{B}(\pi_2(s), (\pi_2(s) =_B \pi_2(t))

with computation rules for ap

ap x , .(a,b)(p)(ap x , .a(p),ap x , .b(p)) \mathrm{ap}_{x, \mathrm{ap}_{x.(a,b)}(p) (a,b)}(p) \equiv (\mathrm{ap}_{x,a}(p), (\mathrm{ap}_{x.a}(p), \mathrm{ap}_{x,b}(p)) \mathrm{ap}_{x.b}(p))
ap x , .π 1(s)(p)π 1(ap x , .s(p)) \mathrm{ap}_{x, \mathrm{ap}_{x.\pi_1(s)}(p) \pi_1(s)}(p) \equiv \pi_1(\mathrm{ap}_{x,s}(p)) \pi_1(\mathrm{ap}_{x.s}(p))
ap x , .π 2(s)(p)π 2(ap x , .s(p)) \mathrm{ap}_{x, \mathrm{ap}_{x.\pi_2(s)}(p) \pi_2(s)}(p) \equiv \pi_2(\mathrm{ap}_{x,s}(p)) \pi_2(\mathrm{ap}_{x.s}(p))

and computation rules for reflexivity

refl (a,b)(p)(refl a(p),refl b(p))\mathrm{refl}_{(a,b)}(p) \equiv (\mathrm{refl}_{a}(p), \mathrm{refl}_{b}(p))
refl π 1(s)(p)π 1(refl s(p))\mathrm{refl}_{\pi_1(s)}(p) \equiv \pi_1(\mathrm{refl}_{s}(p))
refl π 2(s)(p)π 2(refl s(p))\mathrm{refl}_{\pi_2(s)}(p) \equiv \pi_2(\mathrm{refl}_{s}(p))

Identity types and singleton contractibility

π 1(refl Aˇ)id A\pi_1(\widecheck{\mathrm{refl}_A}) \equiv \mathrm{id}_A

Singleton contractibility:

π 1(π 2(refl Aˇ): a:AisContr( b:Aid A(a,b))\pi_1(\pi_2(\widecheck{\mathrm{refl}_A}):\prod_{a:A} \mathrm{isContr}\left(\sum_{b:A} \mathrm{id}_A(a, b)\right)
π 2(π 2(refl Aˇ)): b:AisContr( a:Aid A(a,b))\pi_2(\pi_2(\widecheck{\mathrm{refl}_A})):\prod_{b:A} \mathrm{isContr}\left(\sum_{a:A} \mathrm{id}_A(a, b)\right)

Dependent identity types

Given x:AB:𝒰x:A \vdash B:\mathcal{U} we could define a dependent identity type as

id x.B p(u,v)π 1(ap x.B(p)ˇ)(u,v)\mathrm{id}_{x.B}^{p}(u, v) \coloneqq \pi_1(\widecheck{\mathrm{ap}_{x.B}(p)})(u, v)

There are also rules

id x.B refl a(u,v)id B[a/x](u,v)\mathrm{id}_{x.B}^{\refl_{a}}(u, v) \equiv \mathrm{id}_{B[a/x]}(u, v)

and for constant families

id x.B const p(u,v)id B(u,v)\mathrm{id}_{x.B_\mathrm{const}}^{p}(u, v) \equiv \mathrm{id}_{B}(u, v)

Identity types for function types

Computation rules are defined for function types:

id AB(f,= ABg) a:A b:A q:id A(a,= Ab)id B(f(a),= Bg(b)) \mathrm{id}_{A (f =_{A \to B}(f, B} g) \equiv \prod_{a:A} \prod_{b:A} \prod_{q:\mathrm{id}_{A}(a,b)} \prod_{q:(a \mathrm{id}_{B}(f(a),g(b)) =_A b)} (f(a) =_B g(b))

with computation rules for ap

ap x , .f(b)(p)ap x , .f(p)(b[a/x],b[a /x],ap x , .b(p)) \mathrm{ap}_{x, \mathrm{ap}_{x.f(b)}(p) f(b)}(p) \equiv \mathrm{ap}_{x,f}(p)(b[a/x],b[a^{'}/x], \mathrm{ap}_{x.f}(p)(b[a/x],b[a^{'}/x], \mathrm{ap}_{x,b}(p)) \mathrm{ap}_{x.b}(p))

Computation rules are also defined for abstractions: TBD (involves currying)

Identity Dependent types identity for dependent function types

Given a type AA, a judgment z:𝒯 𝒰(A)B(z)typez:\mathcal{T}_\mathcal{U}(A) \vdash B(z)\ \mathrm{type}, terms x:Ax:A and y:Ay:A, and an identity p:(x= Ay)p:(x =_A y), there is a formation rule for dependent identity types

Atypez:AB(z)typex:Ay:Ap:(x= Ay)u:B(x)v:B(y)(u= B pv)type\frac{A\ \mathrm{type} \quad z:A \vdash B(z)\ \mathrm{type} \quad x:A \quad y:A \quad p:(x =_A y) \quad u:B(x) \quad v:B(y) }{(u =_{B}^{p} v)\ \mathrm{type}}

There is a rule

(u= B refl av)(u= B[a/z]v)(u =_{B}^{\refl_{a}} v) \equiv (u =_{B[a/z]} v)

and for constant families BB a rule

(u= B pv)id B(u= Bv)(u =_{B}^{p} v) \equiv \mathrm{id}_{B}(u =_B v)

Identity types for dependent pair types

Presets

(s= x:AB(x)t) p:(π 1(s)= Aπ 1(t))(π 2(s)= B pπ 2(t))(s =_{\sum_{x:A} B(x)} t) \equiv \sum_{p:(\pi_1(s) =_A \pi_1(t))} (\pi_2(s) =_{B}^p \pi_2(t))

Just as in set theory a preset is a set without an equality relation, a preset in higher observational type theory is a type without a recursively defined identity type.

Identity types for dependent function types

(f= x:AB(x)g) a:A b:A p:(a= Ab)(f(a)= B pg(b))(f =_{\prod_{x:A} B(x)} g) \equiv \prod_{a:A} \prod_{b:A} \prod_{p:(a =_{A} b)} (f(a) =_{B}^p g(b))

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

  • Mike Shulman, Towards a Third-Generation HOTT Part 1 (slides, video)

Revision on April 29, 2022 at 22:06:33 by Anonymous?. See the history of this page for a list of all contributions to it.