Coslice precategories

Content created by Fernando Chu, Egbert Rijke and Fredrik Bakke.

Created on 2024-08-05.
Last modified on 2024-08-29.

module category-theory.coslice-precategories where
Imports 
open import category-theory.functors-precategories
open import category-theory.opposite-precategories
open import category-theory.precategories
open import category-theory.slice-precategories

open import foundation.universe-levels

Idea

The coslice precategory of a precategory C under an object X of C is the category of objects of C equipped with a morphism from X.

Equivalently, it is the opposite of the slice precategory of Cᵒᵖ.

Definitions

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

  Coslice-Precategory : Precategory (l1 ⊔ l2) l2
  Coslice-Precategory =
    opposite-Precategory (Slice-Precategory (opposite-Precategory C) X)

Properties

The coslice precategory has a forgetful functor

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

  forgetful-functor-Coslice-Precategory :
    functor-Precategory (Coslice-Precategory C X) C
  forgetful-functor-Coslice-Precategory =
    opposite-functor-Precategory
      ( Slice-Precategory (opposite-Precategory C) X)
      ( opposite-Precategory C)
      ( forgetful-functor-Slice-Precategory (opposite-Precategory C) X)

Recent changes