search

lawrencecpaulson / lawrencecpaulson.github.io

the blog "Machine Logic"
12 stars 0 forks source link

https://lawrencecpaulson.github.io/2022/03/30/Quotienting.html #10

Open utterances-bot opened 2 years ago

utterances-bot commented 2 years ago

Equivalence classes and quotienting

https://lawrencecpaulson.github.io/2022/03/30/Quotienting.html

jonsterling commented 2 years ago

Thanks for the post, I've been enjoying these explanations of Isabelle-land as a type theorist. Maybe someone would call me a "purist" but I am nonetheless not outraged by Lean approach --- it is true that it disrupts some computational properties of the Lean type system that type theorists like, but personally I don't see a big problem with it. What is important about any implementation of quotients is that it meets the mathematical need --- if it disrupts some properties of the type theory, then so much worse for the type theory.

It is worth noting that the quotients of Nuprl are a bit different --- while Lean's quotients are mathematically useful but have some computational problems, Nuprl's quotients have no such computational problems but they are unfortunately not very mathematically useful. The problem is that quotients in Nuprl are not effective (or another way to put it is, not all equivalence relations in Nuprl are effective), and they cannot be in general. Effectivity means that if two elements are identified by the quotient map, then they lie in the equivalence relation.

The failure of effectivity defect renders Nuprl's quotients somewhat unusable for doing mathematics, so users of Nuprl end up in setoid hell in practice, in spite of the inclusion of quotient types. This situation stands in contrast to the quotients of Isabelle/HOL and of Lean, as well as the quotients that can trivially be axiomatized in Coq, which all are compatible with effectivity.

The last thing I would say is, we 'pure type theorists' have been pushing a different approach to quotients for several years that has all the good semantic/mathematical properties of real quotients (e.g. those of HOL and Lean) without sacrificing the good computational properties of quotients that type theorists would prefer to have. These new quotients are called 'quotient inductive types', a special case of higher-inductive types, and can be implemented in cubical type theory. I realize that cubical type theory is itself quite complex, of course, but we also have other reasons to be interested in it.

Thanks again for your posts!