|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|logical conjunction||product||product type|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
In particular for two terms
f g: X -> Y
p: f == g
between them is to be thought of as a homotopy or natural transformation (a -transfor). In particular it implies, one can prove, that there are families of paths between all the values of the functions
happly f g p: forall x: X, f x == g x .
From a purely intensional point of view, this is to be expected — two functions could be defined in different ways, and thus be intensionally different, yet produce the same values on all inputs (i.e. be extensionally the same).
However, in many contexts one wants to treat functions extensionally, such as when regarding type theory as the internal language of some category. In particular, this is the case in homotopy type theory, where one wants to interpret the type theory as the internal language of an (∞,1)-topos, for instance of Top ∞Grpd.
In such an internal logic context, a family of anything must always mean “continuous family”, so that a family of paths between the values of two functions is a continuous homotopy between them, and hence ought to induce a path between them in the function-space. Thus, one wants to impose the condition that from a term
eta: forall x: X, f x == g x .
we can deduce an actual path between and .
Translating this into direct categorical terms, the term gives a map
where is the identity type or space of paths in . Such a section is tantamount to a lift of . From this we would like to deduce an actual path .
So, very simply, function extensionality means we are able to lift elements through a canonical map that is obtained from a dependent eliminator?.
Of course we are not just interested in global elements here. What we really want is an actual section of in the slice over (although this can be derived from the global element formulation by using the Yoneda lemma together with currying and uncurrying tricks). This condition may be called “naive” or “weak” function extensionality, in view of an apparently stronger condition that this section (and therefore also ) be equivalences. This latter condition might be called “strong function extensionality”.
Under reasonable assumptions on the type theory, it turns out that these and other versions of function extensionality are equivalent; for now see (Lumsdaine) below. In any case, if the type theory has an extra axiom that implies some such version, one says that function extensionality holds.
Notice that every presentable locally Cartesian closed (∞,1)-category (by the discussion there) has a presentation by a right proper Cisinski model category. Accordingly we may say that every presentable locally Cartesian closed (∞,1)-category interprets HoTT+FunExt.
An introduction to the relevant notions and a guided walk through the formal proof that univalence implies functional extensionality is at
A discussion of various flavors of function extensionality, and how to move between them, can be found in
Richard Garner, On the strength of dependent products in the type theory of Martin-Löf