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
logic | category theory | type theory |
---|---|---|
true | terminal object/(-2)-truncated object | h-level 0-type/unit 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
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) 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
</table>
The Mitchell–Bénabou language is a particularly simple form of the internal language of an elementary topos $E$. 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)$ where:
the variables of type $A$ are interpreted as identity morphisms $\mathrm{id}_A: A \to A$ in $E$;
the terms of type $B$ in variables $x_i$ of type $X_i$ are interpreted as morphisms from the product of the $X_i$ to $B$
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 $X$ there are also two binary relations $=_X$ (defined applying the diagonal map to the product term of the arguments) and $\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 \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 $A$ are the objects of the slice category over $A$; 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)$ from any suitable theory $L$ phrased in the above language. The universal property of this topos says that logical functors $E(L)\to E$, for any other topos $E$, are equivalent to models of the theory $L$ in $E$.
Last revised on July 5, 2017 at 08:27:09. See the history of this page for a list of all contributions to it.