ch:identity-types: ch:identity-types

For the identity function, use identity induction with motive $$x,y:A,p:{\mathsf{Id}}_A(x,y)⊢{\mathsf{Id}}_{{\mathsf{Id}}_A(x,y)}({\mathsf{ap}}_{\lambda z.z}(p),p)\mathsf{type};$$ the reflexivity case is ${\mathsf{refl}}_{{\mathsf{refl}}_x}$. For the constant function use the motive $$x,y:A,p:{\mathsf{Id}}_A(x,y)⊢{\mathsf{Id}}_{{\mathsf{Id}}_B(b_0,b_0)}({\mathsf{ap}}_{\lambda z.b_0}(p),{\mathsf{refl}}_{b_0})\mathsf{type},$$ with the same kind of reflexivity clause.

With the definition of $\mathsf{ap}$ in construction 30.17, neither equation is a defining computation on a general identification variable $q$: both eliminators are blocked on $q$. Both compute judgmentally when $q$ is $\mathsf{refl}$.

For fixed $a:A$, based induction has motive $C(x,p)$ in $x:A,p:{\mathsf{Id}}_A(a,x)$ and branch $c:C(a,{\mathsf{refl}}_a)$; it is exactly $\mathsf{J}(C,c,x,p)$. Left unit uses $C(x,p):={\mathsf{Id}}_{}({\mathsf{refl}}_a\cdot p,p)$; inverse uses $C(x,p):={\mathsf{Id}}_{}(p^{-1}\cdot p,{\mathsf{refl}}_x)$; associativity fixes the other two paths and uses $C(x,p):={\mathsf{Id}}_{}((r\cdot q)\cdot p,r\cdot (q\cdot p))$. Each reflexive branch reduces by the path-composition definitions and is $\mathsf{refl}$. Inducting on the endpoint $x$ alone is ill typed: the motive also depends on the path $p:a=x$, which is not determined by $x$.

Start with the given premise $\cdot ⊢A\mathsf{type}$. Its ambient empty context is formed by Ctx-Emp; extending it gives $$\frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{\cdot \mathsf{ctx}}}\mathrm{Ctx}-\mathrm{Emp}\\ \cdot ⊢A\mathsf{type}\end{array}}{x:A\mathsf{ctx}}\mathrm{Ctx}-\mathrm{Ext}.$$ Writing out the context premise that is suppressed in the book’s compressed version of Var, the term derivation is $$\frac{{\displaystyle \frac{\begin{array}{c}\cdot ⊢A\mathsf{type}\\ {\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{\cdot \mathsf{ctx}}}\mathrm{Ctx}-\mathrm{Emp}\\ \cdot ⊢A\mathsf{type}\end{array}}{x:A\mathsf{ctx}}}\mathrm{Ctx}-\mathrm{Ext}\end{array}}{x:A⊢x:A}}\mathrm{Var}}{x:A⊢{\mathsf{refl}}_x:{\mathsf{Id}}_A(x,x)}\mathrm{Id}-\mathrm{intro}.$$ The final identity type is well formed by Id-form applied twice to the same variable judgment; this formation judgment is a presupposition of the conclusion of Id-intro. Thus every context and variable step has been made explicit rather than left to convention 26.14.

The based formation rule is $$\frac{\mathrm{\Gamma }⊢a:A}{\mathrm{\Gamma },y:A⊢{\mathsf{Id}}_A(a,y)\mathsf{type}}\mathrm{Id}-\mathrm{form}-\mathrm{based}.$$ It follows from ordinary Id-form. The premise presupposes $\mathrm{\Gamma }⊢A\mathsf{type}$. Weakening gives $\mathrm{\Gamma },y:A⊢a:A$, while Var gives $\mathrm{\Gamma },y:A⊢y:A$; hence $$\frac{\begin{array}{c}\mathrm{\Gamma },y:A⊢a:A\\ \mathrm{\Gamma },y:A⊢y:A\end{array}}{\mathrm{\Gamma },y:A⊢{\mathsf{Id}}_A(a,y)\mathsf{type}}\mathrm{Id}-\mathrm{form}.$$

