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?

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.

@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.

This branch, I think:

https://github.com/andreaslyn/HoTT/tree/SSR-THIS-ONE

https://github.com/math-comp/math-comp/compare/master...andreaslyn:hott

@Ali Caglayan may also have insights

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.

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.

I doubt univalence will offer any new insights into mathcomps completely set based library

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

algebraic geometry will be mostly set based which can be done in regular coq

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

So my recommendation would be to stick to coq :-)

Also I might as well mention that you can define transport with coq's identity type already, this isn't anything specific to HoTT.

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.

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.

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.

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).

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.

Yes, better support would certainly be helpful. @Ali Caglayan you may want to comment on that issue.

https://github.com/coq/ceps/pull/55

@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...

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.

In that case, I have no objection, mathcomp should always strive to be better.

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"

If mathcomp gets redesigned to use features of HoTT then there is no problem anymore.

This topic was moved by Cyril Cohen to #Hierarchy Builder devs & users > HB for HoTT?

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