instIsEquivalenceOppositeOpFunctor

English

The opposite construction on RelCat yields an equivalence of categories; i.e., RelCat is equivalent to its opposite via the op-functor.

Русский

Противоположная конструкция на RelCat образует эквивалентность категорий; то есть RelCat эквивалентна своей противоположной категорией через граф-функтор противоположного.

LaTeX

$$$ \text{opFunctor.IsEquivalence} \quad \text{for RelCat}. $$$

Lean4

instance : opFunctor.IsEquivalence := by
  change opEquivalence.functor.IsEquivalence
  infer_instance

Похожие утверждения