The Essential Image of Functor (#842)

* a bit

* fully-faithfulness

* more

* done

* comment

* everything

* fix

* a bit

* natIso is path

* done

* presheaf is univalent

* a bit

* more

* more

* done

* done

* supplement

* modify

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 PropTrunc
+
+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) = PropTrunc.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/Properties.agda

@@ -240,8 +240,8 @@ module _
 
   -- Fully-faithful functor between univalent target induces embedding on objects
 
-  isFullyFaithful→isEmbb-ob : isFullyFaithful F → isEmbedding (F .F-ob)
-  isFullyFaithful→isEmbb-ob fullfaith x y =
+  isFullyFaithful→isEmbd-ob : isFullyFaithful F → isEmbedding (F .F-ob)
+  isFullyFaithful→isEmbd-ob fullfaith x y =
     isEquiv[equivFunA≃B∘f]→isEquiv[f] _ (_ , isUnivD .univ _ _)
       (subst isEquiv (F-pathToIso-∘ {F = F})
       (compEquiv (_ , isUnivC .univ _ _)

Cubical/Categories/RezkCompletion/Base.agda

@@ -29,7 +29,6 @@ private
 -- because the universal property is naturally universal polymorphic,
 -- and so the predicate is not inside any universe of finite level.
 
-
 isRezkCompletion : (F : Functor C D) → Typeω
 isRezkCompletion {D = D} F =
       isUnivalent D

Cubical/Foundations/Prelude.agda

@@ -321,15 +321,15 @@ module _ (P : ∀ y → x ≡ y → Type ℓ') (d : P x refl) where
 -- Multi-variable versions of J
 
 module _ {x : A}
-  {P : (y : A) → x ≡ y → Type ℓ'}{d : (y : A)(p : x ≡ y) → P y p}
-  (Q : (y : A)(p : x ≡ y)(z : P y p) → d y p ≡ z → Type ℓ'')
+  {P : (y : A) → x ≡ y → Type ℓ'} {d : (y : A) (p : x ≡ y) → P y p}
+  (Q : (y : A) (p : x ≡ y) (z : P y p) → d y p ≡ z → Type ℓ'')
   (r : Q _ refl _ refl) where
 
   private
     ΠQ : (y : A) → x ≡ y → _
     ΠQ y p = ∀ z q → Q y p z q
 
-  J2 : {y : A}(p : x ≡ y){z : P y p}(q : d y p ≡ z) → Q _ p _ q
+  J2 : {y : A} (p : x ≡ y) {z : P y p} (q : d y p ≡ z) → Q _ p _ q
   J2 p = J ΠQ (λ _ → J (Q x refl) r) p _
 
   J2Refl : J2 refl refl ≡ r