This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Essentially injective functors between precategories

module category-theory.essentially-injective-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

A functor F : C → D between precategories is essentially injective if every pair of objects that are mapped to isomorphic objects in D are isomorphic in C.

Definitions

The type of proofs of being essentially injective

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

  is-essentially-injective-functor-Precategory : UU (l1 ⊔ l2 ⊔ l4)
  is-essentially-injective-functor-Precategory =
    (x y : obj-Precategory C) →
    iso-Precategory D
      ( obj-functor-Precategory C D F x)
      ( obj-functor-Precategory C D F y) →
    iso-Precategory C x y

The type of essentially injective functors

essentially-injective-functor-Precategory :
  {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
essentially-injective-functor-Precategory C D =
  Σ ( functor-Precategory C D)
    ( is-essentially-injective-functor-Precategory C D)

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

  functor-essentially-injective-functor-Precategory :
    functor-Precategory C D
  functor-essentially-injective-functor-Precategory = pr1 F

  is-essentially-injective-essentially-injective-functor-Precategory :
    is-essentially-injective-functor-Precategory C D
      ( functor-essentially-injective-functor-Precategory)
  is-essentially-injective-essentially-injective-functor-Precategory = pr2 F

  obj-essentially-injective-functor-Precategory :
    obj-Precategory C → obj-Precategory D
  obj-essentially-injective-functor-Precategory =
    obj-functor-Precategory C D
      ( functor-essentially-injective-functor-Precategory)

  hom-essentially-injective-functor-Precategory :
    {x y : obj-Precategory C} →
    hom-Precategory C x y →
    hom-Precategory D
      ( obj-essentially-injective-functor-Precategory x)
      ( obj-essentially-injective-functor-Precategory y)
  hom-essentially-injective-functor-Precategory =
    hom-functor-Precategory C D
      ( functor-essentially-injective-functor-Precategory)

See also