Commit 2022-11-20 06:29 09921751

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