1. Quantifiers in a higher topos
Let $\mathcal E$ be a Grothendieck $\infty$-topos. In context $T$ the types are $\mathcal E_{/T}$ and propositions are its $(-1)$-truncated objects $\operatorname{Sub}(T)$. The inclusion $\iota$ has a left adjoint $\tau_{-1}$ given by relative image. Write $\lVert X\rVert_{-1}$ for this support. All constructions are read in the slice for the current generalized context. This is the higher-topos form of Lawvere's predicate doctrine [1,2].
For $f:A\to B$, pullback has the adjoint triples
$$ \Sigma_f\dashv f^*\dashv\Pi_f,\qquad \exists_f\dashv f^*\dashv\forall_f,\qquad \exists_f=\tau_{-1}\Sigma_f\iota,\quad \iota\forall_f\simeq\Pi_f\iota . $$
The left type adjoint is composition. The right exists because pullback preserves colimits between presentable slices [2, Remark 6.1.3.11]. Its defining mapping equivalence $\operatorname{Map}_{/B}(Y,\Pi_fX)\simeq\operatorname{Map}_{/A}(f^*Y,X)$ shows that it preserves propositions. The left proposition adjunction follows by composing with image reflection. Over $b:B$, set $A_b=\sum_{a:A}\operatorname{Id}_B(f(a),b)$. Then $\Sigma_fX(b)=\sum_{(a,p):A_b}X(a)$ and $\Pi_fX(b)=\prod_{(a,p):A_b}X(a)$. The first formula is pullback associativity, and the second represents sections after pullback along a test object. The existential is the support of the sum, with elimination into propositions [6]. Over $b:T\to B$ it holds iff the witness object $T\times_B P\to T$ is an effective epimorphism.
For a pullback with horizontal maps $h:A'\to A$ and $g:B'\to B$, the left Beck–Chevalley equivalence $\Sigma_{f'}h^*\simeq g^*\Sigma_f$ is pullback associativity. Its version $f^*\Sigma_g\simeq\Sigma_h f'^*$, tested by mapping into $X$ and transposing both sides, yields $g^*\Pi_f\simeq\Pi_{f'}h^*$. Relative images commute with pullback, giving both equivalences for propositions. Pullback associativity also gives $\Sigma_f(X\times_A f^*Y)\simeq\Sigma_fX\times_B Y$, whose image on predicates is Frobenius, $\exists_f(P\wedge f^*Q)\simeq(\exists_fP)\wedge Q$.
For sheaves on $\mathbb R$, the projection from the coproduct of the opens $(-\infty,1)$ and $(0,\infty)$ has true existential support, but a global witness would partition the connected space into disjoint opens subordinate to this cover. Change of topos differs from ambient substitution. For the stalk at $0$, the universal quantifier over the family of opens $(-1/n,1/n)$ has empty stalk because their meet is empty, while every individual stalk is terminal.
2. Internal Kan extension
Use complete Segal objects for internal categories and the large coefficient category of types $\mathsf{Type}_{\mathcal E}$, with sections $\mathcal E_{/T}$ in context $T$ [3,4]. For $u:C\to D$ and a covariant type-valued $F$, the adjoints to restriction are computed at each generalized $d:D$ by
$$ \begin{aligned} (\operatorname{Lan}_uF)(d) &\simeq\operatorname*{colim}_{(c,\,u(c)\to d)}F(c) \simeq\int^{c\in C}\operatorname{map}_D(u(c),d)\times F(c),\\ (\operatorname{Ran}_uF)(d) &\simeq\lim_{(c,\,d\to u(c))}F(c) \simeq\int_{c\in C}F(c)^{\operatorname{map}_D(d,u(c))}. \end{aligned} $$
The comma projections classify the presheaf $W_d=\operatorname{map}_D(u(-),d)$ and the covariant diagram $V_d=\operatorname{map}_D(d,u(-))$. Cocones to $Z$ correspond to maps of presheaves $W_d\to Z^{F(-)}$. Cones from $Z$ correspond to maps of covariant diagrams $V_d\to F(-)^Z$. These are the weighted coend and end universal properties. For a diagram classified by a left fibration $L\to I$, the colimit is the realization of $L$, since maps $L\to Z$ into a constant simplicial type give cocones. The limit represents maps $I\times Z\to L$ over $I$. It exists by the right adjoint to $Z\mapsto I\times Z$ into simplicial objects over $I$. Both representations hold in every context by pullback stability of colimits and the projection formula for $\Sigma$ applied to the section object.
The weighted formulas are functorial in $d$ by composition. Taking the end that computes natural transformations and applying tensor–hom adjunction gives
$$ \begin{aligned} \operatorname{Nat}_D(\operatorname{Lan}_uF,G) &\simeq\int_c\left(\int_dG(d)^{\operatorname{map}_D(u(c),d)}\right)^{F(c)} \simeq\operatorname{Nat}_C(F,u^*G),\\ \operatorname{Nat}_D(G,\operatorname{Ran}_uF) &\simeq\int_cF(c)^{\int^d\operatorname{map}_D(d,u(c))\times G(d)} \simeq\operatorname{Nat}_C(u^*G,F). \end{aligned} $$
The last steps are internal Yoneda and co-Yoneda [3,4]. The coherences in these ends and coends implement the comma-triangle relations.
On propositions the left adjoint is $\tau_{-1}\operatorname{Lan}_u\iota$ and the right is the restriction of $\operatorname{Ran}_u$. This follows from the reflection adjunction and preservation of limits by $\iota$. For a proposition diagram with left fibration $L\to I$, the support of the realization is the support of $L_0$, since every level maps to $L_0$ by taking a vertex. A degree-zero section of $L_0\to I_0$ makes it an equivalence and extends uniquely to a section of $L\to I$ by the left fibration identities. Thus the comma formulas become
$$ \begin{aligned} (\operatorname{Lan}^{\mathsf{Prop}}_u P)(d)&\simeq \exists_{c:C_0}\bigl(\lVert u(c)\to d\rVert_{-1}\wedge P(c)\bigr),\\ (\operatorname{Ran}^{\mathsf{Prop}}_u P)(d)&\simeq \forall_{c:C_0}\bigl(\lVert d\to u(c)\rVert_{-1}\Rightarrow P(c)\bigr). \end{aligned} $$
If $A,B$ are regarded as internal groupoids, a left fibration over $A$ is a family over $A$. Restriction is pullback and both comma categories at $b$ identify with $A_b$ by path inversion on the right. Consequently $\operatorname{Lan}_f=\Sigma_f$, $\operatorname{Ran}_f=\Pi_f$, with proposition versions $\exists_f,\forall_f$. For a nontrivial discrete group $G$, the family $1\to BG$ has terminal relative support and empty section space. A section would factor the identity of $BG$ through a point. Thus truncation can change the right extension if applied before the dependent product.
3. Base change with directed indexing
Given $h:C'\to C$, $g:D'\to D$ and $uh\simeq gu'$ for $u':C'\to D'$, the mates are $\operatorname{Lan}_{u'}h^*\to g^*\operatorname{Lan}_u$ and $g^*\operatorname{Ran}_u\to\operatorname{Ran}_{u'}h^*$. Finality of the left comma comparisons and initiality of the right ones suffice [5]. At $d'$ write $W'=\operatorname{map}_{D'}(u'(-),d')$, $W=\operatorname{map}_D(u(-),g(d'))$, $V'=\operatorname{map}_{D'}(d',u'(-))$, $V=\operatorname{map}_D(g(d'),u(-))$. The exact tests for all type diagrams are that $\lambda:\operatorname{Lan}_{h^{\mathrm{op}}}W'\to W$ and $\rho:\operatorname{Lan}_h V'\to V$, respectively, are equivalences. The exact tests for all proposition diagrams are equivalence of their pointwise supports.
Indeed, for $K\otimes_C F=\int^c K(c)\times F(c)$ the first mate is $\lambda\otimes_C F$ by adjunction. Covariant representables test each $\lambda(c)$ by co-Yoneda. The second is precomposition on $\operatorname{Nat}_C(V,F)$ and detects $\rho$ by Yoneda. The support of $K\otimes_C F$ is $\exists_{c:C_0}(\lVert K(c)\rVert_{-1}\wedge\lVert F(c)\rVert_{-1})$, using realization over the right fibration of $K$ and stability of images under products. Reflected representables therefore test the left comparison on propositions. On the right use the reflection adjunction inside the natural transformation object and test all proposition diagrams. These tests range over generalized contexts.
The inclusions of opposite vertices of $[1]$ have empty pullback, yet the arrow contributes to a left or right extension across the square, depending on orientation. To separate the two coefficient tests, include $[1]$ into the category with two parallel arrows from $0$ to $1$ by choosing one arrow. Pull back the inclusion of $0$. At $1$ the left comparison is $X\to X\amalg X$ into one summand. For proposition coefficients its support is always an equivalence. Pullback of the inclusion of $1$ gives the dual projection $X\times X\to X$ at $0$.
4. Observation transport and event identity
Fix a finite coordinate set $J$ with nonempty finite types $X_j$. For $V\subseteq J$, write $X_V=\prod_{j\in V}X_j$, with projections $\pi_{V,W}$ for $W\subseteq V$. The environment emits a trace in $X_J^N$ with unknown law. Agent $i$ observes scope $V_i$ and emits a record $(e,i,y)$ with $y\in X_{V_i}$ for a stable environmental event identifier $e$. An identifier is shared across different views of the same signal. Copies of a report keep its key $(e,i)$ and its value.
Let $D$ be a finite time-ordered information-flow category with retention and delivery edges. Let $u:S\to D$ include its discrete observation sources. In context of a possible record $r$, let $P(s,r)$ mean source $s$ produced it. The left proposition extension gives
$$ r\in L_d\quad\Longleftrightarrow\quad \exists_{s:S_0}\bigl(\lVert s\to d\rVert_{-1}\wedge P(s,r)\bigr). $$
Induction on the last edge of a path computes $L_d$ by union of incoming ledgers and new records. Repeated paths leave membership unchanged. This is a grow-only set merge [7]. With reliable synchronous rounds and no new records, every agent has the union after at most the directed diameter of a strongly connected communication graph. The proof follows a shortest delivery path for each record. A restricted history yields the same ledger for all source predicates precisely when it preserves source reachability, as can be tested by a record belonging only to one source.
For a ledger $L$, let $U_e$ be the union of scopes of the records of event $e$. The type of glued values is
$$ \mathsf{Glue}_e(L)=\sum_{y:X_{U_e}}\prod_{(e,i,z)\in L} \operatorname{Id}_{X_{V_i}}(\pi_{U_e,V_i}y,z). $$
Agreement on all overlaps assigns a unique value to each covered coordinate and gives a unique tuple. A disagreement gives an empty type. This is also the right-extension matching condition for the presheaf $W\mapsto X_W$ on observed subscopes of $U_e$. Its support is the existential statement that the observations can refer to a single signal on the union scope.
5. Coherent ontology models and their realizability
A finite candidate grammar $\mathcal O$ gives each $o$ a finite latent type $Z_o$, a vocabulary of predicates on $Z_o$, logical axioms on the predicates, and rational initial, transition, and emission laws $w_o,K_o,E_o$. Logical axioms are finite propositions, for example $\prod_{z:Z_o}(p(z)\Rightarrow q(z))$. Emission support can enforce an observable relation for each latent concept. The induced trace law is
$$ Q_o(x_{1:N})=\sum_{z_{1:N}}w_o(z_1) \prod_{e=1}^{N}E_o(x_e\mid z_e)\prod_{e=1}^{N-1}K_o(z_{e+1}\mid z_e). $$
The grammar bounds descriptions and assigns a prefix-code length $\ell(o)$. An agent's declared concept map $b_i:X_{V_i}\to B_i$ interprets local claims by pushforward of the corresponding model marginal. Accepted claims can be included as predicates restricting the grammar.
For a common denominator $M$ that accommodates the candidate marginals at a chosen event, put $\mathcal M(V)=\Delta_M(X_V)$, the finite type of mass tables with entries $k_x/M$. Marginalization makes $\mathcal M$ a presheaf. If $a:\mathcal A\hookrightarrow\mathcal P(J)$ includes a downward-closed family of observed scopes, then
$$ (\operatorname{Ran}_{a^{\mathrm{op}}}\mathcal M|_{\mathcal A^{\mathrm{op}}})(V) \simeq\lim_{W\in\mathcal A^{\mathrm{op}},\,W\subseteq V}\mathcal M(W). $$
This is the matching family of local model predictions. A global candidate restricts to a term of it. At $J$, write $R$ for the matching type and $\mathrm{res}:\mathcal O\to R$ for restriction. Given $m:R$, the type of global realizations is $\sum_{o:\mathcal O}\operatorname{Id}_R(\mathrm{res}(o),m)$. Its support is $\exists_{\mathrm{res}}\top$ at $m$.
For three bits, the uniform unequal-pair law on every pair has uniform one-bit marginals. The family matches, but a global realization would assign probability one to three simultaneous inequalities between the bits, an empty event [8]. A positive gluing criterion uses a tree of maximal scopes with the running intersection property. Attach a new scope $V$ to a joint law $q$ already defined on $U$. Its overlap $S$ with $U$ equals its overlap with its parent in the tree. For a new marginal $m_V$ sharing $m_S$, take $q'(x)=q(x_U)m_V(x_V)/m_S(x_S)$ on positive separator mass and zero otherwise. Summing along either side recovers the old marginal, so induction constructs a rational joint law. It can require a finer denominator grid or a larger grammar. Empirical frequencies from different samples are compared through likelihood.
6. Optimization and identifiability
For a consistent ledger, write $y_e:X_{U_e}$ for the glued tuple and $B_L=\{x_{1:N}:x_e|_{U_e}=y_e\ \forall e\}$. Given an exogenous observation schedule, select maximal positive weights
$$ \mathcal W_L(o)=2^{-\ell(o)}Q_o(B_L), \qquad \mathcal J_L(o)=\ell(o)-\log_2Q_o(B_L). $$
This minimizes the two-part description-length objective [9]. The comparison can use exact rational arithmetic. For independent candidate events, $Q_o(B_L)=\prod_e q_o^{U_e}(y_e)$. Each event contributes one joint marginal factor even when several agents report it. For a Markov candidate, put $b_e(z)=\sum_{x|_{U_e}=y_e}E_o(x\mid z)$ and use the forward recursion [10]
$$ \alpha_1(z)=w_o(z)b_1(z),\qquad \alpha_{e+1}(z')=b_{e+1}(z')\sum_z\alpha_e(z)K_o(z'\mid z),\qquad Q_o(B_L)=\sum_z\alpha_N(z). $$
Inductively $\alpha_e(z)$ is the joint mass of the observed prefix and latent state $z$. The recurrence costs $O(N|Z_o|^2)$ arithmetic operations once the marginal emissions are computed. For eventwise noisy sensors with a known joint channel $k_e(r_e\mid x)$, use $\sum_x E_o(x\mid z)k_e(r_e\mid x)$ as the emission factor.
The finite solver merges ledgers, glues each event, enumerates the grammar, and retains all maximal positive weights in the type $\mathsf{Opt}(L)$. Equal ledgers and a common grammar give equal optimizer types. A full-support admitted candidate guarantees a fit for consistent evidence. The logical statements that some or every optimum satisfies $\varphi$ are $\lVert\sum_{o:\mathsf{Opt}(L)}\varphi(o)\rVert_{-1}$ and $\prod_{o:\mathsf{Opt}(L)}\varphi(o)$. Agreement with a witness can conjoin the universal statement with existence of a fit.
On a common ledger snapshot, partition the grammar across agents. Each worker returns its largest positive weight with all attaining candidates, or an empty result. Taking the largest weight and retaining all candidates tied at it recovers the global optimizer type because the partitions cover the grammar.
For independent events and scopes drawn independently of signals with law $w$, the population log-risk excess over the true marginal law is $\sum_V w(V)D_{\mathrm{KL}}(p_\star^V\Vert q_o^V)$. This follows by conditioning on $V$. Thus the observation design distinguishes candidates exactly by their marginals on its support. With a finite grammar and each observed mass at least $\varepsilon>0$, Hoeffding and a union bound give uniform risk error at most $\eta_n=\log_2(1/\varepsilon)\sqrt{\ln(2|\mathcal O|/\delta)/(2n)}$ with probability $1-\delta$ over $n$ independent identically distributed events [11]. A penalized empirical optimum has excess over the best population-risk candidate $o^\star$ at most $2\eta_n+(\ell(o^\star)-\min_o\ell(o))/n$, by optimality on the empirical scores and the uniform error bound.
For acquisition, normalize the positive weights into $\pi_L$. If action $a$ has candidate-predictive law $p_o^a$ for its next report, its expected entropy reduction is $\sum_o\pi_L(o)D_{\mathrm{KL}}(p_o^a\Vert\sum_{o'}\pi_L(o')p_{o'}^a)$ [12]. Subtract a cost expressed in equivalent bits. This compares observing one scope with scheduling complementary scopes at the same event.
7. Three-agent example on a 64-bit signal type
Let $X=\{0,1\}^{64}$. Agents $A,B,C$ observe pairs $(1,2),(2,3),(1,3)$ of the first three bits plus disjoint blocks of $20,20,21$ suffix bits. The suffix bits have an independent fair law in all candidates. The baseline $o_0$ has fair independent first bits and code length 1. Models $o_+,o_-$ have latent parity concepts, uniform emissions within each parity, and even probabilities $7/8,1/8$, with code lengths 3 each. All individual sensor marginals agree.
Agents $A$ and $B$ report events 1 through 8, whose first three bits are $000,011,101,110,000,011,101,001$. Agent $C$ reports events 1, 4, and 9, with pair $(1,0)$ at event 9. Along the bidirectional chain $A\leftrightarrow C\leftrightarrow B$, ledger sizes go from $(8,8,3)$ to $(11,11,19)$ and then $(19,19,19)$. Event gluing yields seven even triples, one odd triple, and one pair. All suffix reports contribute the same $383$ bits to every score. The pair contributes two common bits. Subtracting the suffix contribution, the scores of $o_0,o_+,o_-$ are
$$ 27,\qquad 45-7\log_2 7\simeq25.3485,\qquad 45-\log_2 7\simeq42.1926 . $$
Thus $o_+$ uniquely wins. Per-agent histograms give equal marginal log losses and would favor the shorter baseline code. Event pairing supplies the triple scope needed to distinguish the parity models. With initial code weights normalized to $(2/3,1/6,1/6)$, a fresh single-agent view gives zero information gain. A paired $A,B$ measurement gives $(1-h_2(7/8))/3\simeq0.1521$ bits, where $h_2$ is binary entropy. The exact scores were checked by rational arithmetic.
AI assistance was used in drafting and typesetting this manuscript.
References
1. F. W. Lawvere, Adjointness in foundations, 1969. 2. J. Lurie, Higher Topos Theory, 2009. 3. L. Martini, Yoneda's lemma for internal higher categories, 2021. 4. L. Martini and S. Wolf, Colimits and cocompletions in internal higher category theory, 2024. 5. E. Riehl and D. Verity, Kan extensions and the calculus of modules, 2017. 6. Univalent Foundations Program, Homotopy Type Theory, 2013. 7. M. Shapiro et al., A comprehensive study of convergent and commutative replicated data types, 2011. 8. N. N. Vorob'ev, Consistent families of measures and their extensions, 1962. 9. P. D. Grünwald, The Minimum Description Length Principle, 2007. 10. L. R. Rabiner, A tutorial on hidden Markov models, 1989. 11. W. Hoeffding, Probability inequalities for sums of bounded random variables, 1963. 12. T. M. Cover and J. A. Thomas, Elements of Information Theory, 2nd ed., 2006.