ch:algebraic-syntax: ch:algebraic-syntax

Apply Ext-Uniq to the two substitutions. Their projection components agree because $\mathbf{p}\circ (\gamma \circ \delta )\equiv (\mathbf{p}\circ \gamma )\circ \delta$ by category associativity. Their term components agree because $\mathbf{q}[⟨\gamma ,a⟩\circ \delta ]\equiv \mathbf{q}[⟨\gamma ,a⟩][\delta ]\equiv a[\delta ]$. These are exactly the category and term equations needed by uniqueness, hence $⟨\gamma ,a⟩\circ \delta \equiv ⟨\gamma \circ \delta ,a[\delta ]⟩$.

Expand ${\gamma }^{+}$ as $⟨\gamma \circ \mathbf{p},\mathbf{q}⟩$. For $\gamma =\mathsf{id}$, the projection triangle reduces to $\mathbf{p}$ and the variable triangle to $\mathbf{q}$, so Ext-Uniq gives ${\mathsf{id}}^{+}=\mathsf{id}$. For a composite, use lemma 116.10 twice: both sides have projection $\gamma \circ \delta \circ \mathbf{p}$, while substitution of $\mathbf{q}$ through the lifted right factor reduces again to $\mathbf{q}$. Ext-Uniq therefore gives ${(\gamma \circ \delta )}^{+}={\gamma }^{+}\circ {\delta }^{+}$ at the appropriately substituted type.

Stability of $\mathrm{\Pi }$ gives $\mathrm{\Pi }(A,B)[\gamma ]=\mathrm{\Pi }(A[\gamma ],B[{\gamma }^{+}])$, so the substituted function and argument may be fed to application. Its result type is $B[{\gamma }^{+}][⟨\mathsf{id},a[\gamma ]⟩]$. Term substitution composition changes this to $B[{\gamma }^{+}\circ ⟨\mathsf{id},a[\gamma ]⟩]$. The extension-composition lemma and the two triangles give ${\gamma }^{+}\circ ⟨\mathsf{id},a[\gamma ]⟩=⟨\gamma ,a[\gamma ]⟩$, which is the type on the other side of App-Sb.

At $k=0$ the generic variable has type $A[\mathbf{p}]$. If the displayed term has type $A[{\mathbf{p}}^{k+1}]$ after $k$ extensions, weaken it once. Tm-Subst changes its type to $A[{\mathbf{p}}^{k+1}][\mathbf{p}]$, and substitution composition makes this $A[{\mathbf{p}}^{k+2}]$. The term itself is $\mathbf{q}[{\mathbf{p}}^k][\mathbf{p}]=\mathbf{q}[{\mathbf{p}}^{k+1}]$. Induction on $k$ proves the rule.

In algebraic notation the term is $$\mathsf{lam}(\mathsf{lam}(\mathbf{q}[\mathbf{p}])).$$ The inner generic variable would denote $y$; weakening it once selects the preceding variable $x$. Its type is $A[\mathbf{p}][\mathbf{p}]$, so the inner abstraction has type $\mathrm{\Pi }(A[\mathbf{p}],A[\mathbf{p}])$ and the outer abstraction has the translation of $\mathrm{\Pi }(x:A).\mathrm{\Pi }(y:B).A$. Thus both weakenings occur under the second binder: one in the selected term and one in the translated constant family $A$.

Induct on $b$. A variable is either the variable being replaced, where Var-Ext returns $a$, or an older variable, where Var-Wk commutes past the extension. Application follows from the two induction hypotheses and App-Sb. For $\lambda b_0$, substitution under the binder is by ${⟨\mathsf{id},a⟩}^{+}$; the lift/extension equations reduce this to the simultaneous assignment that fixes the new variable and substitutes $a$ for the next one. The induction hypothesis for $b_0$, followed by Lam-Sb, is exactly the translation of capture-avoiding $b_0[a/x]$.

Distribution through application gives $$E[\mathsf{app}(v_1,v_0),[g,a]]=\mathsf{app}(E[v_1,[g,a]],E[v_0,[g,a]])=\mathsf{app}(g,a).$$ The lifted list is $\mathsf{lift}([g,a])=[\mathsf{shift}(g),\mathsf{shift}(a),v_0]$. List lookup therefore sends $v_0$ to the fresh variable $v_0$, $v_1$ to $\mathsf{shift}(a)$, and $v_2$ to $\mathsf{shift}(g)$. Their types are, respectively, $C$, the weakening of $A$, and the weakening of $A\to B$ in $\mathrm{\Delta },y:C$.

