# 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'`

.