Set and CwF Models of Type Theory

Proof. ${\kappa }_{\omega }$ is a limit of inaccessibles, hence itself a limit cardinal closed under power set and replacement, so ${\mathcal{V}}_{\omega }$ is a model of ZFC minus replacement in the ambient universe and is closed under pairing, power set, union and functions between its elements. A family $A:\mathrm{\Gamma }\to {\mathcal{V}}_{\omega }$ is a subset of $\mathrm{\Gamma }\times {\mathcal{V}}_{\omega }$ whose domain is $\mathrm{\Gamma }\in {\mathcal{V}}_{\omega }$; since $\mathrm{\Gamma }$ has rank below ${\kappa }_{\omega }$ and ${\kappa }_{\omega }$ is regular, the image of $A$ is bounded, so $A\in {\mathcal{V}}_{\omega }$ and $\mathrm{Ty}(\mathrm{\Gamma })\subseteq {\mathcal{V}}_{\omega }$ is again an element of ${\mathcal{V}}_{\omega }$. The set $\mathrm{\Gamma }.A$ is a subset of $\mathrm{\Gamma }\times \bigcup _{g}A(g)$, and $\mathrm{Tm}(\mathrm{\Gamma },A)$ is a subset of the function set $\mathrm{\Gamma }\to \bigcup _{g}A(g)$; both are formed by operations under which ${\mathcal{V}}_{\omega }$ is closed. ◻

Proof. All four are the associativity and unit laws for composition of functions, which hold as equalities of sets of pairs. For the second, both sides are the function sending $t\in \mathrm{\Theta }$ to $A(\gamma (\delta (t)))$, and two functions with the same domain and the same values are equal. The typing of the fourth clause is the third clause applied to $A$: $a[\gamma ]$ has values $a(\gamma (d))\in A(\gamma (d))=A[\gamma ](d)$, so $a[\gamma ]\in \mathrm{Tm}(\mathrm{\Delta },A[\gamma ])$, and both sides of the equation are $t\mapsto a(\gamma (\delta (t)))$. ◻

Proof. Well-definedness: $a(d)\in A[\gamma ](d)=A(\gamma (d))$, so $(\gamma (d),a(d))\in \mathrm{\Gamma }.A$. The two equations are computed pointwise: Uniqueness: suppose $h:\mathrm{\Delta }\to \mathrm{\Gamma }.A$ satisfies both equations. Every element of $\mathrm{\Gamma }.A$ is a pair, so $h(d)=({\mathbf{p}}_A(h(d)),{\mathbf{q}}_A(h(d)))=(\gamma (d),a(d))=⟨\gamma ,a⟩(d)$. ◻

Proof. Unfolding definition 54.19, ${\gamma }^{+}(d,x)=(\gamma (d),x)$, which is well typed because $x\in A[\gamma ](d)=A(\gamma (d))$. The square commutes. Given $u:\mathrm{\Theta }\to \mathrm{\Delta }$ and $v:\mathrm{\Theta }\to \mathrm{\Gamma }.A$ with ${\mathbf{p}}_A\circ v=\gamma \circ u$, write $v(t)=(\gamma (u(t)),x_t)$ with $x_t\in A(\gamma (u(t)))=A[\gamma ](u(t))$ and put $w(t):=(u(t),x_t)$. Then $w$ is the unique map with ${\mathbf{p}}_{A[\gamma ]}\circ w=u$ and ${\gamma }^{+}\circ w=v$, since these two equations determine both components of $w(t)$. ◻

Proof. Functions and their composition form a category with the singleton as terminal object; lemma 151.4 places all data in ${\mathcal{V}}_{\omega }$; lemma 151.5 gives the four functoriality equations; and lemma 151.6 gives comprehension with its universal property. ◻

