3.9. Equivalences of categories
An equivalence between two categories C and D is a term in the
type Equivalence C D, which is denoted C ≌ D, where ≌ (typed as \backcong)
should not be confused with ≅ (typed as \cong). Such a an equivalence
consists of two functors functor : C ⥤ D and inverse : D ⥤ C,
and two isomorphisms unitIso : 𝟭 C ≅ functor ⋙ inverse and
counitIso : inverse ⋙ functor ≅ 𝟭 D which satisfy a triangle identity
(similarly as units and counits of adjunctions do).
The equivalence between the opposite of the opposite of a category C
and the category C can be defined as follows:
-- the mathlib definition is `opOpEquivalence`
@[simps, implicit_reducible]
def opOpEquivalence' (C : Type*) [Category* C] :
Cᵒᵖᵒᵖ ≌ C where
functor.obj X := X.unop.unop
functor.map f := f.unop.unop
inverse.obj X := .op (.op X)
inverse.map f := f.op.op
unitIso := Iso.refl _
counitIso := Iso.refl _