Opposite precategories
Content created by Fredrik Bakke, Fernando Chu and Egbert Rijke.
Created on 2023-05-08.
Last modified on 2023-09-27.
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-set-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
Recent changes
- 2023-09-27. Fredrik Bakke. Presheaf categories (#801).
- 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).
- 2023-05-08. Fernando Chu and Fernando Chu. Opposite precategory (#607).