nLab theory of model homomorphisms



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




For any geometric theory 𝕋\mathbb{T} there exists a geometric theory 𝕋 2\mathbb{T}^2, the theory of 𝕋\mathbb{T}-model homomorphisms, whose models in a Grothendieck topos \mathcal{E} are precisely the homomorphisms between 𝕋\mathbb{T}-models in \mathcal{E}.


Let 𝕋\mathbb{T} be a geometric theory over the signature Σ\Sigma.

Let Σ 2\Sigma^2 be the signature containing a pair of new sort symbols X 0X^0, X 1X^1 and a new function symbol f X:X 0X 1f_X:X^0\to X^1 for any sort symbol XX in Σ\Sigma, as well, as pairs g 0:X 1 0××X n 0Y 0g^0:X_1^0\times\dots\times X_n^0\to Y^0, g 1:X 1 1××X n 1Y 1g^1:X_1^1\times\dots\times X_n^1\to Y^1 of new functions symbols (resp. pairs R 0X 1 0××X n 0R^0\rightarrowtail X_1^0\times\dots\times X_n^0, R 1X 1 1××X n 1R^1\rightarrowtail X_1^1\times\dots\times X_n^1 of new relation symbols) for any function symbol g:X 1××X nYg:X_1\times\dots\times X_n\to Y (resp. relation symbol RX 1××X nR\rightarrowtail X_1\times\dots\times X_n) in Σ\Sigma.

The theory of 𝕋\mathbb{T}-model homomorphisms is the theory 𝕋 2\mathbb{T}^2 over the signature Σ 2\Sigma^2 with the following sequents:

A pair of sequents φ 0ψ 0\varphi^0\vdash \psi^0, φ 1ψ 1\varphi^1\vdash \psi^1 for any sequent φψ\varphi\vdash \psi in 𝕋\mathbb{T} where the new sequents result from replacing the function and relation symbols in φψ\varphi\vdash \psi with their 0-indexed, resp. 1-indexed pendants where necessary1. Plus a sequent

f Y(g 0(x 1,,x n))=g 1(f X 1(x 1),,f X n(x n))\top\vdash f_Y(g^0(x_1,\dots,x_n))=g^1(f_{X_1}(x_1),\dots,f_{X_n}(x_n))


R 0(x 1,,x n)R 1(f X 1(x 1),,f X n(x n))R^0(x_1,\dots,x_n)\vdash R^1(f_{X_1}(x_1),\dots,f_{X_n}(x_n))

for any pair g 0g^0, g 1g^1 of function symbols in Σ 2\Sigma^2 corresponding to g:X 1××X nYg:X_1\times\dots\times X_n\to Y in Σ\Sigma (in case n=0n=0\,, the sequent reads f Y(g 0)=g 1\top\vdash f_Y(g^0)=g^1\,), resp. any pair R 0R^0, R 1R^1 of relation symbols in Σ 2\Sigma^2 corresponding to RX 1××X nR\rightarrowtail X_1\times\dots\times X_n in Σ\Sigma (in case n=0n=0\,, the sequent reads R 0R 1R^0\vdash R^1\,).



Let \mathcal{E} be a Grothendieck topos. Then

𝕋 2-Mod()=𝕋-Mod() 2=𝕋-Mod( 2).{\mathbb{T}^2}\text{-}Mod(\mathcal{E})=\mathbb{T}\text{-}Mod(\mathcal{E})^2=\mathbb{T}\text{-}Mod(\mathcal{E}^2)\quad.

Cf. Johnstone (1977, p. 203; 2002, p.425), Mac Lane-Moerdijk (1994, ex.X.5 p.572).

Note that the second equality determines the class of 𝕋\mathbb{T}-model homomorphisms once the 𝕋\mathbb{T}-models in the arrow categories 2\mathcal{E}^2 are known.

Remark: This e.g. precludes the existence of geometric theories 𝕋 op\mathbb{T}^{op} or 𝕋 ×\mathbb{T}^\times with the property that, given a geometric theory 𝕋\mathbb{T}, the category of models 𝕋 op-Mod(){\mathbb{T}^{op}}\text{-}Mod(\mathcal{E}) and 𝕋 ×-Mod(){\mathbb{T}^{\times}}\text{-}Mod(\mathcal{E}) coincide with the opposite category 𝕋-Mod() op{\mathbb{T}}\text{-}Mod(\mathcal{E})^{op} or the twisted arrow category 𝕋-Mod() ×{\mathbb{T}}\text{-}Mod(\mathcal{E})^\times for any Grothendieck topos, respectively. In particular, since the (geometric) theory of morphisms 𝕆 2\mathbb{O}^2 (see the examples below) assigns the arrow category 2\mathcal{E}^2 as category of models to a Grothendieck topos \mathcal{E} no geometric theory can assign all Grothendieck toposes \mathcal{E} their twisted arrow category ×\mathcal{E}^\times as category of models because the class of models coincides with the class of models for the theory of morphisms. \qed