Conversely, suppose the based rule is primitive and let $a,b:A$ in $\mathrm{\Gamma }$. Apply it to $a$ and then substitute $b$ for its final variable: $$\mathrm{\Gamma },y:A⊢{\mathsf{Id}}_A(a,y)\mathsf{type}{⟹}_{Subst}\mathrm{\Gamma }⊢{\mathsf{Id}}_A(a,b)\mathsf{type}.$$ This recovers binary Id-form.

Reflexivity already has only one meaningful based shape: $$\frac{\mathrm{\Gamma }⊢a:A}{\mathrm{\Gamma }⊢{\mathsf{refl}}_a:{\mathsf{Id}}_A(a,a)}.$$ The constructor lives on the diagonal, so its two endpoints are necessarily the same term. Unlike formation, there is no free second endpoint to turn into a variable or later recover by substitution; hence there is no distinct “binary” introduction rule to compare.

Define concatenation by induction on its first argument, generalizing the third endpoint and second path: $$p{\cdot }^{\prime }q:=(\mathsf{J}(x.y.r.\prod _{z:A}{\mathsf{Id}}_A(y,z)\to {\mathsf{Id}}_A(x,z);w.\lambda z.\lambda s.s;p))(c)(q).$$ The reflexivity computation is judgmental: $${\mathsf{refl}}_a{\cdot }^{\prime }q\equiv q.$$

We now construct the comparison in the two stages requested. First, identity induction on $p$ gives $$\eta (p):{\mathsf{Id}}_{{\mathsf{Id}}_A(a,b)}(p{\cdot }^{\prime }{\mathsf{refl}}_b,p).$$ The motive is $$x,y:A,r:{\mathsf{Id}}_A(x,y)⊢{\mathsf{Id}}_{{\mathsf{Id}}_A(x,y)}(r{\cdot }^{\prime }{\mathsf{refl}}_y,r)\mathsf{type},$$ and at $r={\mathsf{refl}}_x$ both endpoints compute to ${\mathsf{refl}}_x$, so the clause is ${\mathsf{refl}}_{{\mathsf{refl}}_x}$.

Next induct on $q:{\mathsf{Id}}_A(b,c)$, with $p$ generalized into the motive $$y,z:A,s:{\mathsf{Id}}_A(y,z)⊢\prod _{r:{\mathsf{Id}}_A(a,y)}{\mathsf{Id}}_{{\mathsf{Id}}_A(a,z)}(r\cdot s,r{\cdot }^{\prime }s)\mathsf{type}.$$ At $s={\mathsf{refl}}_y$, the original concatenation computes $r\cdot {\mathsf{refl}}_y\equiv r$, whereas the target is $r{\cdot }^{\prime }{\mathsf{refl}}_y$. The required clause is therefore $$\lambda r.\eta (r{)}^{-1}:\prod _{r:{\mathsf{Id}}_A(a,y)}{\mathsf{Id}}_{{\mathsf{Id}}_A(a,y)}(r,r{\cdot }^{\prime }{\mathsf{refl}}_y).$$ Applying the resulting dependent function to the original $p$ yields $${\mathsf{Id}}_{{\mathsf{Id}}_A(a,c)}(p\cdot q,p{\cdot }^{\prime }q).$$ Thus the two asymmetric definitions agree propositionally, although they choose opposite unit laws as their judgmental computation.

For $p:{\mathsf{Id}}_A(a,b)$, transport in an arbitrary small family gives Leibniz substitution: $$\lambda p.\lambda B.\lambda u.{\mathsf{tr}}_p^{x.B(x)}(u):{\mathsf{Id}}_A(a,b)\to L(a,b).$$ Indeed, for $B:A\to {\mathcal{U}}_i$, rule U-El makes each $B(x)$ a type, so transport sends $u:B(a)$ to a term of $B(b)$.

