Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

The Essential Image of Functor #842

Merged
merged 23 commits into from
Aug 12, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
67 changes: 67 additions & 0 deletions Cubical/Categories/Constructions/EssentialImage.agda
Original file line number Diff line number Diff line change
@@ -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
mortberg marked this conversation as resolved.
Show resolved Hide resolved


isUnivalentEssentialImage : isUnivalent D → isUnivalent EssentialImage
isUnivalentEssentialImage = isUnivalentFullSub _ isPropIsInEssentialImage
65 changes: 65 additions & 0 deletions Cubical/Categories/Constructions/FullSubcategory.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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))
2 changes: 1 addition & 1 deletion Cubical/Categories/Equivalence/WeakEquivalence.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions Cubical/Categories/Functor/Properties.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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 _ _)
Expand Down
1 change: 0 additions & 1 deletion Cubical/Categories/RezkCompletion/Base.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions Cubical/Foundations/Prelude.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down