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

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.

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

@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 :-/

@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

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

(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?)

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

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`

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

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

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

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:

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

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

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

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

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

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

I mean `app[global (const "id"), uinstance [set], global (indt "nat"), global (indc "O")]`

would be the polymrphic identity applied to 0

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

but I also need a type for `uinstance`

in order to write `fun "u" ??? u\ app[global (const "id"), uinstance u]`

Doesn't Agda have such a sort?

and lean

`Sort u`

I mean, the type of `u`

Coq has `Type@{u}`

and coq-elpi has `sort (typ u))`

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`

.

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

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.

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

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.

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.

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.

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