Opposites #
In this file we define a type synonym Opposite α := α
, denoted by αᵒᵖ
and two synonyms for the
identity map, 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.
- Define
Opposite α := α
. - Define the isomorphisms
op : α → Opposite α
,unop : Opposite α → α
. - Make the definition
Opposite
irreducible.
This has the following consequences.
Opposite α
andα
are distinct types in the elaborator, so you must useop
andunop
explicitly to convert between them.- Both
unop (op X) = X
andop (unop X) = X
are definitional equalities. Notably, every object of the opposite category is definitionally of the formop X
, which greatly simplifies the definition of the structure of the opposite category, for example.
(Now that Lean 4 supports definitional eta equality for records, we could achieve the same goals using a structure with one field.)
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.
- Define
Opposite α := α
. - Define the isomorphisms
op : α → Opposite α
,unop : Opposite α → α
. - Make the definition
Opposite
irreducible.
This has the following consequences.
Opposite α
andα
are distinct types in the elaborator, so you must useop
andunop
explicitly to convert between them.- Both
unop (op X) = X
andop (unop X) = X
are definitional equalities. Notably, every object of the opposite category is definitionally of the formop X
, which greatly simplifies the definition of the structure of the opposite category, for example.
(Now that Lean 4 supports definitional eta equality for records, we could achieve the same goals using a structure with one field.)
Equations
- «term_ᵒᵖ» = Lean.ParserDescr.trailingNode `term_ᵒᵖ 1024 0 (Lean.ParserDescr.symbol "ᵒᵖ")
Equations
- Opposite.instInhabitedOpposite = { default := Opposite.op default }
A recursor for Opposite
. Use as induction x using Opposite.rec
.
Equations
- Opposite.rec h X = h (Opposite.unop X)