The word "extensionality" is used explicitly in 1940 Church's paper "A formulation of the simple theory of types" in connection with what we call today "functional extesnionality" and "propositional extensionality" ("univalence for propositions") (see p. 61). 

Church there also clearly refers to earlier uses of this word without giving references.

I do not know whether the word "intensional" been in use for so long or not.

V.








On Jan 27, 2014, at 10:20 AM, Steve Awodey <notifications@github.com> wrote:

> In basics.tex:
> 
> > @@ -2453,8 +2453,10 @@ \section{Universal properties}
> >  \index{type theory!extensional}%
> >  \index{reflection rule}%
> >  As mentioned in the notes to \autoref{cha:typetheory}, our identity types are those that belong to \emph{intensional} type theory, by contrast with those of \emph{extensional} type theory which have an additional ``reflection rule'' saying that if $p:x=y$, then in fact $x\jdeq y$.
> > -This reflection rule implies that all the higher groupoid structure collapses (see \autoref{ex:equality-reflection}), so for nontrivial homotopy we must use the intensional version. 
> > -One may argue, however, that homotopy type theory is in another sense more ``extensional'' than traditional extensional type theory, because of the function extensionality and univalence axioms.  
> > +This reflection rule implies that all the higher groupoid structure collapses (see \autoref{ex:equality-reflection}), so for nontrivial homotopy we must use the intensional version.
> > +The terminology is somewhat confusing, however: it is not the identity types of intensional type theory that are intensional, but rather the judgmental equality.
> > +Intensional type theory is so named because it can distinguish an ``intensional'' judgmental equality from the ``extensional'' identity type, as opposed to extensional type theory in which the reflection rule forces \emph{both} of them to be extensional.
> > +The univalence axiom, like function extensionality, can be considered an additional ``extensionality'' property for the identity type; its incompatibility with the reflection rule means that intensional type theory allows for identity types that are ``more extensional'' than extensional type theory does.
> the remark about ua can perhaps be omitted here because it is confusing and disrupts the line of thought.
> alternately, it could be reformulated as:
> The univalence axiom, like function extensionality, can be seen as an extensionality'' property of the identity type; its incompatibility with the reflection rule means that intensional type theory with univalence is, in a sense, evenmore extensional'' than extensional type theory (an unfortunate clash of terminology).
> 
> —
> Reply to this email directly or view it on GitHub.
>