In this file we define a type synonym
opposite α := α, denoted by
αᵒᵖ and two synonyms for the
op : α → αᵒᵖ and
unop : αᵒᵖ → α. The type tag
αᵒᵖ is used with two different
αis a category, then
αᵒᵖis the opposite category, with all arrows reversed;
αis a monoid (group, etc), then
αᵒᵖis the opposite monoid (group, etc) with
op (x * y) = op x * op y.
The type of objects of the opposite of
α; used to define the opposite category or group.
In order to avoid confusion between
α and its opposite type, we
set up the type of objects
opposite α using the following pattern,
which will be repeated later for the morphisms.
opposite α := α.
- Define the isomorphisms
op : α → opposite α,
unop : opposite α → α.
- Make the definition
This has the following consequences.
αare distinct types in the elaborator, so you must use
unopexplicitly to convert between them.
unop (op X) = Xand
op (unop X) = Xare definitional equalities. Notably, every object of the opposite category is definitionally of the form
op X, which greatly simplifies the definition of the structure of the opposite category, for example.
(If Lean supported definitional eta equality for records, we could achieve the same goals using a structure with one field.)