Put $T(\mathrm{\Gamma })=(\mathrm{Ty}(\mathrm{\Gamma }),A\mapsto \mathrm{Tm}(\mathrm{\Gamma },A))$. For $\gamma :\mathrm{\Delta }\to \mathrm{\Gamma }$, let $T(\gamma )$ send $A$ to $A[\gamma ]$ and $a$ to $a[\gamma ]$. The equations $A[\mathsf{id}]=A$, $A[\gamma \circ \delta ]=(A[\gamma ])[\delta ]$ and their two term analogues say exactly that $T(\mathsf{id})$ is the identity family map and $T(\gamma \circ \delta )=T(\delta )T(\gamma )$. Thus the four substitution equations are precisely the contravariant functor laws, in both base and fiber components.

The first universal property gives $u=⟨p^{\prime },q^{\prime }⟩:E\to \mathrm{\Gamma }.A$; the second gives $v=⟨\mathbf{p},\mathbf{q}{⟩}^{\prime }:\mathrm{\Gamma }.A\to E$. Both $uv$ and the identity have projection $\mathbf{p}$ and generic component $\mathbf{q}$, so uniqueness gives $uv=\mathsf{id}$; symmetrically $vu=\mathsf{id}$. Any map commuting with the two components is forced by the corresponding uniqueness clause, so this isomorphism is unique.

Set $\tau =⟨\delta ,{\mathbf{q}}_A[\sigma ]⟩$. Its first triangle is $\mathbf{p}\circ \tau =\delta$. For the second, naturality of substitution and the assumed equality give $$A[\gamma ][\delta ]=A[\gamma \circ \delta ]=A[{\mathbf{p}}_A\circ \sigma ],$$ which is the type of ${\mathbf{q}}_A[\sigma ]$; the variable triangle then yields the required comparison with $\sigma$. If ${\tau }^{\prime }$ has the same triangles, its projection is $\delta$ and its generic component is ${\mathbf{q}}_A[\sigma ]$, so comprehension uniqueness gives ${\tau }^{\prime }=\tau$.

Stability of $\mathrm{\Pi }$ along ${\mathbf{p}}_A$ gives the stated type of $f[{\mathbf{p}}_A]$. Application with ${\mathbf{q}}_A:A[{\mathbf{p}}_A]$ then has codomain $B[{{\mathbf{p}}_A}^{+}][⟨\mathsf{id},{\mathbf{q}}_A⟩]$. By substitution composition this is $B[{{\mathbf{p}}_A}^{+}\circ ⟨\mathsf{id},{\mathbf{q}}_A⟩]$. Both components of the displayed composite are those of the identity substitution; Ext-Uniq gives ${{\mathbf{p}}_A}^{+}\circ ⟨\mathsf{id},{\mathbf{q}}_A⟩=\mathsf{id}$. Hence the application has type $B$, and abstraction makes the eta equation well typed.

From $\mathrm{\Gamma }.A.B$ to $\mathrm{\Gamma }.\mathrm{\Sigma }(A,B)$ use the projection to $\mathrm{\Gamma }$ and the pair of the two generic terms. In the reverse direction, project the generic pair to obtain its first component, extend by it, then extend by the second component transported into the resulting fiber. The two $\mathrm{\Sigma }$ beta laws prove both projection triangles; $\mathrm{\Sigma }$ eta and comprehension uniqueness prove the two composites are identities. Since both maps have first component the projection to $\mathrm{\Gamma }$, the isomorphism is over $\mathrm{\Gamma }$.

Let $\rho =⟨⟨⟨\mathsf{id},a⟩,b⟩,p⟩$ into the generic context and define ${\mathsf{J}}_{a,b,p}(C,d)=\mathsf{J}(C,d)[\rho ]$. Stability of generic $\mathsf{J}$ gives the displayed type. At $b=a,p={\mathsf{refl}}_a$, its computation equation is the generic beta equation followed by substitution. Conversely, instantiate the pointwise operation in the generic context at its three variables. Its assumed stability under every substitution supplies exactly the generic stability equation, so the resulting term is the CwF $\mathsf{J}$-structure.

