Opposites #
In this file we define a structure Opposite α
containing a single field of type α
and
two bijections op : α → αᵒᵖ
and unop : αᵒᵖ → α
. If α
is a category, then αᵒᵖ
is the
opposite category, with all arrows reversed.
@[simp]
The type-level equivalence between a type and its opposite.
Instances For
@[simp]
@[simp]
theorem
Opposite.equivToOpposite_symm_coe
{α : Sort u}
:
↑Opposite.equivToOpposite.symm = Opposite.unop
A recursor for Opposite
.
The @[eliminator]
attribute makes it the default induction principle for Opposite
so you don't need to use induction x using Opposite.rec'
.