Essential fibers of functors between precategories

Content created by Fredrik Bakke.

Created on 2023-11-01.
Last modified on 2023-11-09.

module category-theory.essential-fibers-of-functors-precategories where
open import category-theory.functors-precategories
open import category-theory.isomorphisms-in-precategories
open import category-theory.precategories

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


Given a functor F : C → D between precategories and an object y : D we can form the essential fiber of y over F as the subprecategory of C spanned by... TODO


The essential fiber over an object

module _
  {l1 l2 l3 l4 : Level}
  (C : Precategory l1 l2) (D : Precategory l3 l4)
  (F : functor-Precategory C D)

  essential-fiber-functor-Precategory : (y : obj-Precategory D)  UU (l1  l4)
  essential-fiber-functor-Precategory y =
    Σ ( obj-Precategory C)
      ( λ x  iso-Precategory D (obj-functor-Precategory C D F x) y)

  essential-fiber-functor-Precategory' : (y : obj-Precategory D)  UU (l1  l4)
  essential-fiber-functor-Precategory' y =
    Σ ( obj-Precategory C)
      ( λ x  iso-Precategory D y (obj-functor-Precategory C D F x))

See also

Recent changes