I am quite familiar with the history of these terms, which goes back to Whitehead and Russell’s Principia Mathematica.  I will a brief note on this in the next day or two.

On Jan 27, 2014, at 8:55 PM, Vladimir Voevodsky <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.
> I suggest that you remove all discussion of these issues unless someone is willing to spent time really finding out, through the reading of sources, the history of the use of these words in logic (which I suspect goes back at least to works on combinatory logic). It is much better not to say anything on this subject than to introduce more oversimplified, and consequently false, explanations. V.
> …
> —
> Reply to this email directly or view it on GitHub.
>