Proof. Typing: if $b\in \mathrm{Tm}(\mathrm{\Gamma }.A,B)$ then $b(g,x)\in B(g,x)$, so $\lambda (b)(g)\in \mathrm{\Pi }(A,B)(g)$. $\beta$: for $a\in \mathrm{Tm}(\mathrm{\Gamma },A)$, $$\mathsf{app}(\lambda (b),a)(g)=\lambda (b)(g)(a(g))=b(g,a(g))=b[⟨\mathsf{id},a⟩](g),$$ using lemma 151.6 for the last step. $\eta$: for $f\in \mathrm{Tm}(\mathrm{\Gamma },\mathrm{\Pi }(A,B))$ the function $\lambda (\mathsf{app}(f[{\mathbf{p}}_A],{\mathbf{q}}_A))(g)$ sends $x$ to $f(g)(x)$, and a function is determined by its values, so this is $f(g)$. Stability: for $\gamma :\mathrm{\Delta }\to \mathrm{\Gamma }$, $$\mathrm{\Pi }(A,B)[\gamma ](d)=\mathrm{\Pi }(A,B)(\gamma (d))=\mathrm{\Pi }(A[\gamma ],B[{\gamma }^{+}])(d),$$ because $B[{\gamma }^{+}](d,x)=B(\gamma (d),x)$ by the formula for ${\gamma }^{+}$ in lemma 151.7; both sides are literally the same set of functions. The $\mathrm{\Sigma }$-clauses are the same calculation with pairs, and the surjective-pairing equation holds because every element of $\mathrm{\Sigma }(A,B)(g)$ is a pair. ◻

Proof. $\mathbf{0}$: a term of $\mathrm{Tm}(\mathrm{\Gamma }.[[\mathbf{0}]],C)$ is a function on the empty set $\mathrm{\Gamma }.[[\mathbf{0}]]=\mathrm{\varnothing }$, and the empty function is the unique such, so the eliminator exists and its uniqueness equation is vacuous. $\mathbb{N}$: the displayed clauses define a function on $\mathbb{N}$ by ordinary recursion in the metatheory; its two computation equations are the two clauses read at $n=0$ and $n=m+1$. Stability is immediate because the interpreting families are constant in $g$ and reindexing is precomposition. $\mathbf{2}$ and $\mathbf{1}$ are the finite cases of the same argument. ◻

Proof. Existence of the set: let $T_0:=\mathrm{\varnothing }$ and $T_{\alpha +1}:=\{(x,t)\mid x\in A(g)$ and $t:B(g,x)\to T_{\alpha }\}$, taking unions at limits. The sequence is increasing, and by replacement it stabilises at some ordinal below the cardinality of the ambient stage; put $\mathsf{W}(A,B)(g):=\bigcup _{\alpha }{T}_{\alpha }$. It is an element of ${\mathcal{V}}_{\omega }$ by lemma 151.4 applied to each stage. The eliminator: given $c\in \mathrm{Tm}({\mathrm{\Gamma }}^{\prime },C^{\prime })$ interpreting the step, define $e(\mathsf{sup}(x,t)):=c(x,t,\lambda y.e(t(y)))$ by recursion on the least $\alpha$ with $\mathsf{sup}(x,t)\in T_{\alpha }$; this is well founded because $t(y)\in T_{\beta }$ for some . The computation rule is the defining clause read backwards. ◻

Proof. $\mathsf{J}$: let $C\in \mathrm{Ty}({\mathrm{\Gamma }}_A.{\mathsf{Id}}_A)$ and let $d$ be a section of $C$ over the diagonal. An element of the domain of $\mathsf{J}$ is a tuple $(g,x,y,p)$ with $p\in {\mathsf{Id}}_A(g,x,y)$; the fibre is nonempty only when $x=y$, in which case $p=\star$ and the tuple is literally $(g,x,x,\star )$. Put $\mathsf{J}(C,d)(g,x,y,p):=d(g,x)$. This is well typed because the tuple equals the diagonal tuple, and its computation rule $\mathsf{J}(C,d)[r_A]=d$ holds because the two sides have the same values. Reflection: if $\mathrm{Tm}(\mathrm{\Gamma },{\mathsf{Id}}_A(a,b))$ is nonempty then $a(g)=b(g)$ for every $g$, hence $a=b$ as functions, which is exactly the semantic content of $\mathrm{\Gamma }⊢a\equiv b:A$. Uniqueness: every element of a nonempty fibre is $\star$, so any two terms of an identity type are equal. ◻