Since 2=×Set 2\mathcal{E}^2=\mathcal{E}\times Set^2 in general and the Sierpinski topos Set 2Set^2 is exponentiable, one gets

𝕋 2-Mod()=𝕋-Mod( 2)=Hom( 2,Set[𝕋])=Hom(×Set 2,Set[𝕋])=Hom(,Set[𝕋] (Set 2)){\mathbb{T}^2}\text{-}Mod(\mathcal{E})=\mathbb{T}\text{-}Mod(\mathcal{E}^2)=Hom(\mathcal{E}^2,Set[\mathbb{T}])=Hom(\mathcal{E}\times Set^2, Set[\mathbb{T}])=Hom(\mathcal{E},Set[\mathbb{T}]^{(Set^2)})

or in other words


The classifying topos for the theory 𝕋 2\mathbb{T}^2 of 𝕋\mathbb{T}-model homorphisms is Set[𝕋 2]=Set[𝕋] (Set 2)Set[\mathbb{T}^2]= Set[\mathbb{T}]^{(Set^2)}.

Remark: It is worthwhile to muse a bit how “squaring” fares as a theory operator with respect to the various subdoctrines of geometric logic: since it does not introduce logical operators like infinitary disjunctions or quantifiers unless the operators were already present in 𝕋\mathbb{T}, one sees that the formats of the more expressive subdoctrines like Horn, regular, and coherent logic are respected by the passage to 𝕋 2\mathbb{T}^2. Also, the square of a propositional theory i.e. one over a signature lacking sort symbols, is again propositional - this implies e.g. via the above corollary that the exponentiation of a localic topos by Set 2Set^2 is again a localic topos. The order sensitive subdoctrines like cartesian or disjunctive logic are also respected. One case where squaring does not preserve the subdoctrine is 1-sorted algebraic logic since then 𝕋 2\mathbb{T}^2 is necessarily 2-sorted. \qed

By an observation of Hébert (2010, p.1), the finitely presentable objects in arrow categories 𝒦 2\mathcal{K}^2, are precisely the morphisms between finitely presentable objects in 𝒦\mathcal{K} whence, denoting the subcategory of finitely presentable models of a theory 𝕋\mathbb{T} in a topos \mathcal{E} by 𝕋-Mod fp()\mathbb{T}\text{-}Mod_{fp}(\mathcal{E}) one has

𝕋 2-Mod fp()=𝕋-Mod fp() 2.\mathbb{T}^2\text{-}Mod_{fp}(\mathcal{E})=\mathbb{T}\text{-}Mod_{fp}(\mathcal{E})^2\;.

But since classifying toposes of cartesian theories are given by the presheaf toposes on the opposite of the category of their finitely presentable models in SetSet (cf. Johnstone 2002b, p. 891) one has


Let 𝕋\mathbb{T} be a cartesian theory. Then the theory 𝕋 2\mathbb{T}^2 of 𝕋\mathbb{T}-model homorphisms is cartesian and its classifying topos is Set[𝕋 2]=Set 𝕋 2-Mod fp(Set)=Set (𝕋-Mod fp(Set) 2)=(Set 𝕋-Mod fp(Set)) (Set 2)=Set[𝕋] (Set 2)Set[\mathbb{T}^2]=Set^{\mathbb{T}^2\text{-}Mod_{fp}(Set)}=Set^{(\mathbb{T}\text{-}Mod_{fp}(Set)^2)}=\big (Set^{\mathbb{T}\text{-}Mod_{fp}(Set)}\big)^{(Set^2)}=Set[\mathbb{T}]^{(Set^2)}.

