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

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





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 December 13, 2023 at 15:35:13. See the history of this page for a list of all contributions to it.