Commit 2022-11-20 06:29 09921751
View on Github →port: Data.Opposite (#650)
Commented the meta code at the end that I cannot handle myself. (Never needed it when using category theory in mathlib3...).
Following the comment (If Lean supported definitional eta equality for records, we could achieve the same goals using a structure with one field.)
in the file, would not it be slightly nicer to use a structure with one field (named unop
?!) for Opposite
instead of a type synonym as it was the case in mathlib3 since it seems that in Lean 4 we would still have nice definitional equalities op_unop
and unop_op
?
Mathlib SHA : fd47bdf09e90f553519c712378e651975fe8c829