ee (Jan 29 2024 at 11:37): ee (Jan 29 2024 at 11:37):I defined a whole graph like structure in a locale, it's composed of two sets, the first set contains objects, the second contains the morphisms on these objects. I also define a congruence relation on the first set, if two objects are connected through a morphism in the second set, they are congruent. How do I define the quotient of the first set based on this relation? I tried using quotient_type but got an error, I couldn't find any examples online about this either.
TIA
Lukas Stevens (Jan 30 2024 at 11:45):It is very likely that quotient_type only works in the global context. This is because type definitions in the local context could depend on locally fixed variables which would essentially give you dependent types.
Lukas Stevens (Jan 30 2024 at 11:46):Maybe you can use the quotient operator //? Otherwise, you could maybe use Types_To_Sets but that is quite cumbersome.
Last updated: Apr 27 2024 at 20:14 UTC