Zulip Chat Archive

Stream: general

Topic: extensionality as a typeclass

Kevin Buzzard (Mar 26 2020 at 11:10):

For all these bundled homs, the extensionality lemma can be expressed as saying that ⇑ is injective. Is this some well-known type theory concept? Is injective coe a thing?

Kevin Buzzard (Mar 26 2020 at 11:11):

Is this something to do with norm_cast?

Mario Carneiro (Mar 26 2020 at 11:16):

Isn't this basically the condition behind a concrete category?

Last updated: Dec 20 2023 at 11:08 UTC