Conversely, let $\ell :L(a,b)$. The based identity family $$B_0:=\lambda w.{\mathsf{Id}}_A(a,w):A\to {\mathcal{U}}_i$$ is small by Id-form-$\mathcal{U}$. Since ${\mathsf{refl}}_a:B_0(a)$, instantiate $\ell$ at this family: $$\lambda \ell .\ell (B_0)({\mathsf{refl}}_a):L(a,b)\to {\mathsf{Id}}_A(a,b).$$ Thus identity implies indiscernibility and, once all small predicates may be quantified over, indiscernibility implies identity. No assertion that the two maps are judgmental inverses is needed.

Work in the extension with equality reflection. In the generic context $$x:A,y:A,p:{\mathsf{Id}}_A(x,y),$$ reflection gives $x\equiv y:A$. Hence ${\mathsf{refl}}_x:{\mathsf{Id}}_A(x,x)$ converts to a term $${\overline{\mathsf{refl}}}_x:{\mathsf{Id}}_A(x,y)$$ with the same raw expression. This makes the following motive legitimate: $$C(x,y,p):={\mathsf{Id}}_{{\mathsf{Id}}_A(x,y)}(p,{\overline{\mathsf{refl}}}_x).$$ On the reflexivity diagonal it reduces to $$C(z,z,{\mathsf{refl}}_z)={\mathsf{Id}}_{{\mathsf{Id}}_A(z,z)}({\mathsf{refl}}_z,{\mathsf{refl}}_z),$$ inhabited by ${\mathsf{refl}}_{{\mathsf{refl}}_z}$. Put $d(z):={\mathsf{refl}}_{{\mathsf{refl}}_z}$. Then $$k:=\lambda x.\lambda p.\mathsf{J}(u.v.q.C(u,v,q);z.d(z);p).$$ When the eliminand $p$ has endpoints $x,x$, the result type is literally $${\mathsf{Id}}_{{\mathsf{Id}}_A(x,x)}(p,{\mathsf{refl}}_x).$$ Thus $$k:\prod _{x:A}\prod _{p:{\mathsf{Id}}_A(x,x)}{\mathsf{Id}}_{{\mathsf{Id}}_A(x,x)}(p,{\mathsf{refl}}_x).$$ The construction pinpoints why reflection collapses intensional identity: it permits the diagonal reflexivity constructor to be typed in every generic fiber, thereby making the otherwise invalid K-motive well formed.

Let $$\ell (r):{\mathsf{Id}}_{{\mathsf{Id}}_A(u,v)}({\mathsf{refl}}_u\cdot r,r)$$ denote the left-unit identification of theorem 30.20(i), for $r:{\mathsf{Id}}_A(u,v)$. Induct on $q:{\mathsf{Id}}_A(b,c)$, generalizing both the earlier endpoint and the path $p$. Use the motive $$y,z:A,s:{\mathsf{Id}}_A(y,z)⊢\prod _{x:A}\prod _{r:{\mathsf{Id}}_A(x,y)}{\mathsf{Id}}_{{\mathsf{Id}}_A(z,x)}((r\cdot s{)}^{-1},s^{-1}\cdot r^{-1})\mathsf{type}.$$ In the reflexivity instance $s={\mathsf{refl}}_y$, the left endpoint computes as $$(r\cdot {\mathsf{refl}}_y{)}^{-1}\equiv r^{-1},$$ while the right endpoint computes to ${\mathsf{refl}}_y\cdot r^{-1}$, since ${\mathsf{refl}}_y^{-1}\equiv {\mathsf{refl}}_y$. Hence the clause is $$\lambda x.\lambda r.\ell (r^{-1}{)}^{-1}:\prod _{x:A}\prod _{r:{\mathsf{Id}}_A(x,y)}{\mathsf{Id}}_{{\mathsf{Id}}_A(y,x)}(r^{-1},{\mathsf{refl}}_y\cdot r^{-1}).$$ Identity induction supplies the desired family for arbitrary $q$; applying it to $a$ and $p$ gives $${\mathsf{Id}}_{{\mathsf{Id}}_A(c,a)}((p\cdot q{)}^{-1},q^{-1}\cdot p^{-1}).$$ The inverse on the left-unit witness is forced by the orientation of the goal in the reflexivity case.

