groupoids

Stream: maths

[Jakob von Raumer]

I noticed that there is a lot of groupoid laws the proofs of which are repeated for each notion of equaity/iso which is introduced. Why are they not derived in a commond groupoid class? I'm thinking of eq, equiv, add_equiv, mul_equiv, ...

[Eric Wieser]

My memory at trying to do this thing is that:

• It's difficult to state lawfulness of coercion because Lean 3's has_coe_to_fun doesn't take the codomain as an argument
• It's hard to avoid wanting (and then being unable) to quantify over universes when stating composition

[Jakob von Raumer]

Ah, the second point is a really good one, thanks.

[Jakob von Raumer]

I don't really get the first one, since most of the groupoid laws (cancellation, trans_refl, ...) don't use the has_coe_to_fun at all...

[Eric Wieser]

Sure, but you probably want to also have your typeclass prove things like f.comp g x = f (g x)

[Eric Wieser]

Although that doesn't have to be the same typeclass I guess