Proof. Stability holds because ${\mathcal{U}}_i$ is constant and $\mathsf{El}(-)$ is evaluation. For closure under $\mathrm{\Pi }$, let $X\in {\mathcal{V}}_i$ and $Y:X\to {\mathcal{V}}_i$; the set $\prod _{x\in X}Y(x)$ is a subset of the function set $X\to \bigcup _{x}Y(x)$. Regularity of ${\kappa }_i$ makes $\bigcup _{x}Y(x)$ an element of ${\mathcal{V}}_i$, since it is a union of fewer than ${\kappa }_i$ sets each of rank below ${\kappa }_i$; and the strong limit property makes the function set an element of ${\mathcal{V}}_i$, since whenever . Both properties are exactly strong inaccessibility. If ${\kappa }_i$ were a strong limit but singular — ${\beth }_{\omega }$, say — the union step fails: choose $X=\omega$ and $Y(n)$ of rank cofinal in ${\kappa }_i$. Closure under $\mathrm{\Sigma }$ and $\mathsf{W}$ uses the same two properties, and closure under $\mathsf{Id}$ is trivial since its values are subsingletons. ◻

Proof. $\mathcal{S}$ is a CwF by proposition 151.8 and carries every former of ${\mathcal{T}}_{\mathsf{S}}$ by proposition 151.11, proposition 151.12, proposition 151.13, proposition 151.14, proposition 151.16, with all equations strict. It is therefore a model of the signature in the sense of definition 116.28, and theorem 54.27 supplies the unique morphism. Clauses (1)–(4) are the definition of a strict CwF-morphism (definition 54.26) together with theorem 54.28: judgmental equality in $\mathcal{T}$ is equality of elements, and a function preserves equality. ◻

Proof. Such a derivation would give $[[e]]\in \mathrm{Tm}(\mathbf{1},[[\mathbf{0}]])$ by theorem 151.17. By proposition 151.12 that set consists of the functions $h$ on the singleton $\mathbf{1}$ with $h(\star )\in \mathrm{\varnothing }$, and there are none. ◻

Proof. For the first, proposition 151.14 gives $[[{\mathsf{Id}}_{\mathbf{2}}(\mathsf{tt},\mathsf{ff})]](\star )=\{\star \mid \mathsf{tt}=\mathsf{ff}\}=\mathrm{\varnothing }$ because $\mathsf{tt}$ and $\mathsf{ff}$ are distinct elements of the interpreting set; argue as in corollary 151.18. For the second, clause (4) of theorem 151.17 would force $[[\mathsf{tt}]]=[[\mathsf{ff}]]$, that is $\mathsf{tt}=\mathsf{ff}$. ◻

Proof. By the last sentence of proposition 151.14, $\mathcal{S}$ models the extended signature; repeat the argument of corollary 151.18 with the term model of ${\mathcal{T}}_{\mathsf{S}}^{=}$ in place of $\mathcal{T}$. ◻

Proof. By proposition 151.14, ${\mathsf{Id}}_A(g,x,y)$ is $\{\star \}$ or $\mathrm{\varnothing }$. A term of $\mathsf{UIP}$ must, for every $X\in {\mathcal{V}}_0$, every $x,y\in X$ and every $p,q$ in a fibre, produce an element of $\{\star \mid p=q\}$; and if the fibre containing $p$ and $q$ is nonempty then $p=q=\star$, so the required element is $\star$. The constant function with value $\star$ is therefore a section, and it is stable under reindexing because it is constant. A model in which a type is inhabited proves nothing about the underivability of that type. ◻

Proof. By lemma 116.32 the interpretation factors through the quotient by judgmental equality, so it is a function of the judgment; uniqueness of the morphism in theorem 151.17 then leaves no room for a second value. ◻

Proof. The two assignments are mutually inverse up to isomorphism over $\mathrm{\Gamma }$: for a family $A$, the fibre of ${\mathbf{p}}_A$ over $g$ is $\{g\}\times A(g)$, and $(g,x)\mapsto x$ is a bijection onto $A(g)$ natural in $g$; for $u:X\to \mathrm{\Gamma }$, the map $x\mapsto (u(x),x)$ is a bijection over $\mathrm{\Gamma }$ from $X$ to $\mathrm{\Gamma }.(g\mapsto u^{-1}(g))$. The composite comparisons are identities on the nose in one direction and the displayed bijections in the other. ◻