For an easy application of this result see at the theory 𝕆\mathbb{O} of objects in the examples below!


  • Let 𝕋 \mathbb{T}^\emptyset_\emptyset and 𝕋 1 \mathbb{T}^\emptyset_1 be the empty theory, resp., the inconsistent theory, over the empty signature. Then 𝕋 2=𝕋 \mathbb{T}^{\emptyset 2}_\emptyset=\mathbb{T}^\emptyset_\emptyset and 𝕋 1 2=𝕋 1 \mathbb{T}^{\emptyset 2}_1=\mathbb{T}^\emptyset_1 in accordance with the fact that these theories have only empty models whence all model homomorphisms are identity morphisms of empty models. In other words, squaring theories obeys the laws of arithmetic at 0 and 1.

  • Let 𝕆\mathbb{O} be the theory of objects i.e. the theory with no sequents over the signature with one sort symbol OO. Then 𝕆 2\mathbb{O}^2 is the theory with no sequents over the signature with two sort symbols O 0O^0, O 1O^1 and a function symbol f O:O 0O 1f_O:O^0\to O^1. Clearly, its models in a Grothendieck topos \mathcal{E} are the morphisms of \mathcal{E} and, accordingly, 𝕆 2\mathbb{O}^2 is called the theory of morphisms.

    It is the dual theory of the theory classified by the Sierpinski topos Set 2Set^2, or in other words, its classifying topos called the morphism classifier (cf. Johnstone 1977, p.184; 2002, p.426) is

    Set[𝕆 2]=Set[𝕆] Set 2=(Set FinSet) Set 2=Set (FinSet 2). Set[\mathbb{O}^2]=Set[\mathbb{O}]^{Set^2}=(Set^{FinSet})^{Set^2}=Set^{(FinSet^2)}\quad .

    The generic morphism is given by the natural transformation η:OdomOcod\eta\,:\,\mathbf{O}\circ dom\to\mathbf{O}\circ cod with O\mathbf{O} the generic object i.e. the inclusion functor FinSetSetFinSet\hookrightarrow Set, and dom:FinSet 2FinSet,(XY)Xdom\,:\,FinSet^2\to FinSet\, ,\, (X\to Y)\mapsto X the domain projection functor, and cod:FinSet 2FinSet,(XY)Ycod\,:\,FinSet^2\to FinSet\,,\, (X\to Y)\mapsto Y the codomain projection functor, with components η (XY)=O(XY)\eta_{(X\to Y)}=\mathbf{O}(X\to Y).

  • Let 𝕂\mathbb{K} be the theory of categories (e.g. Johnstone 1977, p.202) whose models in a Grothendieck topos \mathcal{E} are the internal categories Ccat()\mathbf{C}\in cat(\mathcal{E}). Then 𝕂 2\mathbb{K}^2 is the theory of functors. 𝕂\mathbb{K} likely being the most famous cartesian theory, one has Set[𝕂 2]=Set (𝕂-Mod fp(Set) 2)Set[\mathbb{K}^2]=Set^{(\mathbb{K}\text{-}Mod_{fp}(Set)^2)}.

The connection to natural homotopy

The Sierpinski topos Set 2Set^2 is a connected, locally connected and local topos. As a result of Artin gluing along SetidSetSet\overset{id}{\to}Set it has two topos points (corresponding to the two points of the underlying Sierpinski space). Whence one can take Set 2Set^2 as an abstract interval object for a homotopy theory of Grothendieck toposes correlated with their nature as “generalized spaces” and view, accordingly, the exponential Set 2\mathcal{E}^{Set^2} as a path space for \mathcal{E}.

(Cf. Beke 2000, p.11f)


  • Tibor Beke, Homotopoi , ms. University of Massachusetts Lowell (2000). (dvi)

  • Michel Hébert?, Finitely presentable morphisms in exact sequences , TAC 24 no.9 (2010) pp.209-220. (abstract)

  • Peter Johnstone, Topos Theory , Academic Press New York (1977). (Also available as Dover Reprint, Mineola 2014)

  • Peter Johnstone, Sketches of an Elephant vol.1 , Oxford UP 2002.

  • Peter Johnstone, Sketches of an Elephant vol.2 , Oxford UP 2002.

  • André Joyal, Gavin Wraith, Eilenberg-Mac Lane Toposes and Cohomology , pp.117-131 in Cont. Math. 92 AMS 1984.

  • Saunders Mac Lane, Ieke Moerdijk, Sheaves in Geometry and Logic , Springer Heidelberg 1994.

  1. It is understood that variables and contexts are updated with the new sorts e.g. the sequent x:Sx=x\top\vdash_{x:S} x=x yields two sequents x:S 0x=x\top\vdash_{x:S^0} x=x and x:S 1x=x\top\vdash_{x:S^1} x=x and (x:S)x=x\top\vdash \big (\forall x:S\big ) x=x yields (x:S 0)x=x\top\vdash \big (\forall x:S^0\big ) x=x and (x:S 1)x=x\top\vdash \big (\forall x:S^1\big ) x=x etc. In case, the sequent φψ\varphi\vdash\psi contains nothing to update (e.g. the sequent \top\vdash\bot) one just takes the old sequent as the “new pair”.

Last revised on October 10, 2020 at 13:42:16. See the history of this page for a list of all contributions to it.