nLab geometric type theory



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

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type/path type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
completely presented setdiscrete object/0-truncated objecth-level 2-type/set/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
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





Geometric type theory is a conjectural extension of geometric logic to an extensional dependent type theory. That is, it is supposed to be a dependent type theory which under the relation between category theory and type theory corresponds to sheaf toposes, and is preserved by geometric morphisms.

At present it is not clear exactly how such a type theory should be defined.

A motivating example is a geometric theory as follows. Its signature has one sort, NN, and two function symbols 0:1N0\colon 1 \to N and s:NNs \colon N \to N. Its axioms are -

  • 0=s(n) n0 = s(n) \vdash_{n} \bot
  • s(n)=s(n) nnn=ns(n) = s(n') \vdash_{n n'} n=n'
  • n in=s i(0)\top \vdash_{n} \bigvee_{i} n=s^{i}(0)

(“s i(0)s^{i}(0)” is not a term in the formal language, but ii indexes an inductively defined sequence of formulae “n=s i(0)n=s^{i}(0)”.)

In any model (in a Grothendieck topos) the interpretation of NN is uniquely isomorphic to an nno, so the nno can be characterized uniquely up to isomorphism by geometry theory - something that would be impossible in finitary first-order logic. There is essentially only one model, and this theory is equivalent to the empty theory. What this illustrates is that a sort for the nno can be added “for free” to any theory - and this is consistent with the fact that nno’s are preserved by inverse image functors.

List objects (ListXList X is the set of finite sequences of elements from XX) can similarly be added “for free”, and in fact the same goes for free constructions for cartesian theories. Thus such constructors can be added as a type theoretic adjunct to geometric logic without altering its expressive power. Since geometric type theory also includes quotient types, the constructions are similar to quotient inductive types.

As an example, the geometric theory of a real number can be rewritten in a form that more directly describes Dedekind sections of rationals, with sort QQ that is geometrically constrained to be the rationals. For further details, see Vickers 2007.

All this leads to a conjecture of a “geometric type theory”, geometric logic enhanced with the geometrically definable types.

An “arithmetic type theory” has now been formalized Vickers 2018 by adjoining such type constructors to coherent logic. Categorically, it corresponds to replacing Grothendieck toposes with arithmetic universes. Although it lacks the infinitary disjunctions of geometric logic, they can in many cases be provided by existential quantification over infinite sorts. Vickers 2017 shows how it can be used to prove base-free results for (relative) Grothendieck toposes.


  • Steve Vickers, Locales and toposes as spaces, Handbook of Spatial Logics, Springer 2007 (pdf)

  • Steve Vickers, Arithmetic universes and classifying toposes, Cahiers de topologie et géométrie différentielle catégorique 58 (4) (2017), pp. 213-248 (pdf)

  • Steve Vickers, Sketches for arithmetic universes, accepted 2018 for Journal of Logic and Analysis (pdf)

Last revised on January 20, 2020 at 03:49:43. See the history of this page for a list of all contributions to it.