nLab Mitchell-Bénabou language



Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category 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




The Mitchell–Bénabou language is a particularly simple form of the internal language of an elementary topos EE. It makes use of the fact that in the presence of a subobject classifier Ω\Omega, there is no need to treat formulas separately from terms, since a formula or proposition can be identified with a term of type Ω\Omega.

Specifically, the language is a type theory L(E)L(E) where:

  • the (closed) types are the objects of EE;

  • the variables of type AA are interpreted as identity morphisms id A:AA\mathrm{id}_A: A \to A in EE;

  • the terms of type BB in variables x ix_i of type X iX_i are interpreted as morphisms from the product of the X iX_i to BB

  • the formulas are terms of type Ω\Omega, where Ω\Omega is the subobject classifier;

  • the propositional logical connectives are induced from the internal Heyting algebra structure of Ω\Omega;

  • the (type-bounded) quantifiers are induced from the internal completeness of Ω\Omega (i.e., the quantifiers are given by suitable morphisms from internal powers of Ω\Omega to Ω\Omega)

  • for each type XX there are also two binary relations = X=_X (defined applying the diagonal map to the product term of the arguments) and X\in_X (defined applying the evaluation map to the product of the term and the power term of the arguments);

  • a formula is true if the arrow which interprets it factors through the arrow true:1Ωtrue: 1 \to \Omega.

  • one can also construct type families and dependent types, just as in any locally cartesian closed category: the types indexed by elements of some closed type AA are the objects of the slice category over AA; sums and products of type families (i.e., Σ\Sigma- and Π\Pi-types) are given by the left and right adjoints to change-of-base functors, respectively. As these slice categories will be topoi themselves, all the above structure can be interpreted for type families as well.


The Mitchell–Bénabou language, like the internal logic of any category, is a powerful way to describe various objects in a topos as if they were sets. It can be viewed as making the topos into a generalized set theory or a type theory, so that we can write and prove statements in a topos, and properties of a topos, using first order intuitionistic predicate logic.

As is usual for type theories, we can conversely generate a syntactic or free topos E(L)E(L) from any suitable theory LL phrased in the above language. The universal property of this topos says that logical functors E(L)EE(L)\to E, for any other topos EE, are equivalent to models of the theory LL in EE.


Last revised on January 15, 2024 at 09:54:21. See the history of this page for a list of all contributions to it.