search

UniMath / UniMath

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
http://unimath.org/
Other
952 stars 172 forks source link

Get material from workshop on univalent mathematics 2019 merged into UniMath #1501

Open benediktahrens opened 2 years ago

benediktahrens commented 2 years ago

@jozefg wrote some code on Grothendieck universes, available at https://github.com/unimath2019-tt/UniMath/pull/1. Can it get merged into UniMath? @mortberg

mortberg commented 2 years ago

Even if we polish it up we're using an Inductive (https://github.com/unimath2019-tt/UniMath/pull/1/files#diff-452b433f08e8e74d6437469aa8fde510c75068ffb77a815cb2aa0ce3006c183aR185) in the core definition. So unless the UniMath policy on inductive types has changed I'm afraid that preparing the PR to be merged will involve a lot of work. One quick fix would be to just parametrize the development by the existence of the inductive that we need, but that's a bit unsatisfactory and will probably break some proofs because computation rules not being definitional...

mortberg commented 2 years ago

Or is there some construction of W types in UniMath that I'm not aware of? I have a vague recollection that another group at the same school worked on this following Felix Rech's work, but I'm not sure if that was ever finished?

benediktahrens commented 2 years ago

Good point - as such, it cannot go into UniMath/UniMath, but in some satellite repository. There is code on W- and M-types in https://github.com/UniMath/UniMath/tree/master/UniMath/Induction. I have not studied that material, and thus don't know if it would suffice to replace the inductive type used.

rmatthes commented 2 years ago

The outcome of the UniMath 2019 school on Rech's construction is ComputationalM.v. The extension to families was under way. Rech had this already before, but his code was not connected to the UniMath library. The whole point of Rech's construction was to get the desired equations definitionally. It this is not needed, the other code in package Induction could be useful.