In this file we define a type synonym
opposite α := α, denoted by
αᵒᵖ and two synonyms for the
op : α → αᵒᵖ and
unop : αᵒᵖ → α. If
α is a category, then
αᵒᵖ is the opposite
category, with all arrows reversed.
The type of objects of the opposite of
α; used to define the opposite category.
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.)