# 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 use`op`

and`unop`

explicitly to convert between them.- Both
`unop (op X) = X`

and`op (unop X) = X`

are 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.

(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 use`op`

and`unop`

explicitly to convert between them.- Both
`unop (op X) = X`

and`op (unop X) = X`

are 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.

(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)