## Contents ## * table of contents {:toc} ## 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]]. ### Identity types ### The [[identity types]] in higher observational type theory have the following formation rule: $$\frac{A\ \mathrm{type} \quad a:A \quad b:A}{(a =_A b)\ \mathrm{type}}$$ We define a general congruence term called ap $$\frac{x:A \vdash f:B \quad p:(a =_A a^{'})}{\mathrm{ap}_{x.f}(p):(f[a/x] =_B f[a^{'}/x])}$$ and the reflexivity terms: $$\frac{a:A}{\mathrm{refl}_{a}:(a =_A a)}$$ and computation rules for identity functions $$\mathrm{ap}_{x.x}(p) \equiv p$$ and for constant functions $y$ $$\mathrm{ap}_{x.y}(p) \equiv \mathrm{refl}_{y}$$ Thus, ap is a higher dimensional explicit substitution. There are definitional equalities $$\mathrm{ap}_{x.f}(\mathrm{refl}_{a}) \equiv \mathrm{refl}_{f[a/x]}$$ $$\mathrm{ap}_{y.g}(\mathrm{ap}_{x.f}(p)) \equiv \mathrm{ap}_{x.g[f/y]}(p)$$ $$\mathrm{ap}_{x.t}(p) \equiv \mathrm{refl}_{t}$$ for constant term $t$. ### Identity types for pair types ### Computation rules are defend for pair types: $$(s =_{A \times B} t) \equiv (\pi_1(s) =_A \pi_1(t)) \times (\pi_2(s) =_B \pi_2(t))$$ with computation rules for ap $$\mathrm{ap}_{x.(a,b)}(p) \equiv (\mathrm{ap}_{x.a}(p), \mathrm{ap}_{x.b}(p))$$ $$\mathrm{ap}_{x.\pi_1(s)}(p) \equiv \pi_1(\mathrm{ap}_{x.s}(p))$$ $$\mathrm{ap}_{x.\pi_2(s)}(p) \equiv \pi_2(\mathrm{ap}_{x.s}(p))$$ and computation rules for reflexivity $$\mathrm{refl}_{(a,b)}(p) \equiv (\mathrm{refl}_{a}(p), \mathrm{refl}_{b}(p))$$ $$\mathrm{refl}_{\pi_1(s)}(p) \equiv \pi_1(\mathrm{refl}_{s}(p))$$ $$\mathrm{refl}_{\pi_2(s)}(p) \equiv \pi_2(\mathrm{refl}_{s}(p))$$ ### Identity types for function types ### Computation rules are defined for function types: $$(f =_{A \to B} g) \equiv \prod_{a:A} \prod_{b:A} \prod_{q:(a =_A b)} (f(a) =_B g(b))$$ with computation rules for ap $$\mathrm{ap}_{x.f(b)}(p) \equiv \mathrm{ap}_{x.f}(p)(b[a/x],b[a^{'}/x], \mathrm{ap}_{x.b}(p))$$ Computation rules are also defined for abstractions: TBD (involves currying) ### Dependent identity types ### Given a type $A$, a judgment $z:A \vdash B(z)\ \mathrm{type}$, terms $x:A$ and $y:A$, and an identity $p:(x =_A y)$, there is a formation rule for dependent identity types $$\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}}$$ We define a general congruence term called ap $$\frac{p:(x =_A y) \quad t:A, z(t):B(t) \vdash f(t):C(t) \quad q:(u =_{B}^{p} v)}{\mathrm{ap}_{z.f}(q):(f(x)[u/z(x)] =_{C}^p f(y)[v/z(y)])}$$ TODO: Define introduction, elimination, and computation rules for dependent identity types. There is a rule $$(u =_{B}^{\refl_{a}} v) \equiv (u =_{B[a/z]} v)$$ and for constant families $B$ a rule $$(u =_{B}^{p} v) \equiv (u =_B v)$$ ### Identity types for dependent pair types ### Computation rules are defend for dependent pair types: $$(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))$$ with computation rules for ap ... ### Identity types for dependent function types ### Computation rules are defend for dependent pair types: $$(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))$$ ## 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: $$\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 $$\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: $$\frac{a:A}{\mathrm{refl}_{a}:\mathrm{id}_A(a, a)}$$ and computation rules for identity functions $$\mathrm{ap}_{x.x}(p) \equiv p$$ and for constant functions $y$ $$\mathrm{ap}_{x.y}(p) \equiv \mathrm{refl}_{y}$$ Thus, ap is a higher dimensional explicit substitution. There are definitional equalities $$\mathrm{ap}_{x.f}(\mathrm{refl}_{a}) \equiv \mathrm{refl}_{f[a/x]}$$ $$\mathrm{ap}_{y.g}(\mathrm{ap}_{x.f}(p)) \equiv \mathrm{ap}_{x.g[f/y]}(p)$$ $$\mathrm{ap}_{x.t}(p) \equiv \mathrm{refl}_{t}$$ for constant term $t$. ### Identity types for universes ### Let $A \cong_\mathcal{U} B$ be the type of [[bijective correspondences]] between two terms of a universe $A:\mathcal{U}$ and $B:\mathcal{U}$, and let $\mathrm{id}_\mathcal{U}(A, B)$ be the identity type between two terms of a universe $A:\mathcal{U}$ and $B:\mathcal{U}$. Then there are rules $$\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:\mathcal{U}$ $$\mathrm{id}_{\mathcal{T}_\mathcal{U}(A)} \equiv \pi_1(\nabla(\mathrm{refl}_A))$$ with terms representing **singleton contractibility. $$\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)$$ $$\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:\mathcal{U}$, a judgment $z:\mathcal{T}_\mathcal{U}(A) \vdash B:\mathcal{U}$, terms $x:\mathcal{T}_\mathcal{U}(A)$ and $y:\mathcal{T}_\mathcal{U}(A)$, and an identity $p:\mathrm{id}_{\mathcal{T}_\mathcal{U}(A)}(x,y)$, we have $$\mathrm{ap}_{z.B}(p):\mathrm{id}_\mathcal{U}(B(x),B(y))$$ and $$(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 $$\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 $$\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:\mathcal{U}$ $$\mathrm{id}_{\mathcal{T}_\mathcal{U}(z.B)}^{p}(u, v) \equiv \mathrm{id}_{\mathcal{T}_\mathcal{U}(B)}(u, v)$$ ## See also ## * [[homotopy type theory]] * [[Martin-Loef type theory]] * [[cubical type theory]] ## References ## * Mike Shulman, Towards a Third-Generation HOTT Part 1 ([slides](https://www.cmu.edu/dietrich/philosophy/hott/slides/shulman-2022-04-28.pdf), [video](https://www.youtube.com/watch?v=FrxkVzItMzA)) * Mike Shulman, Towards a Third-Generation HOTT Part 2 ([slides](https://www.cmu.edu/dietrich/philosophy/hott/slides/shulman-2022-05-05.pdf), [video](https://www.youtube.com/watch?v=5ciDNfmvMdU), [temporary video](https://u.pcloud.link/publink/show?code=XZXBjpVZ8cOAFR7oWoRbobS6NWsNE82pz3Ny))