The Essential Image of Functor

Cubical/Categories/Category/Base.agda

@@ -120,8 +120,7 @@ record isUnivalent (C : Category ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
 
   -- The function extracting paths from category-theoretic isomorphisms.
   CatIsoToPath : {x y : C .ob} (p : CatIso _ x y) → x ≡ y
-  CatIsoToPath {x = x} {y = y} p =
-    equivFun (invEquiv (univEquiv x y)) p
+  CatIsoToPath = invEq (univEquiv _ _)
 
   isGroupoid-ob : isGroupoid (C .ob)
   isGroupoid-ob = isOfHLevelPath'⁻ 2 (λ _ _ → isOfHLevelRespectEquiv 2 (invEquiv (univEquiv _ _)) (isSet-CatIso _ _))

Cubical/Categories/Constructions/EssentialImage.agda

@@ -0,0 +1,67 @@
+{-
+
+The Essential Image of Functor
+
+-}
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Constructions.EssentialImage where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Sigma
+open import Cubical.HITs.PropositionalTruncation as Prop
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Constructions.FullSubcategory
+
+private
+  variable
+    ℓC ℓC' ℓD ℓD' : Level
+
+
+module _
+  {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}
+  (F : Functor C D) where
+
+  open Category
+  open Functor
+
+
+  isInEssentialImage : D .ob → Type(ℓ-max ℓC ℓD')
+  isInEssentialImage d = ∃[ c ∈ C .ob ] CatIso D (F .F-ob c) d
+
+  isPropIsInEssentialImage : (d : D .ob) → isProp (isInEssentialImage d)
+  isPropIsInEssentialImage _ = squash₁
+
+
+  -- The Essential Image
+  EssentialImage : Category (ℓ-max ℓC (ℓ-max ℓD ℓD')) ℓD'
+  EssentialImage = FullSubcategory D isInEssentialImage
+
+
+  ToEssentialImage : Functor C EssentialImage
+  ToEssentialImage .F-ob c = F .F-ob c , ∣ c , idCatIso ∣₁
+  ToEssentialImage .F-hom = F .F-hom
+  ToEssentialImage .F-id = F .F-id
+  ToEssentialImage .F-seq = F .F-seq
+
+  FromEssentialImage : Functor EssentialImage D
+  FromEssentialImage = FullInclusion D isInEssentialImage
+
+  CompEssentialImage : funcComp FromEssentialImage ToEssentialImage ≡ F
+  CompEssentialImage = Functor≡ (λ _ → refl) (λ _ → refl)
+
+
+  isEssentiallySurjToEssentialImage : isEssentiallySurj ToEssentialImage
+  isEssentiallySurjToEssentialImage (d , p) = Prop.map (λ (c , f) → c , Incl-Iso-inv _ _ _ _ f) p
+
+  isFullyFaithfulFromEssentialImage : isFullyFaithful FromEssentialImage
+  isFullyFaithfulFromEssentialImage = isFullyFaithfulIncl D isInEssentialImage
+
+
+  isFullyFaithfulToEssentialImage : isFullyFaithful F → isFullyFaithful ToEssentialImage
+  isFullyFaithfulToEssentialImage fullfaith = fullfaith
+
+
+  isUnivalentEssentialImage : isUnivalent D → isUnivalent EssentialImage
+  isUnivalentEssentialImage = isUnivalentFullSub _ isPropIsInEssentialImage

Cubical/Categories/Constructions/FullSubcategory.agda

@@ -4,8 +4,15 @@ module Cubical.Categories.Constructions.FullSubcategory where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.Properties
+open import Cubical.Foundations.Isomorphism
+
+open import Cubical.Functions.Embedding
+open import Cubical.Data.Sigma
 
 open import Cubical.Categories.Category
+open import Cubical.Categories.Isomorphism
 open import Cubical.Categories.Functor renaming (𝟙⟨_⟩ to funcId)
 
 private
@@ -34,6 +41,37 @@ module _ (C : Category ℓC ℓC') (P : Category.ob C → Type ℓP) where
   F-id FullInclusion = refl
   F-seq FullInclusion f g = refl
 
+  isFullyFaithfulIncl : isFullyFaithful FullInclusion
+  isFullyFaithfulIncl _ _ = idEquiv _ .snd
+
+  module _ (x y : FullSubcategory .ob) where
+
+    open isIso
+
+    Incl-Iso = F-Iso {F = FullInclusion} {x = x} {y = y}
+
+    Incl-Iso-inv : CatIso C (x .fst) (y .fst) → CatIso FullSubcategory x y
+    Incl-Iso-inv f .fst = f .fst
+    Incl-Iso-inv f .snd .inv = f .snd .inv
+    Incl-Iso-inv f .snd .sec = f .snd .sec
+    Incl-Iso-inv f .snd .ret = f .snd .ret
+
+    Incl-Iso-sec : ∀ f → Incl-Iso (Incl-Iso-inv f) ≡ f
+    Incl-Iso-sec f = CatIso≡ _ _ refl
+
+    Incl-Iso-ret : ∀ f → Incl-Iso-inv (Incl-Iso f) ≡ f
+    Incl-Iso-ret f = CatIso≡ _ _ refl
+
+    Incl-Iso-Iso : Iso (CatIso FullSubcategory x y) (CatIso C (x .fst) (y .fst))
+    Incl-Iso-Iso = iso Incl-Iso Incl-Iso-inv Incl-Iso-sec Incl-Iso-ret
+
+    Incl-Iso≃ : CatIso FullSubcategory x y ≃ CatIso C (x .fst) (y .fst)
+    Incl-Iso≃ = isoToEquiv Incl-Iso-Iso
+
+    isEquivIncl-Iso : isEquiv Incl-Iso
+    isEquivIncl-Iso = Incl-Iso≃ .snd
+
+
 module _ (C : Category ℓC ℓC')
          (D : Category ℓD ℓD') (Q : Category.ob D → Type ℓQ) where
   private
@@ -94,3 +132,30 @@ module _ (C : Category ℓC ℓC') (P : Category.ob C → Type ℓP)
   MapFullSubcategory-seq F f G g = Functor≡
     (λ (c , p) → refl)
     (λ γ → refl)
+
+
+-- Full subcategory (injective on objects)
+
+open Category
+
+module _
+  (C : Category ℓC ℓC')
+  {P : C .ob → Type ℓP}(isPropP : (c : C .ob) → isProp (P c))
+  where
+
+  open Functor
+  open isUnivalent
+
+
+  -- Full subcategory (injective on objects) is injective on objects.
+
+  isEmbdIncl-ob : isEmbedding (FullInclusion C P .F-ob)
+  isEmbdIncl-ob _ _ = isEmbeddingFstΣProp isPropP
+
+
+  -- Full subcategory (injective on objects) of univalent category is univalent.
+
+  isUnivalentFullSub : isUnivalent C → isUnivalent (FullSubcategory C P)
+  isUnivalentFullSub isUnivC .univ _ _ = isEquiv[equivFunA≃B∘f]→isEquiv[f] _ (Incl-Iso≃ C P _ _)
+    (subst isEquiv (sym (F-pathToIso-∘ {F = FullInclusion C P}))
+      (compEquiv (_ , isEmbdIncl-ob _ _) (_ , isUnivC .univ _ _) .snd))

Cubical/Categories/Equivalence/WeakEquivalence.agda

@@ -65,7 +65,7 @@ module _
 
   isEquivF-ob : {F : Functor C D} → isWeakEquivalence F → isEquivMap (F .F-ob)
   isEquivF-ob {F = F} is-w-equiv = isEmbedding×isSurjection→isEquiv
-    (isFullyFaithful→isEmbb-ob isUnivC isUnivD {F = F} (is-w-equiv .fullfaith) ,
+    (isFullyFaithful→isEmbd-ob isUnivC isUnivD {F = F} (is-w-equiv .fullfaith) ,
      isSurj→isSurj-ob isUnivD {F = F} (is-w-equiv .esssurj))
 
   isWeakEquiv→isEquiv : {F : Functor C D} → isWeakEquivalence F → isEquivalence F

Cubical/Categories/Functor/Base.agda

@@ -3,6 +3,7 @@ module Cubical.Categories.Functor.Base where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.HLevels
 
 open import Cubical.Data.Sigma
 
@@ -63,6 +64,29 @@ F-id (Functor≡ {C = C} {D = D} {F = F} {G = G} hOb hHom i) =
 F-seq (Functor≡ {C = C} {D = D} {F = F} {G = G} hOb hHom i) f g =
   isProp→PathP (λ j → isSetHom D (hHom (f ⋆⟨ C ⟩ g) j) ((hHom f j) ⋆⟨ D ⟩ (hHom g j))) (F-seq F f g) (F-seq G f g) i
 
+FunctorSquare :
+  {F₀₀ F₀₁ F₁₀ F₁₁ : Functor C D}
+  (F₀₋ : F₀₀ ≡ F₀₁) (F₁₋ : F₁₀ ≡ F₁₁)
+  (F₋₀ : F₀₀ ≡ F₁₀) (F₋₁ : F₀₁ ≡ F₁₁)
+  → Square (cong F-ob F₀₋) (cong F-ob F₁₋) (cong F-ob F₋₀) (cong F-ob F₋₁)
+  → Square F₀₋ F₁₋ F₋₀ F₋₁
+FunctorSquare {C = C} {D = D} F₀₋ F₁₋ F₋₀ F₋₁ r = sqr
+  where
+  sqr : _
+  sqr i j .F-ob = r i j
+  sqr i j .F-hom {x = x} {y = y} f =
+    isSet→SquareP (λ i j → D .isSetHom {x = sqr i j .F-ob x} {y = sqr i j .F-ob y})
+    (λ i → F₀₋ i .F-hom f) (λ i → F₁₋ i .F-hom f) (λ i → F₋₀ i .F-hom f) (λ i → F₋₁ i .F-hom f) i j
+  sqr i j .F-id {x = x} =
+    isSet→SquareP (λ i j → isProp→isSet (D .isSetHom (sqr i j .F-hom (C .id)) (D .id)))
+    (λ i → F₀₋ i .F-id) (λ i → F₁₋ i .F-id) (λ i → F₋₀ i .F-id) (λ i → F₋₁ i .F-id) i j
+  sqr i j .F-seq f g =
+    isSet→SquareP (λ i j →
+      isProp→isSet (D .isSetHom (sqr i j .F-hom (f ⋆⟨ C ⟩ g)) ((sqr i j .F-hom f) ⋆⟨ D ⟩ (sqr i j .F-hom g))))
+    (λ i → F₀₋ i .F-seq f g) (λ i → F₁₋ i .F-seq f g) (λ i → F₋₀ i .F-seq f g) (λ i → F₋₁ i .F-seq f g) i j
+
+FunctorPath≡ : {F G : Functor C D}{p q : F ≡ G} → cong F-ob p ≡ cong F-ob q → p ≡ q
+FunctorPath≡ {p = p} {q = q} = FunctorSquare p q refl refl
 
 
 -- Helpful notation