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.




On Jan 27, 2014, at 10:11 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.
> how about this in place of 2458:
> Intensional type theory is so named because its judgmental equality is ``intensional'' in the sense that it does not strictly respect the relation of propositional equality, as opposed to extensional type theory in which the reflection rule forces the two to agree.
> 
> —
> Reply to this email directly or view it on GitHub.
>