Parametric Large Sizes and Realizability Consistency

Proof. Take $A:=\lambda i.\mathbf{0}$ and $f:=\lambda i.\lambda g.g\mathrm{\infty }p$. For this to type-check we need , which the hypothesis supplies only at $i:=\mathrm{\infty }$; so restrict attention to that instance. There and $g\mathrm{\infty }p:\mathbf{0}$, so . The fixed point at $\mathrm{\infty }$ is a term $x:\mathbf{0}$ satisfying , and its mere existence inhabits $\mathbf{0}$. ◻

Proof. The pair $(\mathsf{fix}f,{\mathsf{fix}}^{\beta }f)$ inhabits the type. Let $(g,g^{\beta })$ be another inhabitant. It suffices to give a pointwise identity $e:\mathrm{\forall }i.{\mathsf{Id}}_{}(\mathsf{fix}fi,gi)$ and an identity $e^{\beta }$ transporting ${\mathsf{fix}}^{\beta }f$ to $g^{\beta }$ along $\mathsf{funext}(e)$.

For $e$, apply Fix to $\lambda i.\lambda e^{\prime }.p_{i,e^{\prime }}$, where $p_{i,e^{\prime }}$ is the concatenation Here is the argument supplied by Fix at $i$.

For $e^{\beta }$, it suffices that the square whose two horizontal sides are ${\mathsf{fix}}^{\beta }fi$ and $g^{\beta }i$ and whose two vertical sides are $ei$ and commutes. That is exactly ${\mathsf{fix}}^{\beta }$ applied to the term $\lambda i.\lambda e^{\prime }.p_{i,e^{\prime }}$ just constructed. ◻

Proof. Both are argument exchange. For the first, send $h$ to $\lambda .{}^{\mathrm{\forall }}i.\lambda x.hxi$ and $k$ to $\lambda x.\lambda .{}^{\mathrm{\forall }}i.kix$; the two round trips are the $\beta$- and $\eta$-rules of definition 166.4 together with those of $\mathrm{\Pi }$. For the second, send $(x,⟨s,b{⟩}^{\mathrm{\exists }})$ to $⟨s,(x,b){⟩}^{\mathrm{\exists }}$ and back; both directions are definable by Ex-E, since the motive in each case is small, and the round trips are the computation rule of Ex-E together with the $\eta$-rule for $\mathrm{\Sigma }$. ◻

Proof. The case $A:=\mathbf{1}$. For $\mathrm{\exists }$, the middle step reading Ex-Pi from right to left with $A:=\mathbf{0}$. For $\mathrm{\forall }$, $\mathrm{\forall }i.\mathbf{1}\simeq \mathbf{1}$ by function extensionality, since both sides are contractible.

The general case. Using $\sum _{x:A}\mathbf{1}\simeq A$ and proposition 166.7, $$\mathrm{\exists }i.A\stackrel{\mathrm{\Sigma }-\mathbf{1}}{=}\mathrm{\exists }i.\sum _{x:A}\mathbf{1}\stackrel{proposition166.7}{=}\sum _{x:A}\mathrm{\exists }i.\mathbf{1}\stackrel{firstcase}{=}\sum _{x:A}\mathbf{1}\stackrel{\mathrm{\Sigma }-\mathbf{1}}{=}A,$$ and the same chain with $\mathrm{\forall }$ in place of $\mathrm{\exists }$, using All-Sg at the second step. ◻

Proof. The carrier is a fixed point. By Fix-$\beta$,

The structure map. Transporting along the displayed identity pointwise in $i$ gives ${\mathsf{in}}^{\mathrm{\exists }}:F[\mathrm{\exists }-]({\mu }^{\mathrm{\exists }}F)\to {\mu }^{\mathrm{\exists }}F$.

