Higher-Order Logic in Infinity-Toposes
Extending the Lambek–Scott correspondences
Lambek and Scott connect typed lambda calculi with cartesian closed categories, extensional intuitionistic type theory with toposes, and numerical recursion with categorical universal properties. We develop these correspondences in the slices of a Grothendieck $\infty$-topos. The full proofs and bibliography are in the attached PDF and LaTeX bundle.
Indexed recovery theorem
Let $\mathcal E$ be a Grothendieck $\infty$-topos and $\mathcal C=\mathcal E_{\le0}$ its ordinary topos of $0$-truncated objects. For $X\in\mathcal C$, the slice of relatively $0$-truncated types $(\mathcal E_{/X})_{\le0}$ is $\mathcal C_{/X}$, and the subobject posets agree. For maps $f:X\to Y$ in $\mathcal C$, these identifications intertwine $\Sigma_f\dashv f^*\dashv\Pi_f$ and the predicate quantifiers $\exists_f(P)=\tau_{\le-1}^Y\Sigma_fP$ and $\forall_f(P)=\Pi_fP$. They preserve relative exponentials, equality, and the subobject classifier and respect Beck–Chevalley and Frobenius reciprocity.
If $X$ and $A$ are $0$-truncated, testing $A\to X$ by any source gives a map of discrete spaces, with discrete fibers. Conversely, a relatively $0$-truncated map over a $0$-truncated context has $0$-truncated total space by composition. Monomorphisms are detected by their relative diagonals, and the inclusion of $0$-truncated objects preserves finite limits. Composition and pullback preserve the required truncation, and dependent product preserves truncated objects by its mapping-space adjunction. The two adjunctions and the image universal property therefore restrict. The subobject classifier is $0$-truncated because its mapping space from a test object is the discrete space of subobjects. Pullback pasting gives the Beck–Chevalley equivalence for sums, and taking adjoint mates gives the comparison for products. Both sides of Frobenius have total space $A\times_Y B$.
Limits of recovery
The ordinary topoi of $\mathcal S$ and $\mathcal S_{/S^2}$ are both equivalent to $\mathbf{Set}$. Indeed, discrete fibers over $S^2$ classify through its terminal fundamental groupoid. The constant object $cK$ is intrinsically the $K$-indexed colimit of the terminal object. Its section spaces are respectively $K$ and $\operatorname{Map}(S^2,K)$ in the two topoi. For $K=K(\mathbb Z,2)$ their component sets are respectively a singleton and $\mathbb Z$, distinguishing the higher topoi.
Applying $\Pi_f$ to the truncation unit gives a comparison
$$ \tau_{\le0}^{Y}\Pi_f A \longrightarrow \Pi_f\tau_{\le0}^{X}A. $$
Obstructed section. In spaces take $f:BC_2\to 1$ and $A=(BC_4\to BC_2)$ induced by reduction modulo $2$. The fiber is connected, with homotopy type $BC_2$. Truncating first makes the family terminal. A coherent section before truncating would split $C_4\to C_2$ on fundamental groups, which is impossible. Here the comparison is $\varnothing\to *$.
Failure over set-valued contexts. Let $D$ be the face poset of the boundary of a triangle and adjoin a terminal object $t$ to form $C$. In $\mathcal E=\operatorname{Fun}(C^{\mathrm{op}},\mathcal S)$, let $U$ be the subterminal that is $*$ on $D$ and $\varnothing$ at $t$. Take $f:U\to 1$ and $A=U\times cS^1\to U$. At $t$, $\Pi_f A$ has value $\operatorname{Map}(|ND|,S^1)$ since $y(t)=1$ and $U$ is the left Kan extension of the terminal presheaf on $D$. Objectwise truncation leaves $\mathbb Z$ at $t$ since $|ND|\simeq S^1$ and maps have integer degree. Truncating the family first gives a terminal product.
Finite local criterion. If $f$ is locally a finite coproduct of copies of the identity on an effective-epimorphism cover, the comparison is invertible. Base change commutes with $\Pi_f$ and relative truncation and detects equivalences on the cover. Over each trivialization, $\Pi_f$ is a finite product, and truncation preserves finite products in the slice.
Descent, classification, and recursion
The full manuscript describes slice descent, path induction, and univalent object classifiers. It gives distinct presheaf classifiers for unrestricted and discrete sorts and shows that maps to a delooping $BG$ classify the full space of $G$-torsors. Statements about judgmental computation require a coherent presentation, such as the strict univalent models described by Shulman.
The natural numbers object is $N=\coprod_{n\in\mathbb N}1$. A recursion solution includes a sequence of values and paths enforcing the base and successor equations. At each finite stage the space of possible new values equipped with a path to the prescribed value is contractible. The space of all solutions is the inverse limit of these stages and is contractible; the same argument applies to dependent recursion. Classical external mathematics supplies a nonrecursive numerical function, which becomes an endomorphism of $N$ by the coproduct property. Every standard program code fails on some numeral for this endomorphism, so the subobject of codes computing it is initial on every summand and hence initially empty. Thus absolute internal Church’s thesis with the stated standard computation predicate is false in any nondegenerate Grothendieck $\infty$-topos. Effective realizability provides a different categorical setting with tracked numerical maps.
Sources and disclosure
This is an article-length development of the source’s themes. AI assistance was used to draft, organize, and typeset the manuscript. The submitter is responsible for the manuscript and uses the public byline Anonymous.
- J. Lambek and P. J. Scott, Introduction to Higher Order Categorical Logic (1986). Publisher front matter
- J. Lurie, Higher Topos Theory (2009), Chapter 6. Author's text
- M. Shulman, All $(\infty,1)$-toposes have strict univalent universes (2019). arXiv
- J. M. E. Hyland, The Effective Topos (1982). Author's copy