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
Imports 
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

Idea

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

Definitions

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)
  where

  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