Stream: Hierarchy Builder devs & users

Topic: HB for HoTT?


view this post on Zulip Cyril Cohen (Apr 14 2021 at 12:07):

@Xuanrui Qi in particular, using HB on HoTT is something I'd really like to try. (cc @Enrico Tassi)

view this post on Zulip Xuanrui Qi (Apr 14 2021 at 12:08):

Actually, MathComp has way too little algebra for any serious algebra project that is not group theory. I wanted to do algebraic geometry, but not necessarily in HoTT. It just seems that univalence is something that could help me.

view this post on Zulip Xuanrui Qi (Apr 14 2021 at 12:08):

@Cyril Cohen I am also interested - I might also talk to @Reynald Affeldt about this

view this post on Zulip Reynald Affeldt (Apr 14 2021 at 12:10):

@Xuanrui Qi I’ll be happy to give a hand since we are in the same time zone, I am learning hb the hard way right now :-/

view this post on Zulip Bas Spitters (Apr 14 2021 at 12:41):

@Cyril Cohen @Enrico Tassi would it be possible to target HoTT-classes with HB?
@Gaëtan Gilbert may also have insights on this
https://github.com/HoTT/HoTT/tree/master/theories/Classes
https://github.com/SkySkimmer/HoTTClasses

view this post on Zulip Bas Spitters (Apr 14 2021 at 12:43):

It would also be interesting to consider how HB fits with universal algebra @Andreas Lynge is working on this.
https://github.com/HoTT/HoTT/tree/master/theories/Algebra/Universal

view this post on Zulip Cyril Cohen (Apr 14 2021 at 12:44):

(Theoretically speaking, there should not, but I'm not sure the universe polymorphism API of coq-elpi will follow as of today, @Enrico Tassi did you make some progress? I gathered it was low priority, compared to porting mathcomp, but maybe after that?)

view this post on Zulip Enrico Tassi (Apr 14 2021 at 12:45):

I have a branch, but it changes too many API to be named other than coq-elpi 2.0

view this post on Zulip Enrico Tassi (Apr 14 2021 at 12:46):

And, to be honest, I don't like the new API much, since the gref data type is now almost always accompained by a univ-instance

view this post on Zulip Enrico Tassi (Apr 14 2021 at 12:46):

see https://github.com/LPCIC/coq-elpi/pull/190 , in particular this diff: https://github.com/LPCIC/coq-elpi/pull/190/files#diff-dfa6bd6976ca3464c87f36bd82b13a799dd2990882000e85a0964e61573ec1e7

view this post on Zulip Enrico Tassi (Apr 14 2021 at 12:49):

What I don't like is that a used which does not care/use univpoly, is still hit by the API change

view this post on Zulip Enrico Tassi (Apr 14 2021 at 12:49):

And I'm all ears on different approaches...

view this post on Zulip Cyril Cohen (Apr 14 2021 at 12:51):

Well since you are the pro of Constraint Handling Rules, I'm quite worried that you do not have an answer based on that :worried:

view this post on Zulip Enrico Tassi (Apr 14 2021 at 12:52):

The problem is not in the constraints. The problem is that abstraction and instantiations of universe levels are not regular abstractions and applications.

view this post on Zulip Enrico Tassi (Apr 14 2021 at 12:52):

(this is how it is done inside Coq, and how the API esposes it)

view this post on Zulip Notification Bot (Apr 14 2021 at 12:52):

This topic was moved here from #math-comp users > MathComp for HoTT? by Cyril Cohen

view this post on Zulip Cyril Cohen (Apr 14 2021 at 12:53):

Enrico Tassi said:

The problem is not in the constraints. The problem is that abstraction and instantiations of universe levels are not regular abstractions and applications.

I see...

view this post on Zulip Enrico Tassi (Apr 14 2021 at 12:53):

every time you pair a gref with a univ-instance, you are forming the application, morally...

view this post on Zulip Enrico Tassi (Apr 14 2021 at 12:55):

I could also pretend to have a sort/binder for universe levels, and a ulevel term constructor. But the embed/readback function from/to Coq would be much harder

view this post on Zulip Enrico Tassi (Apr 14 2021 at 12:57):

I mean app[global (const "id"), uinstance [set], global (indt "nat"), global (indc "O")] would be the polymrphic identity applied to 0

view this post on Zulip Enrico Tassi (Apr 14 2021 at 12:59):

maybe it's not so hard after all ;-)

view this post on Zulip Enrico Tassi (Apr 14 2021 at 13:03):

but I also need a type for uinstance in order to write fun "u" ??? u\ app[global (const "id"), uinstance u]

view this post on Zulip Enrico Tassi (Apr 14 2021 at 13:04):

Doesn't Agda have such a sort?

view this post on Zulip Cyril Cohen (Apr 14 2021 at 13:06):

and lean

view this post on Zulip Cyril Cohen (Apr 14 2021 at 13:06):

Sort u

view this post on Zulip Enrico Tassi (Apr 14 2021 at 13:13):

I mean, the type of u

view this post on Zulip Enrico Tassi (Apr 14 2021 at 13:14):

Coq has Type@{u} and coq-elpi has sort (typ u))

view this post on Zulip Enrico Tassi (Apr 14 2021 at 13:15):

but u is "meta". I want to make it a proper term. So I can add a term constructor injecting this thing into terms, eg uinstance u, but I need its type (as a term), as in coq.typecheck (uinstance u) ??? ok.

view this post on Zulip Enrico Tassi (Apr 14 2021 at 13:16):

I believe it should be a new sort, decorrelated to the others.

view this post on Zulip Enrico Tassi (Apr 14 2021 at 13:20):

Morally, the prenex universe polymorphism is an extesion of CIC where this sort can only appear in a prenex spine of binders to global constants/inductive, and where all univpoly constants are always applied to at least the arguments standing for these abstractions. But the implementation is totally different.

view this post on Zulip Enrico Tassi (Apr 14 2021 at 13:21):

Maybe @Matthieu Sozeau can confirm that my intuition is not completely wrong

view this post on Zulip Matthieu Sozeau (Apr 14 2021 at 20:15):

Yes, that's the way it is implemented today. The univ polymorphism is prenex on global references (forall u, Type@{u} -> Type@{u} doesn't have a "type"). The alternative, in Agda for example would give it type Set@{omega} which itself doesn't have a type.

view this post on Zulip Matthieu Sozeau (Apr 14 2021 at 20:19):

The advantage of not using "regular" binders for univ variables is that we can have a clean treatment of cumulative inductives, and an optimized substitution for universes. This matters when we have a lot of them: this is the case currently because we don't have a good decision procedure for the theory of univ variables with +1, <= and max.

view this post on Zulip Matthieu Sozeau (Apr 14 2021 at 20:21):

If we can get past that obstacle, then I guess it would make sense to have Univ be treated as a specific sort and use the same binding mechanism.

view this post on Zulip Bas Spitters (Apr 14 2021 at 20:47):

Sounds like a problem in tropical geometry. I don't know enough about the algorihms in that field (but there is a theory of that).
https://en.wikipedia.org/wiki/Tropical_geometry


Last updated: Jan 29 2023 at 15:02 UTC