Use identity induction on $p$ with motive At $r={\mathsf{refl}}_x$, functorial action computes to reflexivity for both functions. The left endpoint therefore reduces judgmentally to $$(h(x{)}^{-1}\cdot {\mathsf{refl}}_{f(x)})\cdot h(x)\equiv h(x{)}^{-1}\cdot h(x),$$ because the first concatenation uses its judgmental right-unit law. The right endpoint reduces to ${\mathsf{refl}}_{f^{\prime }(x)}$. Apply the second inverse law of theorem 30.20(ii) to $h(x):f(x)=f^{\prime }(x)$. It supplies the term $${\mathsf{Id}}_{{\mathsf{Id}}_B(f^{\prime }(x),f^{\prime }(x))}(h(x{)}^{-1}\cdot h(x),{\mathsf{refl}}_{f^{\prime }(x)}).$$ This supplies the reflexivity clause, so path induction gives the required identification for every $p$.

If the boundary composite is bracketed as $h(a{)}^{-1}\cdot ({\mathsf{ap}}_f(p)\cdot h(b))$, first use the associativity witness of theorem 30.20(iv) to compare it with the left-associated composite above, then concatenate that comparison with the constructed naturality identification.

Generalize the transported argument into the motive $$x,y:A,p:{\mathsf{Id}}_A(x,y)⊢\prod _{v:B(x)}{\mathsf{Id}}_{C(y)}({\mathsf{tr}}_p^C(h(x)(v)),h(y)({\mathsf{tr}}_p^B(v)))\mathsf{type}.$$ At $p={\mathsf{refl}}_x$, both transports compute judgmentally: $${\mathsf{tr}}_{{\mathsf{refl}}_x}^C(h(x)(v))\equiv h(x)(v),h(x)({\mathsf{tr}}_{{\mathsf{refl}}_x}^B(v))\equiv h(x)(v).$$ Hence the reflexivity clause is simply $$\lambda v.{\mathsf{refl}}_{h(x)(v)}.$$ Identity elimination with this motive yields a dependent function in $v:B(a)$; applying it to $u$ produces $${\mathsf{Id}}_{C(b)}({\mathsf{tr}}_p^C(h(a)(u)),h(b)({\mathsf{tr}}_p^B(u))).$$ The construction is the naturality of transport with respect to a fiberwise map $h$.

For $q:{\mathsf{Id}}_A(a,b)$, based induction at the fixed source $a$ reconstructs inverse as $$q^{-1}:={\mathsf{J}}^{\prime }(y.p.{\mathsf{Id}}_A(y,a);{\mathsf{refl}}_a;q):{\mathsf{Id}}_A(b,a).$$ Its computation is ${\mathsf{refl}}_a^{-1}\equiv {\mathsf{refl}}_a$ by Id-comp${}^{\prime }$.

For $p:{\mathsf{Id}}_A(a,b)$ and $q:{\mathsf{Id}}_A(b,c)$, apply based induction to $q$, whose fixed source is $b$: $$p\star q:={\mathsf{J}}^{\prime }(z.r.{\mathsf{Id}}_A(a,z);p;q):{\mathsf{Id}}_A(a,c).$$ The based computation rule gives $$p\star {\mathsf{refl}}_b\equiv p.$$ Thus the right unit is judgmental. This is the same asymmetry and, up to notation, the same operation as the concatenation of construction 30.15, which transports $p$ along the second path. Defining concatenation instead by based induction on the first path would require the second path to be generalized and would select the left unit as the direct computation.

