Xuanrui Qi (Apr 13 2021 at 16:34): Xuanrui Qi (Apr 13 2021 at 16:34):I wonder if there is any interest in porting MathComp to Coq/HoTT. I suspect most of MathComp will stay the same, but by utilizing univalence and transport I suppose we can simplify some proofs?
More generally, has anyone experimented with using packed classes w/ HoTT?
Cyril Cohen (Apr 13 2021 at 17:30):I am interested, and started an experiment back in 2013 at the IAS, together with @Assia Mahboubi. I did not dedicate time to it since then, and will not have time to put some time into it any time soon, although I am still interested. I think @Bas Spitters was conducting such experiments more recently, but that's all I know about it.
Bas Spitters (Apr 13 2021 at 18:10):@Andreas Lynge worked hard on the problem, and made quite a bit of progress. Now that that hott no longer depends on the stdlib it may be somewhat easier than before.
Bas Spitters (Apr 13 2021 at 18:13):This branch, I think:
https://github.com/andreaslyn/HoTT/tree/SSR-THIS-ONE
Bas Spitters (Apr 13 2021 at 18:15):https://github.com/math-comp/math-comp/compare/master...andreaslyn:hott
@Ali Caglayan may also have insights
Ali Caglayan (Apr 13 2021 at 22:29):I doubt that HoTT will offer any simplifications to mathcomp which is already pretty lean. AFAIK mathcomp depends on the coq stdlib so porting mathcomp to HoTT will require a lot of work.
Ali Caglayan (Apr 13 2021 at 22:31):I am also unsure that you need any HoTT if you are thinking about using mathcomp anyway. The simpler solution would be to just use mathcomp with normal coq.
Ali Caglayan (Apr 13 2021 at 22:32):I doubt univalence will offer any new insights into mathcomps completely set based library
Ali Caglayan (Apr 13 2021 at 22:33):I am only saying this since you mentioned you were interested in formalizing algebraic geometry in HoTT before, but I really don't think HoTT will give you anything interesting
Ali Caglayan (Apr 13 2021 at 22:34):algebraic geometry will be mostly set based which can be done in regular coq
Ali Caglayan (Apr 13 2021 at 22:35):All higher algebraic geometry using oo-cats and what not use tools that are not available to HoTT as of current. We don't have a way of talking about higher structures, at least not in regular HoTT
Ali Caglayan (Apr 13 2021 at 22:35):So my recommendation would be to stick to coq :-)
Ali Caglayan (Apr 13 2021 at 22:39):Also I might as well mention that you can define transport with coq's identity type already, this isn't anything specific to HoTT.
Xuanrui Qi (Apr 14 2021 at 03:44):I know you can define transport (it's just a fancy name for rewrite, no?), but I was mainly thinking about univalence and transporting along equivalences. Sometimes I really think I need univalence (not in the sense that "this is not true without univalence", but "it would make my life much easier), but I might be wrong.
Kenji Maillard (Apr 14 2021 at 08:29):Having access to both HoTT (not necessarily univalence, but the theory of equivalences, assuming funext when needed, and sometimes arbitrary quotients) together with mathcomp (and in particular the conveniences of ssreflect's tacticals) would be extremely useful to develop "univalent style" mathematics. In practice I often end up reproving for each project the small subset of HoTT results that I need which is far from optimal.
Ali Caglayan (Apr 14 2021 at 09:45):Then this is more about adding the theory of equivalences, usable funext and quotients to coq. Sure HoTT does a lot of these things, but there isn't any reason you can't do them in coq.
Ali Caglayan (Apr 14 2021 at 09:47):Also if you add univalence to coq, you have to drop things like equality living in prop. This is quite a huge deal when it comes to mathcomp. It still would be possible, but you have to spend a lot of time proving things you really shouldn't be spending time proving (that all equality you are considering is hprop).
Théo Zimmermann (Apr 14 2021 at 09:58):IIUC @Hugo Herbelin would like to add new sorts to Coq (hProp?) or change the meaning of some so that HoTT would become compatible with the rest of the ecosystem (and avoid this kind of dilemma). But I'm not very knowledgeable about all of this. @Kenji Maillard probably understands better what it would entail and the plans about this.
Bas Spitters (Apr 14 2021 at 11:08):Yes, better support would certainly be helpful. @Ali Caglayan you may want to comment on that issue.
https://github.com/coq/ceps/pull/55
Cyril Cohen (Apr 14 2021 at 11:35):@Ali Caglayan
(that all equality you are considering is hprop).
I'm not sure that's a big problem for mathcomp, many equalities are decidable hence automatically in hProp...
More generally, I'm not sure I understand your arguments about the non usefulness of using mathcomp on HoTT... maybe you are thinking of mathcomp as a static object, which would indeed not gain anything by being ported to HoTT.
However mathcomp is also what it is because of the restrictions of Coq and is trying very hard to circumvent them, for me going towards HoTT would be more that a simple recompilation of mathcomp on top of HoTT, but making heavy refactoring, removing unnecessary hacks and enabling new features... and maybe finding new hacks à la mathcomp to circumvent new restrictions, who knows...
Ali Caglayan (Apr 14 2021 at 11:39):OK so I seem to be a bit confused. It seemed to me that people were interested in making a port of mathcomp to HoTT. To this I say I don't see the point. But if you want to use features of HoTT (no prop, quotients, univalence) in mathcomp that's an entirely different story.
Ali Caglayan (Apr 14 2021 at 11:40):In that case, I have no objection, mathcomp should always strive to be better.
Ali Caglayan (Apr 14 2021 at 11:41):What I thought before was: "I want to do algebraic geometry in HoTT" -> "there is not enough algebra" -> "mathcomp has a lot of algebra" -> "let's port mathcomp to HoTT"
Ali Caglayan (Apr 14 2021 at 11:41):If mathcomp gets redesigned to use features of HoTT then there is no problem anymore.
Notification Bot (Apr 14 2021 at 12:52):This topic was moved by Cyril Cohen to #Hierarchy Builder devs & users > HB for HoTT?
Cyril Cohen (Apr 14 2021 at 12:54):FTR I moved my fork of the discussion from mathcomp to HB to the #Hierarchy Builder devs & users stream.
Last updated: Jan 29 2023 at 19:02 UTC