## 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. ## Definitions ## We are working in a [[dependent type theory]] with [[universes]]. The [[identity types]] 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}{\widehat{R}:\mathrm{id}_\mathcal{U}(A, B)}$$ $$\frac{P:\mathrm{id}_\mathcal{U}(A, B)}{\widecheck{P}:A \cong_\mathcal{U} B}$$ $$\frac{R:A \cong_\mathcal{U} B}{\widecheck{\widehat{R}} \equiv R}$$ ### Identity types for product types ### Computation rules are defend for product types: $$\mathrm{id}_{A \times B}(s, t) \equiv \mathrm{id}_{A}(\pi_1(s), \pi_1(t)) \times \mathrm{id}_{B}(\pi_2(s), \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 and singleton contractibility ### $$\pi_1(\widecheck{\mathrm{refl}_A}) \equiv \mathrm{id}_A$$ Singleton contractibility: $$\pi_1(\pi_2(\widecheck{\mathrm{refl}_A}):\prod_{a:A} \mathrm{isContr}\left(\sum_{b:A} \mathrm{id}_A(a, b)\right)$$ $$\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:A \vdash B:\mathcal{U}$ we could define a dependent identity type as $$\mathrm{id}_{x.B}^{p}(u, v) \coloneqq \pi_1(\widecheck{\mathrm{ap}_{x.B}(p)})(u, v)$$ There are also rules $$\mathrm{id}_{x.B}^{\refl_{a}}(u, v) \equiv \mathrm{id}_{B[a/x]}(u, v)$$ and for constant families $$\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: $$\mathrm{id}_{A \to B}(f, g) \equiv \prod_{a:A} \prod_{b:A} \prod_{q:\mathrm{id}_{A}(a,b)} \mathrm{id}_{B}(f(a),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) ### Identity types for dependent function types ### ### Identity types for dependent pair types ### ### Presets ### 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. ## See also ## * [[homotopy 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))