Let $f:\prod _{x:A}B(x)$ and $q:{\mathsf{Id}}_A(a,b)$. For the ordinary $J$-motive used by dependent action, put $$C(x,y,p):={\mathsf{Id}}_{B(y)}({\mathsf{tr}}_p^B(f(x)),f(y)).$$ Fixing the first endpoint at $a$, its uncurried family over the singleton $u:{\mathrm{Sing}}_A(a)$ is $${\hat{C}}_a(u):={\mathsf{Id}}_{B({\mathsf{pr}}_1(u))}({\mathsf{tr}}_{{\mathsf{pr}}_2(u)}^B(f(a)),f({\mathsf{pr}}_1(u))).$$ The formula for ${\mathsf{J}}_{\mathsf{tr}}$ in proposition 30.27 therefore gives the reconstruction $${\mathsf{apd}}_f(q):={\mathsf{tr}}_{{\mathsf{uniq}}_a((b,q))}^{u.{\hat{C}}_a(u)}({\mathsf{refl}}_{f(a)}).$$ At the center, the source fiber is $${\hat{C}}_a((a,{\mathsf{refl}}_a))\equiv {\mathsf{Id}}_{B(a)}({\mathsf{tr}}_{{\mathsf{refl}}_a}^B(f(a)),f(a))\equiv {\mathsf{Id}}_{B(a)}(f(a),f(a)),$$ so the displayed ${\mathsf{refl}}_{f(a)}$ is well typed by conversion. At $(b,q)$, the target fiber is exactly $${\mathsf{Id}}_{B(b)}({\mathsf{tr}}_q^B(f(a)),f(b)).$$

For $q={\mathsf{refl}}_a$, singleton contraction computes first and transport computes second: This verifies the required judgmental computation using only the primitive rules for $\mathsf{tr}$ and $\mathsf{uniq}$, not primitive $\mathsf{J}$.

Assume $u:{\mathsf{UIP}}_A$, fix $a,b:A$, and abbreviate $$I:={\mathsf{Id}}_A(a,b).$$ We construct ${\mathsf{UIP}}_I$. Fix first $p:I$, and for every $q:I$ define the canonical path $$c(q):=u(a)(b)(p)(q):{\mathsf{Id}}_I(p,q).$$ For $q:I$ put $$k(q):=c(p{)}^{-1}\cdot c(q):{\mathsf{Id}}_I(p,q).$$ We first compare every path out of $p$ with this canonical one. Based path induction on $r:{\mathsf{Id}}_I(p,q)$ gives $$d(q,r):{\mathsf{Id}}_{{\mathsf{Id}}_I(p,q)}(r,k(q)).$$ The motive is $$q:I,r:{\mathsf{Id}}_I(p,q)⊢{\mathsf{Id}}_{{\mathsf{Id}}_I(p,q)}(r,c(p{)}^{-1}\cdot c(q))\mathsf{type}.$$ At $q=p,r={\mathsf{refl}}_p$, the target is $c(p{)}^{-1}\cdot c(p)$. The inverse law supplies $$\iota (c(p)):{\mathsf{Id}}_{{\mathsf{Id}}_I(p,p)}(c(p{)}^{-1}\cdot c(p),{\mathsf{refl}}_p),$$ so the required reflexivity clause, oriented from ${\mathsf{refl}}_p$ to the canonical composite, is $\iota (c(p){)}^{-1}$.

Now let $r,s:{\mathsf{Id}}_I(p,q)$. Both are connected to the same canonical path, hence $$d(q,r)\cdot d(q,s{)}^{-1}:{\mathsf{Id}}_{{\mathsf{Id}}_I(p,q)}(r,s).$$ Abstracting successively over $p,q,r,s$ constructs $$\prod _{p:I}\prod _{q:I}\prod _{r:{\mathsf{Id}}_I(p,q)}\prod _{s:{\mathsf{Id}}_I(p,q)}{\mathsf{Id}}_{{\mathsf{Id}}_I(p,q)}(r,s),$$ which is ${\mathsf{UIP}}_I$. Thus UIP at $A$ propagates to every identity type of $A$.

Unfold $$\chi :\prod _{f:\mathbf{2}\to \mathbf{2}}\prod _{g:\mathbf{2}\to \mathbf{2}}\mathsf{Pt}(f,g)\to {\mathsf{Id}}_{\mathbf{2}\to \mathbf{2}}(f,g).$$ The function $$g:=\lambda x.{\mathsf{ind}}_{\mathbf{2}}(y.\mathbf{2};\mathsf{tt},\mathsf{ff};x)$$ has type $\mathbf{2}\to \mathbf{2}$: in context $x:\mathbf{2}$, the constant motive is $\mathbf{2}$, both branches have that type, and the scrutinee is $x$. Its closed-constructor computations are $$g(\mathsf{tt})\equiv \mathsf{tt},g(\mathsf{ff})\equiv \mathsf{ff}.$$ For a variable $x$, however, the Boolean eliminator in its body is neutral.

