Commit 2023-04-18 01:37 d090d0a8

View on Github →

chore: made Opposite a structure (#3193) The opposite category is no longer a type synonym, but a structure.

Estimated changes

modified def Quiver.Hom.op
modified def Quiver.Hom.unop
modified def Opposite.op
modified theorem Opposite.op_injective
deleted def Opposite.unop
modified theorem Opposite.unop_injective
added structure Opposite
deleted def Opposite
modified theorem Set.singleton_op
modified theorem Set.singleton_op_unop
modified theorem Set.singleton_unop
modified theorem Set.singleton_unop_op