For syntactic $\gamma :\mathrm{\Delta }\to \mathrm{\Gamma }$ and $a:A[\gamma ]$, the extension $⟨\gamma ,a⟩$ has projection $\gamma$ by Ext-Wk and generic component $a$ by Ext-Var. If $\delta :\mathrm{\Delta }\to \mathrm{\Gamma }.A$ has those two components, Ext-Uniq gives $\delta =⟨\gamma ,a⟩$. Passing to judgmental-equality classes makes the construction and the uniqueness equality well defined, which is item 4.

Choose a raw representative and induct mutually over contexts, substitutions, types, and terms. Empty context, identity, composition, projection, and extension are forced because both morphisms preserve the chosen CwF operations strictly. The $\mathrm{\Pi }$, application, and abstraction cases are likewise forced by preservation of the chosen $\mathrm{\Pi }$-structure; the induction hypotheses identify every argument. Both morphisms respect judgmental equality, so the result is independent of the representative and gives $F=G$ on all four quotient sorts.

Here $\mathrm{\Gamma }.A=\{(\rho ,a)\mid a\in A(\rho )\}$, $\mathbf{p}(\rho ,a)=\rho$, and $\mathbf{q}(\rho ,a)=a$. Thus $⟨\gamma ,a⟩(\delta )=(\gamma \delta ,a\delta )$: the two triangles, naturality, and $⟨\mathbf{p},\mathbf{q}⟩=\mathrm{id}$ are literal equalities of ordered pairs. Interpret $\mathrm{\Sigma }(A,B)(\rho )$ by $\sum _{a\in A(\rho )}B(\rho ,a)$, with ordinary pairing and projections. Their beta/eta laws are pair equalities, and reindexing acts componentwise, so every $\mathrm{\Sigma }$ operation is strictly stable.

The Grothendieck construction $\mathrm{\Gamma }.A$ has objects $(\rho ,a)$ and arrows $(u,\alpha ):(\rho ,a)\to ({\rho }^{\prime },a^{\prime })$ with $u:\rho \to {\rho }^{\prime }$ and $\alpha :A(u)(a)\to a^{\prime }$. A functor $F:\mathrm{\Delta }\to \mathrm{\Gamma }.A$ therefore projects to $\gamma =pF$ and its second components form a natural section of $A[\gamma ]$. Conversely a functor $\gamma$ and such a section assemble componentwise into $F$. The two constructions are inverse on objects and arrows, hence give the required bijection.

At $\rho$, take the Grothendieck groupoid $\mathrm{\Sigma }(A,B)(\rho )={\int }_{a:A(\rho )}B(\rho ,a)$. Pairing sends $(a,b)$ to its object; an arrow is the pair $(\alpha ,\beta )$ with $\beta$ lying over $\alpha$. The projections return $a$ and $b$, including their arrow components. Beta is componentwise, while eta sends $(a,b)$ and $(\alpha ,\beta )$ back to themselves. Reindexing applies the functors $A(u)$ and $B(u,-)$ to these components, so it commutes on the nose with pairing and both projections.

Induct on the type former over a discrete context. Empty, unit, Boolean, and natural groupoids are discrete. Products, dependent sums, and dependent products of discrete fibers are discrete because a natural isomorphism between their objects is componentwise an equality. The identity type is interpreted by a hom-set of a discrete groupoid, hence is empty or singleton. Thus every interpreted identity proof is unique and UIP holds. A universe is different: its objects are small groupoids and its arrows are equivalences, so it is not discrete; this is exactly the source of the counterexample.

Interpret a syntactic context $\mathrm{\Gamma }$ as its set of environments, a substitution $\gamma :\mathrm{\Delta }\to \mathrm{\Gamma }$ as the environment map $\rho \mapsto \gamma [\rho ]$, a type $A$ as the family $\rho \mapsto [[A{]]}_{\rho }$, and a term $a:A$ as the section $\rho \mapsto [[a{]]}_{\rho }$. The comprehension comparison is the literal bijection $$[[\mathrm{\Gamma }.A]]=\{(\rho ,u)\mid \rho \in [[\mathrm{\Gamma }]],u\in [[A{]]}_{\rho }\},$$ under which projection is first projection and the generic term is second projection. Induction over context, substitution, type, and term formation forces these four clauses and every constructor clause; hence any CwF morphism preserving the chosen structure agrees with this interpretation.