For $$h:=\lambda x.{\mathsf{ind}}_{\mathbf{2}}(y.{\mathsf{Id}}_{\mathbf{2}}(y,g(y));{\mathsf{refl}}_{\mathsf{tt}},{\mathsf{refl}}_{\mathsf{ff}};x),$$ the motive is a type because $y:\mathbf{2}$ and $g(y):\mathbf{2}$. In the true branch, $g(\mathsf{tt})\equiv \mathsf{tt}$, so ${\mathsf{refl}}_{\mathsf{tt}}$ converts to ${\mathsf{Id}}_{\mathbf{2}}(\mathsf{tt},g(\mathsf{tt}))$; the false branch is identical. Hence $$h:\prod _{x:\mathbf{2}}{\mathsf{Id}}_{\mathbf{2}}(x,g(x))=\mathsf{Pt}(\lambda x.x,g).$$ The applications of $\chi$ therefore derive $$e:=\chi (\lambda x.x)(g)(h):{\mathsf{Id}}_{\mathbf{2}\to \mathbf{2}}(\lambda x.x,g).$$ Now take the constant $J$-motive $u,v:\mathbf{2}\to \mathbf{2},p:{\mathsf{Id}}_{\mathbf{2}\to \mathbf{2}}(u,v)⊢\mathbf{2}$ and the clause $z.\mathsf{tt}$. Rule Id-elim gives $$b:=\mathsf{J}(u.v.p.\mathbf{2};z.\mathsf{tt};e):\mathbf{2}.$$

The reductions available inside this construction are:

• function beta exposes the bodies of $g(t)$ and $h(t)$;

• Boolean computation reduces $g(\mathsf{tt}),g(\mathsf{ff})$ and, after beta, reduces $h(\mathsf{tt}),h(\mathsf{ff})$ to the corresponding reflexivity terms;

• the identity function satisfies $(\lambda x.x)(t)\equiv t$;

• substitutions into the constant outer motive and constant clause are literal.

The blocked neutral subterms are:

• ${\mathsf{ind}}_{\mathbf{2}}(y.\mathbf{2};\mathsf{tt},\mathsf{ff};x)$ when $x$ is a variable;

• the analogous Boolean eliminator defining $h(x)$ when its scrutinee is a variable;

• the application $e=\chi (\lambda x.x)(g)(h)$, whose head is the variable $\chi$;

• consequently the outer $J$-term, whose eliminand is the neutral term $e$, not a displayed $\mathsf{refl}$.

Rule Id-comp therefore does not apply to $b$. Function extensionality has supplied an identification, but no computation rule for that variable-provided identification.

Let $F:=\prod _{x:A}B$. Unfolding the definition gives $$s:\prod _{f^{\prime }:F}\prod _{g^{\prime }:F}\mathsf{Pt}(f^{\prime },g^{\prime })\to {\mathsf{Id}}_F(f^{\prime },g^{\prime }).$$ One Pi-elimination at $f:F$ yields $$s(f):\prod _{g^{\prime }:F}\mathsf{Pt}(f,g^{\prime })\to {\mathsf{Id}}_F(f,g^{\prime }),$$ and a second at $g:F$ yields $$s(f)(g):\mathsf{Pt}(f,g)⟶{\mathsf{Id}}_F(f,g).$$ The pointwise-action construction supplies the opposite map $${\mathsf{happly}}_{f,g}:{\mathsf{Id}}_F(f,g)⟶\mathsf{Pt}(f,g).$$ Thus the two displayed maps are $$\mathsf{Pt}(f,g)\stackrel{s(f)(g)}{⟶}{\mathsf{Id}}_F(f,g)\stackrel{{\mathsf{happly}}_{f,g}}{⟶}\mathsf{Pt}(f,g).$$ The type of $s$ asserts only existence of the first map. It contains no fields or equations saying either composite is an identity, so no inverse law follows merely by unfolding the binders.