I did some renaming per @jcommelin's suggestions, making things slightly less ugly.

This looks generally clearer. Another op-tion is the Haskell-style

structure op_cat (C : Type u₁) : Type u₁ := op :: (unop : C)

which will make C and its opposite category distinct things in the kernel as well as in the elaborator. I'm not sure whether that is a good thing or a bad thing though.

The choice might affect the pretty-printer for example--Lean just asked me for a F ≅ F', but I gave it one and surprise, it wanted an isomorphism in the opposite category! It would be nice if it would show op F ≅ op F' then.

@digama0 Is there anything controversial left in this PR? (Note that the title is now misleading... see the latest commit.)

I'd like to continue to advocate for using irreducible type synonyms for both the objects and the morphisms of the opposite category. In outline:

• It's important to consistently use the correct "spelling" (e.g., op X) for objects and morphisms of the opposite category, so as to both eliminate ambiguity in Lean input and output (e.g., goals) and also guide automated reasoning.
• In principle we could always use the correct spelling even with an ordinary semireducible type synonym, but in practice it's too difficult to always get it right without automated checking.
• The irreducible type synonym approach enforces correct spelling while introducing almost no additional overhead for the user (see below).
• Using a structure instead of an irreducible type synonym introduces serious complications, starting already at the definition of the opposite category. (The obvious definition id := λ X, (𝟙 (unop X)).op doesn't type check because the right hand side has the type op (unop X) ⟶ op (unop X) not X ⟶ X.)
• In a language like Coq that supports definitional eta for records, these complications would not arise. Lean does not support definitional eta for records but we can simulate the case of a one-field record using the irreducible type synonym method and (if even necessary?) consider the support in other languages as justification for the use of this method.

Concretely, I suggest 89379bc, which is basically a cleaned-up implementation of the original version of this PR. Of note:

• Most of the changes are to insert op or unop as needed in the statements of definitions and lemmas.
• Few proofs are affected, and only in simple ways.
• A number of proofs can be deleted because tidy now has the correct information to produce them automatically. In particular, the lemmas op_id_app and op_comp_app were required for category_theory.cocones, but tidy now succeeds without them.

I was originally intending to also prepare a version which uses a structure in place of the irreducible type synonym, but in view of the complications which arose already with the category instance for the opposite category I decided not to finish it.

Okay, go ahead. Get this PR working or make a replacement and I'll merge it.

@rwbarton Thanks a lot for this thorough review of the options! I'm glad we're converging towards a solution.

New PR at #627. It contains only the minimum changes to opposite and not the handful of other improvements in this PR.

@semorrison, would you like me to make new PRs for the parts of this not covered by #627 and #633?

I'm closing this; everything has been divided up into smaller PRs.