Initiality. Given a size-indexed algebra $(A,k_A)$, define ${\mathsf{fold}}^{\mathrm{\exists }}A{k}_A$ by Fix with the step that sends $i$ and a family of maps at smaller sizes to $k_{A}i\circ F[\mathrm{\exists }-](\text{that family})i$, precomposed with the transport above. That it is an algebra morphism is the $\beta$-identity of Fix-$\beta$; that it is unique is lemma 166.6 together with function extensionality, since a competing morphism is a competing solution of the same unfolding equation. ◻

Proof. Since $i$ does not occur in $A$, the term is well defined by Ex-E, because its motive $TAi\equiv A$ is small and does not mention the bound size. Set $k_{TA}i:=k_A\circ F({\mathsf{extract}}_{A}i)$, using $F({\mathsf{extract}}_{A}i):F[\mathrm{\exists }-](TA)i\to FA$. For an algebra map $f$, put $Tf:=\lambda i.f$; it is a morphism because ${\mathsf{extract}}_A$ is natural in $A$. ◻

Proof. The map $\mathrm{\exists }f$ is definable by Ex-E with the small motive $\mathrm{\exists }i.Bi$. Composing it with the quasi-inverse supplied by definition 166.14 gives $k_{\mathrm{\exists }A}$ of the stated type. Functoriality follows from naturality of ${\mathrm{can}}_A$ in $A$, which holds because ${\phi }_A$ is natural in $A$ and $F$ is a functor. ◻

Proof. Proof idea. The functor $\mathrm{\exists }$ of proposition 166.15 is left adjoint to the functor $T$ of lemma 166.13, and a left adjoint preserves initial objects; the initial size-indexed algebra of lemma 166.12 therefore maps to an initial $F$-algebra.

Spelling out the adjunction: for $A:\mathsf{Size}\to \mathcal{U}$ and $B:\mathcal{U}$, the currying equivalence identifies morphisms $A\to TB$ of size-indexed types with maps $\mathrm{\exists }i.Ai\to B$, because a morphism $A\to TB$ is a term of $\mathrm{\forall }i.(Ai)\to B$ and Ex-E turns such a term into a map out of $\mathrm{\exists }i.Ai$, with Ex-I giving the converse and the computation rule giving the two round trips. The identification carries algebra morphisms to algebra morphisms, since $k_{TB}$ was defined through $\mathsf{extract}$ and $k_{\mathrm{\exists }A}$ through ${\mathrm{can}}_A^{-1}$, which are the two components of the same currying.

Hence giving an algebra morphism $(\mu F,\mathsf{in})\to (B,k_B)$ is the same as giving a size-indexed algebra morphism $({\mu }^{\mathrm{\exists }}F,{\mathsf{in}}^{\mathrm{\exists }})\to (TB,k_{TB})$, and the latter type is contractible by lemma 166.12. ◻

Proof. Compute, using that $i$ is free in neither $A$ nor $B(a)$: The composite is the canonical map of definition 166.14, so that map is an equivalence. ◻

Proof. Proposition 166.17 and theorem 166.16. ◻

Proof. Each step is the dual of the corresponding step in lemma 166.12–proposition 166.17, with the following substitutions: $\mathsf{fix}$ is applied to in place of the existential body, giving ${\nu }^{\mathrm{\forall }}Fi=F[\mathrm{\forall }-]({\nu }^{\mathrm{\forall }}F)i$ by Fix-$\beta$; the functor $T$ of lemma 166.13 becomes the inclusion of coalgebras into size-indexed coalgebras, with $\mathsf{extract}$ replaced by the map that ignores the bound; the functor $\mathrm{\exists }$ of proposition 166.15 becomes $\mathrm{\forall }$, right adjoint rather than left; and the chain of proposition 166.17 becomes A right adjoint preserves terminal objects, which replaces the use of preservation of initial objects in theorem 166.16. Laarakker, Otten and van den Berg state the dual development and refer its details to the full version of their paper; the steps just listed are the ones that differ from the initial case, and no step of section 166.1–section 166.3 is reused outside its stated hypotheses. ◻

