natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
For any geometric theory there exists a geometric theory , the theory of -model homomorphisms, whose models in a Grothendieck topos are precisely the homomorphisms between -models in .
Let be a geometric theory over the signature .
Let be the signature containing a pair of new sort symbols , and a new function symbol for any sort symbol in , as well, as pairs , of new functions symbols (resp. pairs , of new relation symbols) for any function symbol (resp. relation symbol ) in .
The theory of -model homomorphisms is the theory over the signature with the following sequents:
for any pair , of function symbols in corresponding to in (in case , the sequent reads ), resp. any pair , of relation symbols in corresponding to in (in case , the sequent reads ).
Let be a Grothendieck topos. Then
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 -model homomorphisms once the -models in the arrow categories are known.
Remark: This e.g. precludes the existence of geometric theories or with the property that, given a geometric theory , the category of models and coincide with the opposite category or the twisted arrow category for any Grothendieck topos, respectively. In particular, since the (geometric) theory of morphisms (see the examples below) assigns the arrow category as category of models to a Grothendieck topos no geometric theory can assign all Grothendieck toposes their twisted arrow category as category of models because the class of models coincides with the class of models for the theory of morphisms.
Since in general and the Sierpinski topos is exponentiable, one gets
or in other words
The classifying topos for the theory of -model homorphisms is .
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 , one sees that the formats of the more expressive subdoctrines like Horn, regular, and coherent logic are respected by the passage to . 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 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 is necessarily 2-sorted.
By an observation of Hébert (2010, p.1), the finitely presentable objects in arrow categories , are precisely the morphisms between finitely presentable objects in whence, denoting the subcategory of finitely presentable models of a theory in a topos by one has
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 (cf. Johnstone 2002b, p. 891) one has
Let be a cartesian theory. Then the theory of -model homorphisms is cartesian and its classifying topos is .
For an easy application of this result see at the theory of objects in the examples below!
Let and be the empty theory, resp., the inconsistent theory, over the empty signature. Then and 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 be the theory of objects i.e. the theory with no sequents over the signature with one sort symbol . Then is the theory with no sequents over the signature with two sort symbols , and a function symbol . Clearly, its models in a Grothendieck topos are the morphisms of and, accordingly, is called the theory of morphisms.
It is the dual theory of the theory classified by the Sierpinski topos , or in other words, its classifying topos called the morphism classifier (cf. Johnstone 1977, p.184; 2002, p.426) is
The generic morphism is given by the natural transformation with the generic object i.e. the inclusion functor , and the domain projection functor, and the codomain projection functor, with components .
Let be the theory of categories (e.g. Johnstone 1977, p.202) whose models in a Grothendieck topos are the internal categories . Then is the theory of functors. likely being the most famous cartesian theory, one has .
The Sierpinski topos is a connected, locally connected and local topos. As a result of Artin gluing along it has two topos points (corresponding to the two points of the underlying Sierpinski space). Whence one can take as an abstract interval object for a homotopy theory of Grothendieck toposes correlated with their nature as “generalized spaces” and view, accordingly, the exponential as a path space for .
(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. 30 AMS 1984.
Saunders Mac Lane, Ieke Moerdijk, Sheaves in Geometry and Logic , Springer Heidelberg 1994.
It is understood that variables and contexts are updated with the new sorts e.g. the sequent yields two sequents and and yields and etc. In case, the sequent contains nothing to update (e.g. the sequent ) one just takes the old sequent as the “new pair”. ↩
Last revised on October 22, 2024 at 10:09:10. See the history of this page for a list of all contributions to it.