[FOM] New umbrella? (Freek Wiedijk)
Paul B Levy
P.B.Levy at cs.bham.ac.uk
Mon Nov 3 13:26:50 EST 2014
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 Blain Levy
School of Computer Science, University of Birmingham
More information about the FOM