Chapter 156Core route

Coherence and Local Universes

Substitution in the syntax is strictly functorial: the type $A [γ] [δ]$ and the type $A [γ \circ δ]$ are the same type, because both are the result of the same textual operation. In the semantics they need not be the same object. A dependent type is often presented as a map into its base, reindexing as pullback along a substitution, and a pullback is determined only up to canonical isomorphism. Proposition 151.27 already exhibited a chosen pullback for which $δ^{*} (γ^{*} w)$ and $(γ \circ δ)^{*} w$ are distinct objects.

That gap is not repaired by choosing more carefully. The next section shows a type former — dependent products in the slices of $Set$ , the very structure proposition 151.25 constructed — for which the reindexing square commutes only up to isomorphism, and for which no choice makes it commute on the nose. So a category producing type formers up to isomorphism does not, by itself, interpret the judgmental equations $Θ ⊢ (Π (A, B)) [γ] [δ] \equiv Π (A [γ] [δ], B [γ^{+}] [δ^{+}]) type$ that the syntax proves by reflexivity. The question of this chapter is what extra data repairs this, and the answer is a construction: replace each type by a small classifying family together with a name, and reindex the name rather than the family.

A former that is stable only up to isomorphism

Example 156.1 — Chosen dependent products in slices ¶

Fix the standard pullback of proposition 151.27, $X \times_{Γ} Y : = {(x, y) ∣ u (x) = w (y)}$ , and define the chosen dependent product of $v : Z \to Y$ along $w : Y \to Γ$ by $Π_{w} (v) : = {(g, s) | g \in Γ, s : w^{- 1} (g) \to Z, v \circ s = {id}_{}} \overset{{pr}_{1}}{\to} Γ,$ as in proposition 151.25. Let $γ : Δ \to Γ$ and $δ : Θ \to Δ$ . Then $δ^{*} (γ^{*} Π_{w} (v)) and Π_{(γ \circ δ)^{*} w} ((γ \circ δ)^{*} v)$ are canonically isomorphic over $Θ$ and are not equal. Indeed an element of the first is a nested pair $(t, (δ (t), (γ (δ (t)), s)))$ with $s$ a section over the fibre $w^{- 1} (γ δ (t))$ , while an element of the second is a pair $(t, s^{'})$ with $s^{'}$ a section over the fibre of the pulled-back map, whose elements are themselves pairs. Already for $Θ = Δ = Γ = Y = Z = {0}$ with all maps the identity the two underlying sets are ${(0, (0, (0,!)))}$ and ${(0,!^{'})}$ with $!$ and $!^{'}$ sections of different maps, so the sets differ.

Referenced from 8 locations

Coherence and Local Universes

Remark 156.2 — No choice repairs it ¶

One might hope to choose pullbacks and products so that the displayed objects coincide. They cannot, for a reason of shape rather than of taste: the underlying set of $Π_{w} (v)$ mentions the fibres of $w$ , and pulling back changes those fibres to sets of pairs. A choice function on isomorphism classes would have to select, from each class, an object depending only on the class, while the two sides above depend on the route by which the class was reached. The repair below therefore does not choose better objects; it changes what a type is.

Referenced from 2 locations

Coherence and Local Universes

Comprehension categories and stability

Definition 156.3 — Comprehension category ¶

A comprehension category consists of a category $C$ , a cloven Grothendieck fibration $p : T \to C$ , and a functor $χ : T \to C^{\to}$ into the arrow category, sending cartesian arrows to pullback squares, such that $cod \circ χ = p$ strictly. It is split when $p$ is a split fibration, and full when $χ$ is full and faithful. All comprehension categories below are full. Objects of the fibre $T (Γ)$ are types over $Γ$ , and $χ (A) : Γ . A \to Γ$ is the display map of $A$ . A map in $C$ isomorphic to some $χ (A)$ is a display map.

Referenced from 3 locations

Coherence and Local Universes

Splitness is exactly the property the syntax has and example 156.1 lacks: in a split fibration the chosen cartesian lifts compose on the nose, so $A [γ] [δ] = A [γ \circ δ]$ as objects.

Definition 156.4 — Weak and strict stability ¶

Let $C = (C, T, p, χ)$ be a comprehension category.

An identity type for $A \in T (Γ)$ is a type ${Id}_{A} \in T (Γ . A . A)$ , a factorization $r_{A} : Γ . A \to Γ . A . A . {Id}_{A}$ of the diagonal $Δ_{A} : Γ . A \to Γ . A . A$ , and, for every $C \in T (Γ . A . A . {Id}_{A})$ and every $d : Γ . A \to Γ . A . A . {Id}_{A} . C$ over $r_{A}$ , a diagonal filler $j_{A, C, d} : Γ . A . A . {Id}_{A} \to C$ making both triangles commute.
A choice of identity types assigns one to every $Γ, A$ . It is strictly stable when for every $σ : Γ^{'} \to Γ$ ${Id}_{A} [σ] = {Id}_{A [σ]}, r_{A} [σ] = r_{A [σ]}, j_{A, C, d} [σ] = j_{A [σ], C [σ], d [σ]} .$
A weakly stable identity type for $A$ is a pair $({Id}_{A}, r_{A})$ as in (1) such that for every $σ : Γ^{'} \to Γ$ there exists some $j$ making $({Id}_{A} [σ], r_{A} [σ], j)$ an identity type for $A [σ]$ . $C$ has weakly stable identity types when every $Γ, A$ admits one.

The analogous definitions for $Π$ , $Σ$ , $0$ , $1$ , binary sums and $W$ replace $(Id, r)$ by the type former with its constructors and $j$ by the eliminator.

Referenced from 5 locations

Coherence and Local Universes

Lemma 156.5 — Strict stability is what the syntax needs ¶

Let $C$ be split with a strictly stable choice of the formers of a signature $T$ . Then the interpretation of theorem 54.28 applies: derivable judgmental equalities of $T$ become equalities of semantic data. If instead the choice is only weakly stable, the interpretation of a derivation is not well defined on judgments in general.

Referenced from 3 locations

Coherence and Local Universes

Proof of Lemma 156.5 — Strict stability is what the syntax needs

Proof. For the first claim, splitness gives strict functoriality of reindexing and the stability equations give the former-wise substitution equations; these are exactly the clauses required by definition 116.28, so the induction of theorem 54.28 goes through. For the second, take the substitution rule for $Π$ : two derivations of $Θ ⊢ (Π (A, B)) [γ] [δ] type$ , one applying substitution twice and one applying it once to the composite, are sent to the two objects of example 156.1, which are distinct. A function on judgments would have to give them one value. ◻

Local universes

The construction replaces a type over $Γ$ by a type over an auxiliary object together with a name: a map from $Γ$ that selects it. Reindexing then acts on the name only, and names compose strictly because they are arrows.

Definition 156.6 — The comprehension category C_!¶

Let $C = (C, T, p, χ)$ be a full comprehension category. Define $C_{!} = (C, T_{!}, p_{!}, χ_{!})$ by:

base: the same category $C$ ;
types: an object of $T_{!} (Γ)$ is a triple $A = (V_{A}, E_{A}, ⌜ A ⌝)$ with $V_{A} \in C$ , $E_{A} \in T (V_{A})$ and $⌜ A ⌝ : Γ \to V_{A}$ an arrow of $C$ . Write $[A] : = E_{A} [⌜ A ⌝] \in T (Γ)$ . An arrow $B \to A$ over $σ : Δ \to Γ$ is an arrow $[B] \to [A]$ over $σ$ in $T$ ;
reindexing: $A [σ] : = (V_{A}, E_{A}, ⌜ A ⌝ \circ σ)$ , with the cartesian arrow $A [σ] \to A$ the canonical one supplied by cartesianness of $E_{A}$ over $⌜ A ⌝$ ;
comprehension: $χ_{!} (A) : = χ ([A])$ .

Referenced from 7 locations

Coherence and Local Universes

Lemma 156.7 — C_! is a split full comprehension category ¶

$p_{!}$ is a split fibration, $χ_{!}$ is full and faithful and sends cartesian arrows to pullback squares, and $cod \circ χ_{!} = p_{!}$ .

Referenced from 7 locations

Coherence and Local Universes

Proof of Lemma 156.7 — C_! is a split full comprehension category

Proof. Splitness is the point of the definition: for $σ : Δ \to Γ$ and $τ : Θ \to Δ$ , $(A [σ]) [τ] = (V_{A}, E_{A}, (⌜ A ⌝ \circ σ) \circ τ) = (V_{A}, E_{A}, ⌜ A ⌝ \circ (σ \circ τ)) = A [σ \circ τ],$ because composition in $C$ is strictly associative; and $A [{id}_{Γ}] = A$ because ${id}_{}$ is a strict unit. The lifts are cartesian because they are the canonical comparisons of cartesian arrows in $T$ , and they compose to the canonical comparison for the composite by uniqueness of such comparisons. Fullness and faithfulness of $χ_{!}$ follow from those of $χ$ , since an arrow of $T_{!}$ over $σ$ was defined to be an arrow of $T$ between the associated types; and cartesian arrows of $T_{!}$ are sent to the same squares as the corresponding cartesian arrows of $T$ . ◻

Example 156.8 — Reindexing computed ¶

Take $C = Set$ , $T$ the codomain fibration, and let $A$ over $Γ$ be presented by $V_{A} : = Γ$ , $E_{A} : = χ (A)$ and $⌜ A ⌝ : = {id}_{Γ}$ . For $γ : Δ \to Γ$ and $δ : Θ \to Δ$ , $(A [γ]) [δ] = (Γ, E_{A}, γ \circ δ) = A [γ \circ δ],$ an equation of triples, whereas the associated types $[(A [γ]) [δ]]$ and $[A [γ \circ δ]]$ are computed by one pullback along $γ \circ δ$ in both cases. Contrast example 156.1: there the two routes built different objects, because the object was recomputed at each step; here only the name was recomputed.

Referenced from 3 locations

Coherence and Local Universes

Definition 156.9 — Dependent exponentials and condition (LF)¶

For maps $Z \overset{g}{\to} Y \overset{f}{\to} X$ with all pullbacks of $f$ existing, a dependent exponential of $f$ and $g$ is an object $\prod_{f} g$ of $C / X$ together with a bijection ${hom}_{C / X} (W, \prod_{f} g) ≅ {hom}_{C / Y} (W \times_{X} Y, Z),$ natural in $W$ . Say $C$ satisfies condition (LF) when its underlying category has finite products and, whenever $f$ is a display map and $g$ is either a display map or a product projection, the dependent exponential $\prod_{f} g$ exists.

Referenced from 6 locations

Coherence and Local Universes

Proposition 156.10 — Sufficient conditions ¶

Each of the following implies (LF):

$C$ has finite products and every display map is exponentiable;
every map $X \to 1$ is a display map, and each reindexing functor $χ (A)^{*} : T (Γ) \to T (Γ . A)$ has a right adjoint;
$C$ is locally cartesian closed.

Referenced from 3 locations

Coherence and Local Universes

Proof of Proposition 156.10 — Sufficient conditions

Proof. (3) implies (1) because in a locally cartesian closed category every map is exponentiable and finite products exist. (1) implies (LF): a product projection $Z \to Y$ is the pullback of $Z \times Y \to Y$ along the diagonal, so exponentiability of $f$ gives the required right adjoint at the two cases allowed by definition 156.9. (2) implies (LF): the hypothesis makes every object fibrant, so slices of $C$ are recovered as fibres of $T$ , and the stated right adjoints are exactly the dependent exponentials required. ◻

Remark 156.11 — The exponentials are not object-theory function types ¶

Condition (LF) asks for categorical exponentials in $C$ , and does not require them to be display maps. It is therefore independent of whether the type theory being modelled has function types, and it is not implied by the object theory having them: type-theoretic $Π$ -types satisfying only a weak universal property need not be categorical exponentials.

Referenced from 3 locations

Coherence and Local Universes

Lifting structure to the split replacement

The pattern is uniform. Given local universes for the type premises of a rule, construct one object $V$ representing the remaining premise data; an instance of the premises over $Γ$ is then an arrow $Γ \to V$ , there is a universal instance over $V$ itself, and the operation is performed once, on that universal instance. The result over $Γ$ is obtained by composing with the arrow. Only the arrow mentions $Γ$ , and composition of arrows is strict; hence strict stability.

Construction 156.12 — Binary sums ¶

Let $C$ have weakly stable binary sums. For $A_{1} = (V_{A_{1}}, E_{A_{1}}, ⌜ A_{1} ⌝)$ and $A_{2} = (V_{A_{2}}, E_{A_{2}}, ⌜ A_{2} ⌝)$ in $T_{!} (Γ)$ put $\begin{aligned} V_{A_{1} + A_{2}} & : = V_{A_{1}} \times V_{A_{2}}, & E_{A_{1} + A_{2}} & : = E_{A_{1}} [π_{1}] + E_{A_{2}} [π_{2}], \\ ⌜ A_{1} + A_{2} ⌝ & : = ⟨ ⌜ A_{1} ⌝, ⌜ A_{2} ⌝ ⟩ . \end{aligned}$

Referenced from 5 locations

Coherence and Local Universes

Lemma 156.13 — Sums are strictly stable in C_!¶

Construction 156.12 defines binary sums in $C_{!}$ , and they are strictly stable.

Referenced from 3 locations

Coherence and Local Universes

Proof of Lemma 156.13 — Sums are strictly stable in C_!

Proof. The two projections $π_{i}$ let both $E_{A_{i}}$ be pulled back to $V_{A_{1}} \times V_{A_{2}}$ , where the weakly stable sum of $C$ is formed once. Its universal property is retained after reindexing along $⌜ A_{1} + A_{2} ⌝$ precisely because the sum was chosen weakly stably. For stability, let $σ : Δ \to Γ$ . The universe and the type component of $(A_{1} + A_{2}) [σ]$ are $V_{A_{1}} \times V_{A_{2}}$ and $E_{A_{1}} [π_{1}] + E_{A_{2}} [π_{2}]$ , unchanged, while the name is $⟨ ⌜ A_{1} ⌝, ⌜ A_{2} ⌝ ⟩ \circ σ = ⟨ ⌜ A_{1} ⌝ \circ σ, ⌜ A_{2} ⌝ \circ σ ⟩ = ⌜ A_{1} [σ] + A_{2} [σ] ⌝$ , an equation of arrows. Hence $(A_{1} + A_{2}) [σ] = A_{1} [σ] + A_{2} [σ]$ on the nose. ◻

Construction 156.14 — The universe of dependent families ¶

Assume (LF). For local universes $(V_{A}, E_{A})$ and $(V_{B}, E_{B})$ put $V_{A} / V_{B} : = \sum_{V_{A}} \prod_{E_{A}} ((V_{A} . E_{A}) \times V_{B} \to V_{A} . E_{A}),$ the dependent exponential of the display map of $E_{A}$ with the projection, summed over $V_{A}$ ; in the internal notation of (LF) this is $V_{A} / V_{B} = [a : V_{A}, b : V_{B}^{E_{A} (a)}] .$ Write $π_{A} : V_{A} / V_{B} \to V_{A}$ and $π_{B} : (V_{A} / V_{B}) . E_{A} [π_{A}] \to V_{B}$ for the two arrows corresponding to the identity of $V_{A} / V_{B}$ .

Referenced from 4 locations

Coherence and Local Universes

Lemma 156.15 — The representing property ¶

For every $Γ$ the assignment $h \mapsto (π_{A} \circ h, π_{B} \circ h^{+})$ is a bijection between arrows $h : Γ \to V_{A} / V_{B}$ and pairs of arrows $⌜ A ⌝ : Γ \to V_{A}$ and $⌜ B ⌝ : Γ . E_{A} [⌜ A ⌝] \to V_{B}$ , natural in $Γ$ .

Referenced from 4 locations

Coherence and Local Universes

Proof of Lemma 156.15 — The representing property

Proof. Unfold definition 156.9: arrows $Γ \to \sum_{V_{A}} W$ are pairs of an arrow $⌜ A ⌝ : Γ \to V_{A}$ and an arrow into $W$ over it, and arrows into $\prod_{E_{A}} (-)$ over $⌜ A ⌝$ correspond by the displayed bijection to arrows out of the pullback $Γ \times_{V_{A}} (V_{A} . E_{A})$ , which is $Γ . E_{A} [⌜ A ⌝]$ because $χ$ sends cartesian arrows to pullbacks. Naturality in $Γ$ is the naturality clause of definition 156.9 together with functoriality of the pullback. Taking $Γ = V_{A} / V_{B}$ and $h = {id}_{}$ names the universal pair, which is $(π_{A}, π_{B})$ . ◻

Construction 156.16 — Dependent products ¶

Let $C$ have weakly stable $Π$ -types and satisfy (LF). For $A \in T_{!} (Γ)$ and $B \in T_{!} (Γ . A)$ put $\begin{aligned} V_{Π (A, B)} & : = V_{A} / V_{B}, & E_{Π (A, B)} & : = Π (E_{A} [π_{A}], E_{B} [π_{B}]), \\ ⌜ Π (A, B) ⌝ & : = h, \end{aligned}$ where $h : Γ \to V_{A} / V_{B}$ is the arrow corresponding by lemma 156.15 to the pair $(⌜ A ⌝, ⌜ B ⌝)$ , and $Π$ on the right is the weakly stable former of $C$ applied to the universal instance.

Referenced from 5 locations

Coherence and Local Universes

Theorem 156.17 — Π is strictly stable in C_!¶

Construction 156.16 equips $C_{!}$ with a choice of $Π$ -types satisfying the formation, introduction, elimination and computation rules, and for every $σ : Δ \to Γ$ , $Π (A, B) [σ] = Π (A [σ], B [σ^{+}]) .$

Referenced from 6 locations

Coherence and Local Universes

Proof of Theorem 156.17 — Π is strictly stable in C_!

Proof. The former is well defined. Over $V_{A} / V_{B}$ the pair $(π_{A}, π_{B})$ is a universal instance of the premises, so $E_{A} [π_{A}]$ and $E_{B} [π_{B}]$ are types over $V_{A} / V_{B}$ and over its extension; the weakly stable $Π$ of $C$ applies. Reindexing that type along $h$ gives, by weak stability, a type over $Γ$ still satisfying the universal property of a $Π$ -type for $[A]$ and $[B]$ : this is exactly what definition 156.4(3) provides, and it is the only place weak stability is used. Introduction, elimination and computation are the operations of that retained universal property.

Strict stability. The universe and type components of $Π (A, B)$ do not mention $Γ$ ; only $⌜ Π (A, B) ⌝ = h$ does. By definition 156.6, $Π (A, B) [σ]$ has the same first two components and name $h \circ σ$ . By naturality in lemma 156.15, $h \circ σ$ is the arrow corresponding to the pair $(⌜ A ⌝ \circ σ, ⌜ B ⌝ \circ σ^{+})$ , which is the pair of names of $A [σ]$ and $B [σ^{+}]$ . Hence the two sides have the same three components and are equal. ◻

Theorem 156.18 — Coherence ¶

Let $C$ be a full comprehension category satisfying condition (LF). If $C$ has weakly stable binary sums, respectively $Π$ -types, identity types, $Σ$ -types, zero types, unit types, or $W$ -types relative to a stable class of $Π$ -types, then its split replacement $C_{!}$ has a strictly stable choice of the corresponding structure, and therefore models the syntax of type theory with that structure.

Referenced from 11 locations

Coherence and Local Universes

Proof of Theorem 156.18 — Coherence

Proof. $C_{!}$ is split by lemma 156.7. For each former the argument has the shape of theorem 156.17: build an object $V$ representing the non-type premises of the rule using (LF) — products for sums (construction 156.12), $V_{A} / V_{B}$ for $Π$ , $Σ$ and $W$ (construction 156.14), $V_{A}$ itself for identity, zero and unit types — apply the weakly stable structure of $C$ to the universal instance over $V$ , and take the name to be the arrow $Γ \to V$ classifying the actual premises. In each case:

the universal property survives reindexing along the name, by weak stability;
for a term former one additionally reindexes the resulting arrow from $T (V)$ to $T (Γ)$ , which is an operation on arrows and hence strictly natural in $Γ$ ;
the components not equal to the name are independent of $Γ$ , and the name composes strictly, so all the stability equations of definition 156.4(2) hold on the nose.

For $W$ -types the representing object is built with the same $V_{A} / V_{B}$ , and the hypothesis that the $Π$ -types used in its construction come from a stable class is what makes the universal instance available; without it the object $V$ is not defined. Finally lemma 156.5 turns the strictly stable choice into an interpretation of the syntax. ◻

Corollary 156.19 — The slice interpretation is repaired ¶

Let $C$ be locally cartesian closed with $T$ the codomain fibration. Then $C_{!}$ is a split full comprehension category with strictly stable $Π$ , $Σ$ , unit and identity types; in particular the interpretation of proposition 151.25 in $Set$ yields, after the replacement, a model in which the judgmental equation $Θ ⊢ (Π (A, B)) [γ] [δ] \equiv Π (A [γ] [δ], B [γ^{+}] [δ^{+}]) type$ holds as an equality of semantic types.

Referenced from 4 locations

Coherence and Local Universes

Proof of Corollary 156.19 — The slice interpretation is repaired

Proof. Local cartesian closure gives (LF) by proposition 156.10(3), and the codomain fibration of a locally cartesian closed category has weakly stable $Π$ , $Σ$ , unit and identity types — the last by factoring the diagonal through the object of paths in the slice, whose fillers exist for each reindexing. Apply theorem 156.18. The displayed equation is then an instance of the stability equation of theorem 156.17 applied twice, since names compose strictly by lemma 156.7. ◻

Remark 156.20 — The rule that was at risk ¶

Before the replacement, the substitution rule for $Π$ was in the following position: syntactically it is an instance of reflexivity, since substitution is defined by recursion and both sides are the same expression; semantically example 156.1 produced two distinct objects. A model validating only an isomorphism between them cannot interpret a derivation that uses the rule silently — and every derivation does, because substitution is applied without ceremony. Corollary 156.19 removes the risk by exhibiting a model in which the two sides are literally equal. It does not weaken the rule, and it does not replace the isomorphism by a further axiom: it changes the objects so that the isomorphism is an identity.

Referenced from 3 locations

Coherence and Local Universes

Exercise 156.1 ¶

★☆☆ Verify lemma 156.7 for a three-fold composite: show $((A [σ]) [τ]) [ρ] = A [σ \circ τ \circ ρ]$ directly from definition 156.6, and say which property of $C$ is used.

Referenced from 2 locations

Coherence and Local Universes

Exercise 156.2 ¶

★★☆ Show that construction 156.12 requires the finite products demanded by condition (LF): exhibit a comprehension category with weakly stable binary sums but without binary products in the base, and locate the step of lemma 156.13 that fails.

Referenced from 2 locations

Coherence and Local Universes

Exercise 156.3 ¶

★★☆ In the proof of theorem 156.17, weak stability is used exactly once. Identify the step, and show by an example that the conclusion fails if $C$ has $Π$ -types that are not weakly stable: give $Γ$ , $A$ , $B$ and a $σ$ for which the reindexed type loses the universal property.

Referenced from 2 locations

Coherence and Local Universes

Exercise 156.4 ¶

★★☆ Carry out the construction of theorem 156.18 for identity types: name the representing object, write down the universal instance, and check the three stability equations of definition 156.4(2) explicitly.

Referenced from 2 locations

Coherence and Local Universes

Extensions, natural models, and boundary

Theorem 156.18 lists the formers it covers, and each is covered by the construction actually carried out for it. Three extensions are frequently wanted and each requires its own hypotheses. Higher inductive structure needs a representing object for its point and path constructors together, and the argument applies only at signatures for which such an object exists. A universe in the object theory is not automatically strictly stable after the replacement: a universe is a type, so it acquires a local universe of its own, and the decoding must be shown stable, which is an extra verification. Strict equality in the object theory — a former whose elimination produces judgmental equations — may be treated by the same pattern, but it must not be used to prove the external theorem: the internal strict equality of a model is a statement inside the object theory, whereas theorem 156.18 is a statement about the model, and conflating them would make the coherence argument circular.

Remark 156.21 — When natural models are the shorter route ¶

A comprehension category can be presented equivalently by a single representable natural transformation of presheaves, and in that presentation the data of definition 156.6 become a factorization of that transformation. This is sometimes the more economical way to state a single construction, and where it is, the operation should be translated back into the comprehension-category language used above rather than left in a second formalism. A general dictionary between presentations is not needed here: no result of this chapter is proved by comparing formalisms [Awo18, CCD21].

Referenced from 2 locations

Coherence and Local Universes

The results are lemma 156.7, theorem 156.17, theorem 156.18 and corollary 156.19. Their boundaries are these. Condition (LF) is a hypothesis of the theorem and is used to build every representing object; by remark 156.11 it is a condition on the ambient category, not on the object theory. Weak stability is a hypothesis about the structure being lifted, used once per former. The theorem produces a model of the syntax with the listed formers and nothing else: a former absent from the list is absent from the conclusion. And the construction changes the model, not the syntax: it neither adds nor removes a rule, and by remark 156.20 its effect is to make an equation that the syntax already proved into an equality of semantic objects.

The proof base is Lumsdaine and Warren’s local-universes construction, from which definition 156.6, definition 156.9, construction 156.14 and the statement of theorem 156.18 are taken with their hypotheses intact; the comprehension-category framework and the fibrational vocabulary of definition 156.3 follow [Jac99]; the precise comparison of split and non-split presentations, used implicitly whenever a model is said to be “the same” as a category with families, is [CCD21]; and the survey framing of the strictness problem is [Hof97, AG26]. The coherence result for strict equalities and its mechanization are [Boc25]; it is cited for the comparison in section 156.5 only, and no theorem of this chapter depends on it.

[4]

Suggested first pass.

Begin with exercise 156.5, then exercise 156.6, and finish with exercise 156.8.

Exercise 156.5 ¶

★★★ Take $C$ to be groupoids with $T$ the fibration of isofibrations. Show that $C$ satisfies condition (LF) and has weakly stable identity types, using the path object of proposition 152.26. Conclude from theorem 156.18 that the split replacement models identity types strictly, and compare the result with the direct construction of proposition 152.10: which one chooses the eliminator, and which one only asserts that a choice exists?

Referenced from 3 locations

Coherence and Local Universes

Exercise 156.6 ¶

★★★ Suppose $C$ carries a universe: an object $U$ with a display map $El \to U$ such that every display map in a certain class is a pullback of it. Formulate strict stability for the decoding operation, and show that $C_{!}$ inherits it provided the classifying arrows are chosen functorially. Then exhibit a choice for which stability fails.

Referenced from 3 locations

Coherence and Local Universes

Exercise 156.7 ¶

★★☆ The local universe $V_{A}$ of a type may be much larger than the type itself. Show that in example 156.8 one may always take $V_{A} = Γ$ , and give an example in which every choice of $V_{A}$ that makes construction 156.16 work is strictly larger than $Γ$ . What does this say about the size assumptions needed to run theorem 156.18?

Referenced from 2 locations

Coherence and Local Universes

Exercise 156.8 — Practical: a strictness checker ¶

★★★ Practical project.local-universe-strictness-checker Implement, for the category of finite sets and functions with the codomain fibration, two representations of a dependent type over a base: the direct one, a display map with chosen pullbacks, and the local-universe one, a triple $(V_{A}, E_{A}, ⌜ A ⌝)$ as in definition 156.6. Implement reindexing for both, and the chosen $Π$ of example 156.1 for the direct representation and construction 156.16 for the replacement. The invariant the program must maintain is that it compares objects by identity of the represented data, never by the existence of a bijection, and that it reports an isomorphism separately from an equality. The program must print, for each named input, the two objects obtained by the two reindexing routes, whether they are equal, and whether they are isomorphic. The acceptance test is: for the direct representation and the data of example 156.1 the two routes print isomorphic: yes and equal: no; for the local-universe representation on the same data they print equal: yes; the reindexing of a name along a composite prints the same triple as the two-step reindexing, matching lemma 156.7; and the underlying types $[A]$ agree in all four cases, showing that the replacement changed the presentation and not the type. A finite-set checker is evidence on named inputs; it does not prove theorem 156.18, and it does not test condition (LF), which is automatic for finite sets.

Referenced from 3 locations