Proof. The displayed relation is symmetric and transitive by construction, and modesty makes the witness $x$ unique, so the equivalence classes of ${\sim }_X$ correspond to the elements of $X$ that have a realizer, which is all of them. Conversely a partial equivalence relation $\sim$ gives the modest set whose carrier is the set of $\sim$-classes with $n\Vvdash [n]$. A morphism of modest sets is tracked, hence induces a map of classes, and conversely. ◻

Proof. $M(A)$ is modest: if $n$ realizes $[a_1]$ and $[a_2]$ then it realizes members $a_1^{\prime }{\sim }_M{a}_1$ and $a_2^{\prime }{\sim }_M{a}_2$, so $a_1^{\prime }{\sim }_M{a}_2^{\prime }$ by the generating clause, and the classes coincide. The unit $A\to M(A)$ sends $a$ to $[a]$ and is tracked by the identity. For the universal property, a morphism $A\to I(B)$ into a modest set identifies any two elements sharing a realizer, hence factors through ${\sim }_M$, and the factorization is tracked by the same realizer. ◻

Proof. We treat the five groups separately.

Sizes and their order. $\mathsf{Size}=\mathrm{\nabla }{\omega }_1$ has the required terms: $0$ and the ordinal successor. The order is interpreted by a subterminal assembly, so $i\le j$ is a mere proposition, and the four constructors of definition 166.3 are the corresponding facts about ordinals. There is no interpretation of a largest size: ${\omega }_1$ has no greatest element, so the hypothesis of proposition 166.1 is not met.

The universal quantifier. Assemblies support impredicative dependent products: a tracked dependent function out of $\mathrm{\nabla }{\omega }_1$ into a family of modest sets is itself tracked by a single realizer, so the product is modest and hence small. This is the clause that makes $\mathrm{\forall }$ impredicative.

The existential quantifier. By lemma 166.27, lemma 166.25, the modest reflection of the semantic $\mathrm{\Sigma }$-type is a partial equivalence relation, hence an element of $\mathcal{U}$. Its introduction is the unit of the reflection; its elimination is the universal property, whose motive must be modest, which is exactly the smallness side condition of Ex-E. Since the reflection quotients by shared realizers and every element of $\mathrm{\nabla }{\omega }_1$ has every realizer, two pairs with the same second component and different sizes are identified, which is why no first projection exists.

The fixed-point operator. Given $f$, define the underlying function of $\mathsf{fix}f$ by well-founded induction on ${\omega }_1$; that definition satisfies the unfolding identity of Fix-$\beta$ on the nose, which is a propositional identity in the theory because the model is extensional. For $\mathsf{fix}f$ to be a morphism it must be tracked, and a partial combinatory algebra contains a term $\mathsf{fix}$ with $\mathsf{fix}e\downarrow$ and $\mathsf{fix}ea\simeq e(\mathsf{fix}e)a$; that term tracks it, uniformly in the ordinal, because the ordinal carries no realizer information.

The four axioms. All-Sg and All-Lt hold because $\mathrm{\forall }$ is a product over $\mathrm{\nabla }{\omega }_1$ and $\mathrm{\nabla }$ makes every map out of it uniform, so the product commutes with $\mathrm{\Sigma }$ and the bound may be weakened. Ex-Lt holds because the reflection identifies a pair with any pair over a larger size. Ex-Pi is the clause that fixes the choice of ${\omega }_1$: reading it from left to right, a dependent function from a small type $A$ into $\mathrm{\exists }i.B(a,i)$ assigns to each $a$ a size, and a size bounding all of them is required. A small type is a partial equivalence relation on $\mathbb{N}$, so it has at most countably many classes; a countable supremum of countable ordinals is countable, hence lies in ${\omega }_1$. ◻

Proof. By theorem 166.28 every closed term of a closed type denotes a global element of the interpretation of that type in definition 166.26. The empty type is interpreted by the assembly with empty carrier, which has no global element. Hence no closed term of type $\mathbf{0}$ exists. ◻