[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] **[[type formation rules]]** for the unit type $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Unit} \; \mathrm{type}}$$ \linebreak **[[term introduction rules]]** for the unit type: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{pt}:\mathrm{Unit}}$$ \linebreak **fiberwise elimination rules** for the unit type: $$\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \mathrm{Unit} \quad \Gamma \vdash c:C \quad \Gamma \vdash p:f(c) =_\mathrm{Unit} \mathrm{pt} \\ \Gamma \vdash b:\mathrm{Unit} \end{array} }{\Gamma \vdash \mathrm{ind}_\mathrm{Unit}^{C, \mathrm{sec}}(f, c, p, b):C}$$ $$\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \mathrm{Unit} \quad \Gamma \vdash c:C \quad \Gamma \vdash p:f(c) =_\mathrm{Unit} \mathrm{pt} \\ \Gamma \vdash b:\mathrm{Unit} \end{array} }{\Gamma \vdash \mathrm{ind}_\mathrm{Unit}^{C, \mathrm{path}}(f, c, p, b):f(\mathrm{ind}_\mathrm{Unit}^{C, \mathrm{sec}}(f, c, p, b)) =_\mathrm{Unit} b}$$ **fiberwise computation rules** for the unit type: $$\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \mathrm{Unit} \quad \Gamma \vdash c:C \quad \Gamma \vdash p:f(c) =_\mathrm{Unit} \mathrm{pt} \\ \end{array} }{\Gamma \vdash \beta_\mathrm{Unit}^{C, \mathrm{sec}, \mathrm{pt}}(f, c, p):\mathrm{ind}_\mathrm{Unit}^{C, \mathrm{sec}}(f, c, p, \mathrm{pt}) =_{C} c}$$ $$\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \mathrm{Unit} \quad \Gamma \vdash c:C \quad \Gamma \vdash p:f(c) =_\mathrm{Unit} \mathrm{pt} \\ \end{array} }{\Gamma \vdash \beta_\mathrm{Unit}^{C, \mathrm{path}, \mathrm{pt}}(f, c, p):\mathrm{ind}_\mathrm{Unit}^{C, \mathrm{path}}(f, c, p, \mathrm{pt}) =_{f(-) =_\mathrm{Unit} \mathrm{pt}}^{\beta_\mathrm{Unit}^{C, \mathrm{sec}, \mathrm{pt}}(f, c, p)} p}$$ The usual induction rules are given for $C \equiv \sum_{x:\mathrm{Unit}} P(x)$ ---- We work on the interval type instead of the circle type, since that is more relevant for my purposes given a heterogeneous identification $c_p:c_0 =_{\sum_{z:C} f(z) =_\mathbb{I} (-)}^{p} c_1$, ... maybe we could use transport $$\mathrm{tr}_{\sum_{z:C} f(z) =_\mathbb{I} (-)}^{p}:\left(\sum_{z:C} f(z) =_\mathbb{I} 0\right) \simeq \left(\sum_{z:C} f(z) =_\mathbb{I} 1\right)$$ because then we just have $$c_p:\mathrm{tr}_{\sum_{z:C} f(z) =_\mathbb{I} (-)}^{p}(c_0) =_{\sum_{z:C} f(z) =_\mathbb{I} 1} c_1$$ But we have $$\lambda w:\left(\sum_{z:C} f(z) =_\mathbb{I} 0\right).(\pi_1(w), \pi_2(w) \bullet p):\left(\sum_{z:C} f(z) =_\mathbb{I} 0\right) \to \left(\sum_{z:C} f(z) =_\mathbb{I} 1\right)$$ to use as the transport function, with inverse function $$\lambda w:\left(\sum_{z:C} f(z) =_\mathbb{I} 1\right).(\pi_1(w), \pi_2(w) \bullet p^{-1}):\left(\sum_{z:C} f(z) =_\mathbb{I} 1\right) \to \left(\sum_{z:C} f(z) =_\mathbb{I} 0\right)$$ so we could just use $$c_p:(\pi_1(c_0), \pi_2(c_0) \bullet p) =_{\sum_{z:C} f(z) =_\mathbb{I} 1} c_1$$ This means that it suffices to have $$c_0:C \quad q_0:f(c_0) =_\mathbb{I} 0 \quad c_1:C \quad q_1:f(c_1) =_\mathbb{I} 1$$ $$c_p:(c_0, q_0 \bullet p) =_{\sum_{z:C} f(z) =_\mathbb{I} 1} (c_1, q_1)$$ by the extensionality principle of dependent sum types, this is the same as $$c_p:\sum_{r:c_0 =_C c_1} q_0 \bullet p =_{f(-) =_\mathbb{I} 1}^r q_1$$ so it suffices to have $$c_0:C \quad q_0:f(c_0) =_\mathbb{I} 0 \quad c_1:C \quad q_1:f(c_1) =_\mathbb{I} 1$$ $$c_p:c_0 =_C c_1 \quad q_p:q_0 \bullet p =_{f(-) =_\mathbb{I} 1}^{c_p} q_1$$ or alternatively, using heterogeneous identifications over $(c_p, p):(c_0, 0) =_{C \times \mathbb{I}} (c_1, 1)$ we have $$c_p:c_0 =_C c_1 \quad q_p:q_0 =_{f(-) =_\mathbb{I} (-)}^{c_p, p} q_1$$ ---- More heterogeneous identity types: Suppose you have type $A$, type family $x:A \vdash B(x)$, and type family $x:A, y:B(x) \vdash z:C(x, y)$, elements $a_0:A$, $a_1:A$, $a_p:a_0 =_A a_1$, $b_0:B(a_0)$, $b_1:B(a_1)$, $b_p:b_0 =_{B(-)}^{a_p} b_1$, and $c_0:C(a_0, b_0)$ and $c_1:C(a_1, b_1)$. Then there exists a type family $c_0 =_{C(-,-)}^{a_p, b_p} c_1$ inductively generated by $\mathrm{hrefl}_{C(-,-)}(c_0):c_0 =_{C(-, -)}^{\mathrm{refl}_A(a_0)), \mathrm{hrefl}_{B(-)}(b_0))} c_0$ Then by the extensionality principle of dependent sum types we have that $$\left(c_0 =_{C(-,-)}^{a_p, b_p} c_1\right) \simeq \left(\mathrm{ind}_\sum(c_0) =_{C(-)}^{\mathrm{ext}_\sum^{-1}(a_p, b_p)} \mathrm{ind}_\sum(c_1)\right)$$ category: redirected to nlab