Proof. Adjointness of ${\mathrm{\Sigma }}_{\gamma }$: an arrow $\gamma \circ u\to w$ over $\mathrm{\Gamma }$ is a function commuting with the structure maps, and this is literally an arrow $u\to {\gamma }^{\ast }w$ over $\mathrm{\Delta }$. Adjointness of ${\mathrm{\Pi }}_{\gamma }$: an arrow ${\gamma }^{\ast }w\to v$ over $\mathrm{\Delta }$ assigns to each $d\in \mathrm{\Delta }$ and each element of the fibre $w^{-1}(\gamma (d))$ an element of $v^{-1}(d)$; currying over the fibres of $\gamma$ turns this into an arrow $w\to {\mathrm{\Pi }}_{\gamma }(v)$ over $\mathrm{\Gamma }$, and uncurrying inverts it. Both bijections are natural because they are defined pointwise. For the last claim, take $\gamma ={\mathbf{p}}_A$ and $v={\mathbf{p}}_B$: the fibre of ${\mathbf{p}}_A$ over $g$ is $\{g\}\times A(g)$, so a section over that fibre is a function $x\mapsto y$ with $y\in B(g,x)$, which is an element of $\mathrm{\Pi }(A,B)(g)$. The identification of ${\mathrm{\Sigma }}_{{\mathbf{p}}_A}$ with $\mathrm{\Sigma }(A,B)$ is the same unfolding. ◻

Proof. Take $\mathrm{\Gamma }$ terminal in proposition 151.25 for the second claim, and $\gamma$ a product projection in the slice for the first; exponentials in $\mathcal{S}/\mathrm{\Gamma }$ are the special case of ${\mathrm{\Pi }}_{\gamma }$ where the domain is a pullback projection. ◻

Proof. Take $\mathrm{\Theta }=\mathrm{\Delta }=\mathrm{\Gamma }=X=\{0\}$ with all maps the identity. Then $(\gamma \circ \delta {)}^{\ast }w$ has underlying set $\{(0,0)\}$, whereas ${\delta }^{\ast }({\gamma }^{\ast }w)$ has underlying set $\{(0,(0,0))\}$: the pair $(0,(0,0))$ is not the pair $(0,0)$, since in the Kuratowski encoding their transitive closures differ. The canonical comparison $(0,(0,0))\mapsto (0,0)$ is a bijection over $\mathrm{\Theta }$, so the two objects are isomorphic in $\mathcal{S}/\mathrm{\Theta }$, and not equal. ◻

Proof. Each component is a pair of a component of $\mathcal{T}$ and a displayed component, and each equation is the pair of the corresponding equations; since the displayed sets are subsingletons, the displayed halves of the equations are automatic. For $\mathrm{\Pi }$ one must check that the clause for $S_{\mathrm{\Pi }(A,B)}$ is closed under the CwF operations: application of a term satisfying the clause to an argument satisfying $S_A$ satisfies $S_B$ by definition, and abstraction of a term satisfying $S_B$ over a fresh variable satisfies the clause because $\beta$ converts the application back. For $\mathbf{2}$ the two constructors satisfy $S_{\mathbf{2}}$ by reflexivity of judgmental equality, and the eliminator preserves the predicate by case analysis on which disjunct holds, using the two computation rules. $\mathbb{N}$ is the same argument with an induction on $n$. Strictness of $\pi$ is immediate: it forgets the second component and every operation was defined componentwise. ◻

Proof. $\int \mathcal{C}$ is a model of the signature by lemma 151.31, so theorem 54.27 gives a unique morphism $\sigma$; the composite $\pi \circ \sigma$ is a strict endomorphism of the initial model, hence the identity, again by uniqueness. ◻

Proof. The last paragraph of example 151.33 for $\mathbf{2}$; the same instantiation with $S_{\mathbb{N}}$ for $\mathbb{N}$. ◻