Opposite precategories

module category-theory.opposite-precategories where

Imports

open import category-theory.precategories

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

Idea

Let C be a precategory, its opposite precategory Cᵒᵖ is given by reversing every morphism.

Definition

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  where

  opposite-Precategory : Precategory l1 l2
  pr1 opposite-Precategory = obj-Precategory C
  pr1 (pr2 opposite-Precategory) x y = hom-Precategory C y x
  pr1 (pr1 (pr2 (pr2 opposite-Precategory))) f g = comp-hom-Precategory C g f
  pr2 (pr1 (pr2 (pr2 opposite-Precategory))) f g h =
    inv (associative-comp-hom-Precategory C h g f)
  pr1 (pr2 (pr2 (pr2 opposite-Precategory))) x = id-hom-Precategory C {x}
  pr1 (pr2 (pr2 (pr2 (pr2 opposite-Precategory)))) f =
    right-unit-law-comp-hom-Precategory C f
  pr2 (pr2 (pr2 (pr2 (pr2 opposite-Precategory)))) f =
    left-unit-law-comp-hom-Precategory C f