[FOM] formal proofs

[Hendrik Boom]

On Thu, Oct 23, 2014 at 05:43:09PM +0200, Urs Schreiber wrote:

...
> only that it is yet a bit better even. Where Paul Taylor argued that
> type theory and its categorical semantics offers a practical advantage
> over traditional foundations, homotopy type theory carries this
> further and observes that taking the constructive aspect fully
> seriously in taking intensional identity types fully seriously makes
> type theoretic foundations actually be a practically useful formal
> language for homotopy theory and topics that are considered in
> contemporary research algebraic topology.

Do I understand this correctly -- we have intensional identity here 
because we care about the specific witness; i.e., the path?  And 
Martin-Lof's theory has extensional identity becaue he  doesn't care 
about the witness in an identity type, and just lets all them be 'r', 
so to speak?

-- hendrik