[FOM] New umbrella? (Freek Wiedijk)

[Paul B Levy]

On 03/11/14 12:00, Freek Wiedijk wrote:

> Still in Mizar
> you certainly can do abstract mathematics very well, and
> both set theory and category theory are seriously present.
> And it has dependent types.  And in a way that's much more
> pleasant than the way you get it in type theory.
>
> I certainly can imagine an improved system, like Mizar but
> with the most irritating flaws fixed and the more important
> Coq/Isabelle goodies added on top, that would easily handle
> abstract mathematics well, without needing to stomach the
> ideosyncracies of type theory.

Thanks Freek.  Just to point out: "type theory" and "Martin-Lof type 
theory" are not synonymous.  The latter is designed to make typing 
decidable, so that a proof can be just a lambda-term, with no additional 
evidence needed that it has a given type.  To achieve this goal, various 
restrictions (aka "idiosyncrasies") are required, notably the 
disallowance of judgemental eta-laws for sum type (A+B) and identity 
type.  (See Notes on Chapter 1 of the HoTT book.  Univalence, to some 
extent, repairs the damage caused by these restrictions.)

By contrast, in "extensional" dependent type theory,  all the eta-laws 
are allowed, which is theoretically very natural, corresponding to the 
categorical notion of "adjoint".  But because typing is undecidable, 
this theory can't form the basis of a proof assistant in which a proof 
is in all cases just a lambda-term.

Paul

-- 
Paul Blain Levy
School of Computer Science, University of Birmingham
http://www.cs.bham.ac.uk/~pbl