From b357f48881f64150cc5b4332574ad1a82208aa06 Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Fri, 3 Jun 2022 01:50:55 +0800 Subject: [PATCH 01/18] a bit --- .../Categories/Constructions/BinProduct.agda | 18 +++- .../Categories/Equivalence/Isomorphism.agda | 92 +++++++++++++++++ Cubical/Categories/Isomorphism.agda | 98 +++++++++++++++++++ 3 files changed, 205 insertions(+), 3 deletions(-) create mode 100644 Cubical/Categories/Equivalence/Isomorphism.agda create mode 100644 Cubical/Categories/Isomorphism.agda diff --git a/Cubical/Categories/Constructions/BinProduct.agda b/Cubical/Categories/Constructions/BinProduct.agda index c6498dc2d3..5d3658b45e 100644 --- a/Cubical/Categories/Constructions/BinProduct.agda +++ b/Cubical/Categories/Constructions/BinProduct.agda @@ -3,11 +3,12 @@ module Cubical.Categories.Constructions.BinProduct where -open import Cubical.Categories.Category.Base -open import Cubical.Categories.Functor.Base -open import Cubical.Data.Sigma renaming (_×_ to _×'_) open import Cubical.Foundations.HLevels open import Cubical.Foundations.Prelude +open import Cubical.Data.Sigma renaming (_×_ to _×'_) +open import Cubical.Categories.Category.Base +open import Cubical.Categories.Functor.Base +open import Cubical.Categories.Isomorphism private variable @@ -62,3 +63,14 @@ module _ (C : Category ℓC ℓC') - define inverse to `assoc`, prove isomorphism - prove product is commutative up to isomorphism -} + + + -- The isomorphisms in product category + + open CatIso + + iso× : {x y : C .ob}{z w : D .ob} → CatIso C x y → CatIso D z w → CatIso (C × D) (x , z) (y , w) + iso× f g .mor = f .mor , g .mor + iso× f g .inv = f .inv , g .inv + iso× f g .sec i = f .sec i , g .sec i + iso× f g .ret i = f .ret i , g .ret i diff --git a/Cubical/Categories/Equivalence/Isomorphism.agda b/Cubical/Categories/Equivalence/Isomorphism.agda new file mode 100644 index 0000000000..789c1dba1f --- /dev/null +++ b/Cubical/Categories/Equivalence/Isomorphism.agda @@ -0,0 +1,92 @@ +{-# OPTIONS --safe #-} + +module Cubical.Categories.Equivalence.Isomorphism where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Sigma +open import Cubical.Categories.Category +open import Cubical.Categories.Functor +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Morphism +open import Cubical.Categories.Equivalence.Base +open import Cubical.HITs.PropositionalTruncation.Base + +open Category +open Functor +open NatIso +open CatIso +open NatTrans +open isEquivalence + +private + variable + ℓC ℓC' ℓD ℓD' : Level + +-- Equivalence implies Full, Faithul, and Essentially Surjective + +module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where + symEquiv : ∀ {F : Functor C D} → (e : isEquivalence F) → isEquivalence (e .invFunc) + symEquiv {F} record { invFunc = G ; η = η ; ε = ε } = record { invFunc = F ; η = symNatIso ε ; ε = symNatIso η } + + isEquiv→Faithful : ∀ {F : Functor C D} → isEquivalence F → isFaithful F + isEquiv→Faithful {F} record { invFunc = G + ; η = η + ; ε = _ } + c c' f g p = f + ≡⟨ sqRL η ⟩ + cIso .mor ⋆⟨ C ⟩ G ⟪ F ⟪ f ⟫ ⟫ ⋆⟨ C ⟩ c'Iso .inv + ≡⟨ cong (λ v → cIso .mor ⋆⟨ C ⟩ (G ⟪ v ⟫) ⋆⟨ C ⟩ c'Iso .inv) p ⟩ + cIso .mor ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⟫ ⋆⟨ C ⟩ c'Iso .inv + ≡⟨ sym (sqRL η) ⟩ + g + ∎ + where + + -- isomorphism between c and GFc + cIso = isIso→CatIso (η .nIso c) + -- isomorphism between c' and GFc' + c'Iso = isIso→CatIso (η .nIso c') + +module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where + isEquiv→Full : ∀ {F : Functor C D} → isEquivalence F → isFull F + isEquiv→Full {F} eq@record { invFunc = G + ; η = η + ; ε = _ } + c c' g = ∣ h , isEquiv→Faithful (symEquiv eq) _ _ _ _ GFh≡Gg ∣₁ -- apply faithfulness of G + where + -- isomorphism between c and GFc + cIso = isIso→CatIso (η .nIso c) + -- isomorphism between c' and GFc' + c'Iso = isIso→CatIso (η .nIso c') + + -- reverses + cIso⁻ = symCatIso cIso + c'Iso⁻ = symCatIso c'Iso + + h = cIso .mor ⋆⟨ C ⟩ G ⟪ g ⟫ ⋆⟨ C ⟩ c'Iso .inv + + -- we show that both `G ⟪ g ⟫` and `G ⟪ F ⟪ h ⟫ ⟫` + -- are equal to the same thing + -- namely : cIso .inv ⋆⟨ C ⟩ h ⋆⟨ C ⟩ c'Iso .mor + Gg≡ηhη : G ⟪ g ⟫ ≡ cIso .inv ⋆⟨ C ⟩ h ⋆⟨ C ⟩ c'Iso .mor + Gg≡ηhη = invMoveL cAreInv move-c' ∙ sym (C .⋆Assoc _ _ _) + where + cAreInv : areInv _ (cIso .mor) (cIso .inv) + cAreInv = CatIso→areInv cIso + + c'AreInv : areInv _ (c'Iso .mor) (c'Iso .inv) + c'AreInv = CatIso→areInv c'Iso + + move-c' : cIso .mor ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ h ⋆⟨ C ⟩ c'Iso .mor + move-c' = invMoveR (symAreInv c'AreInv) refl + + GFh≡Gg : G ⟪ F ⟪ h ⟫ ⟫ ≡ G ⟪ g ⟫ + GFh≡Gg = G ⟪ F ⟪ h ⟫ ⟫ + ≡⟨ sqLR η ⟩ + cIso .inv ⋆⟨ C ⟩ h ⋆⟨ C ⟩ c'Iso .mor + ≡⟨ sym Gg≡ηhη ⟩ + G ⟪ g ⟫ + ∎ + + isEquiv→Surj : ∀ {F : Functor C D} → isEquivalence F → isEssentiallySurj F + isEquiv→Surj isE d = (isE .invFunc ⟅ d ⟆) , isIso→CatIso ((isE .ε .nIso) d) diff --git a/Cubical/Categories/Isomorphism.agda b/Cubical/Categories/Isomorphism.agda new file mode 100644 index 0000000000..3af5ef285a --- /dev/null +++ b/Cubical/Categories/Isomorphism.agda @@ -0,0 +1,98 @@ +{-# OPTIONS --safe #-} +module Cubical.Categories.Isomorphism where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.GroupoidLaws +open import Cubical.Categories.Category + renaming (CatIso≡ to CatIso≡Ext) +open import Cubical.Categories.Functor.Base +open import Cubical.Categories.Functor.Properties + +private + variable + ℓC ℓC' ℓD ℓD' : Level + + +module _ {C : Category ℓC ℓC'} where + + open Category C + open CatIso + + + ⋆Iso : {x y z : ob} → (f : CatIso C x y)(g : CatIso C y z) → CatIso C x z + ⋆Iso f g .mor = f .mor ⋆ g .mor + ⋆Iso f g .inv = g .inv ⋆ f .inv + ⋆Iso f g .sec = sym (⋆Assoc _ _ _) + ∙ (λ i → ⋆Assoc (g .inv) (f .inv) (f .mor) i ⋆ g .mor) + ∙ (λ i → (g .inv ⋆ f .sec i) ⋆ g .mor) + ∙ (λ i → ⋆IdR (g .inv) i ⋆ g .mor) + ∙ g .sec + ⋆Iso f g .ret = sym (⋆Assoc _ _ _) + ∙ (λ i → ⋆Assoc (f .mor) (g .mor) (g .inv) i ⋆ f .inv) + ∙ (λ i → (f .mor ⋆ g .ret i) ⋆ f .inv) + ∙ (λ i → ⋆IdR (f .mor) i ⋆ f .inv) + ∙ f .ret + + compIso : {x y z : ob} → (g : CatIso C y z)(f : CatIso C x y) → CatIso C x z + compIso g f = ⋆Iso f g + + + CatIso≡ : {x y : ob} (f g : CatIso C x y) → f .mor ≡ g .mor → f ≡ g + CatIso≡ f g p = CatIso≡Ext f g p inv≡ + where + inv≡ : f .inv ≡ g .inv + inv≡ = sym (⋆IdL _) + ∙ (λ i → g .sec (~ i) ⋆ f .inv) + ∙ ⋆Assoc _ _ _ + ∙ (λ i → g .inv ⋆ (p (~ i) ⋆ f .inv)) + ∙ (λ i → g .inv ⋆ f .ret i) + ∙ ⋆IdR _ + + + ⋆IsoIdL : {x y : ob} → (f : CatIso C x y) → ⋆Iso idCatIso f ≡ f + ⋆IsoIdL _ = CatIso≡ _ _ (⋆IdL _) + + ⋆IsoIdR : {x y : ob} → (f : CatIso C x y) → ⋆Iso f idCatIso ≡ f + ⋆IsoIdR _ = CatIso≡ _ _ (⋆IdR _) + + + pathToIso-∙ : {x y z : ob}(p : x ≡ y)(q : y ≡ z) → pathToIso (p ∙ q) ≡ ⋆Iso (pathToIso p) (pathToIso q) + pathToIso-∙ p q = J (λ y p → (z : ob)(q : y ≡ z) → pathToIso (p ∙ q) ≡ ⋆Iso (pathToIso p) (pathToIso q)) + (λ _ q → J (λ z q → pathToIso (refl ∙ q) ≡ ⋆Iso (pathToIso refl) (pathToIso q)) pathToIso-∙-refl q) p _ q + where + pathToIso-∙-refl : {x : ob} → pathToIso {x = x} (refl ∙ refl) ≡ ⋆Iso (pathToIso refl) (pathToIso refl) + pathToIso-∙-refl = cong pathToIso (sym compPathRefl) + ∙ sym (⋆IsoIdL _) + ∙ (λ i → ⋆Iso (pathToIso-refl (~ i)) (pathToIso refl)) + + +module _ {C : Category ℓC ℓC'} where + + open Category + open CatIso + + op-Iso : {x y : C .ob} → CatIso C x y → CatIso (C ^op) x y + op-Iso f .mor = f .inv + op-Iso f .inv = f .mor + op-Iso f .sec = f .sec + op-Iso f .ret = f .ret + + +module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}{F : Functor C D} where + + open Category + open CatIso + open Functor + + + F-Iso : {x y : C .ob} → CatIso C x y → CatIso D (F .F-ob x) (F .F-ob y) + F-Iso f .mor = F . F-hom (f .mor) + F-Iso f .inv = F . F-hom (f .inv) + F-Iso f .sec = sym (F .F-seq (f .inv) (f .mor)) ∙ cong (F .F-hom) (f .sec) ∙ F .F-id + F-Iso f .ret = sym (F .F-seq (f .mor) (f .inv)) ∙ cong (F .F-hom) (f .ret) ∙ F .F-id + + F-Iso-PresId : {x : C .ob} → F-Iso (idCatIso {x = x}) ≡ idCatIso + F-Iso-PresId = CatIso≡ _ _ (F .F-id) + + F-Iso-Pres⋆ : {x y z : C .ob} → (f : CatIso C x y)(g : CatIso C y z) → F-Iso (⋆Iso f g) ≡ ⋆Iso (F-Iso f) (F-Iso g) + F-Iso-Pres⋆ _ _ = CatIso≡ _ _ (F .F-seq _ _) From 98edcd964c1b124e2b9f71c3a069c40c813cec99 Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Fri, 3 Jun 2022 02:52:51 +0800 Subject: [PATCH 02/18] fully-faithfulness --- Cubical/Categories/Equivalence/Base.agda | 1 - .../Categories/Equivalence/Isomorphism.agda | 92 ------------------- .../Equivalence/WeakEquivalence.agda | 73 +++++++++++++++ Cubical/Categories/Functor/Base.agda | 6 ++ Cubical/Categories/Functor/Properties.agda | 18 ++++ Cubical/Functions/Embedding.agda | 9 ++ 6 files changed, 106 insertions(+), 93 deletions(-) delete mode 100644 Cubical/Categories/Equivalence/Isomorphism.agda create mode 100644 Cubical/Categories/Equivalence/WeakEquivalence.agda diff --git a/Cubical/Categories/Equivalence/Base.agda b/Cubical/Categories/Equivalence/Base.agda index e5d8255aa8..fdfe4eb58e 100644 --- a/Cubical/Categories/Equivalence/Base.agda +++ b/Cubical/Categories/Equivalence/Base.agda @@ -27,4 +27,3 @@ record _≃ᶜ_ (C : Category ℓC ℓC') (D : Category ℓD ℓD') : field func : Functor C D isEquiv : isEquivalence func - diff --git a/Cubical/Categories/Equivalence/Isomorphism.agda b/Cubical/Categories/Equivalence/Isomorphism.agda deleted file mode 100644 index 789c1dba1f..0000000000 --- a/Cubical/Categories/Equivalence/Isomorphism.agda +++ /dev/null @@ -1,92 +0,0 @@ -{-# OPTIONS --safe #-} - -module Cubical.Categories.Equivalence.Isomorphism where - -open import Cubical.Foundations.Prelude -open import Cubical.Data.Sigma -open import Cubical.Categories.Category -open import Cubical.Categories.Functor -open import Cubical.Categories.NaturalTransformation -open import Cubical.Categories.Morphism -open import Cubical.Categories.Equivalence.Base -open import Cubical.HITs.PropositionalTruncation.Base - -open Category -open Functor -open NatIso -open CatIso -open NatTrans -open isEquivalence - -private - variable - ℓC ℓC' ℓD ℓD' : Level - --- Equivalence implies Full, Faithul, and Essentially Surjective - -module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where - symEquiv : ∀ {F : Functor C D} → (e : isEquivalence F) → isEquivalence (e .invFunc) - symEquiv {F} record { invFunc = G ; η = η ; ε = ε } = record { invFunc = F ; η = symNatIso ε ; ε = symNatIso η } - - isEquiv→Faithful : ∀ {F : Functor C D} → isEquivalence F → isFaithful F - isEquiv→Faithful {F} record { invFunc = G - ; η = η - ; ε = _ } - c c' f g p = f - ≡⟨ sqRL η ⟩ - cIso .mor ⋆⟨ C ⟩ G ⟪ F ⟪ f ⟫ ⟫ ⋆⟨ C ⟩ c'Iso .inv - ≡⟨ cong (λ v → cIso .mor ⋆⟨ C ⟩ (G ⟪ v ⟫) ⋆⟨ C ⟩ c'Iso .inv) p ⟩ - cIso .mor ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⟫ ⋆⟨ C ⟩ c'Iso .inv - ≡⟨ sym (sqRL η) ⟩ - g - ∎ - where - - -- isomorphism between c and GFc - cIso = isIso→CatIso (η .nIso c) - -- isomorphism between c' and GFc' - c'Iso = isIso→CatIso (η .nIso c') - -module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where - isEquiv→Full : ∀ {F : Functor C D} → isEquivalence F → isFull F - isEquiv→Full {F} eq@record { invFunc = G - ; η = η - ; ε = _ } - c c' g = ∣ h , isEquiv→Faithful (symEquiv eq) _ _ _ _ GFh≡Gg ∣₁ -- apply faithfulness of G - where - -- isomorphism between c and GFc - cIso = isIso→CatIso (η .nIso c) - -- isomorphism between c' and GFc' - c'Iso = isIso→CatIso (η .nIso c') - - -- reverses - cIso⁻ = symCatIso cIso - c'Iso⁻ = symCatIso c'Iso - - h = cIso .mor ⋆⟨ C ⟩ G ⟪ g ⟫ ⋆⟨ C ⟩ c'Iso .inv - - -- we show that both `G ⟪ g ⟫` and `G ⟪ F ⟪ h ⟫ ⟫` - -- are equal to the same thing - -- namely : cIso .inv ⋆⟨ C ⟩ h ⋆⟨ C ⟩ c'Iso .mor - Gg≡ηhη : G ⟪ g ⟫ ≡ cIso .inv ⋆⟨ C ⟩ h ⋆⟨ C ⟩ c'Iso .mor - Gg≡ηhη = invMoveL cAreInv move-c' ∙ sym (C .⋆Assoc _ _ _) - where - cAreInv : areInv _ (cIso .mor) (cIso .inv) - cAreInv = CatIso→areInv cIso - - c'AreInv : areInv _ (c'Iso .mor) (c'Iso .inv) - c'AreInv = CatIso→areInv c'Iso - - move-c' : cIso .mor ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ h ⋆⟨ C ⟩ c'Iso .mor - move-c' = invMoveR (symAreInv c'AreInv) refl - - GFh≡Gg : G ⟪ F ⟪ h ⟫ ⟫ ≡ G ⟪ g ⟫ - GFh≡Gg = G ⟪ F ⟪ h ⟫ ⟫ - ≡⟨ sqLR η ⟩ - cIso .inv ⋆⟨ C ⟩ h ⋆⟨ C ⟩ c'Iso .mor - ≡⟨ sym Gg≡ηhη ⟩ - G ⟪ g ⟫ - ∎ - - isEquiv→Surj : ∀ {F : Functor C D} → isEquivalence F → isEssentiallySurj F - isEquiv→Surj isE d = (isE .invFunc ⟅ d ⟆) , isIso→CatIso ((isE .ε .nIso) d) diff --git a/Cubical/Categories/Equivalence/WeakEquivalence.agda b/Cubical/Categories/Equivalence/WeakEquivalence.agda new file mode 100644 index 0000000000..f40a8a2006 --- /dev/null +++ b/Cubical/Categories/Equivalence/WeakEquivalence.agda @@ -0,0 +1,73 @@ +{-# OPTIONS --safe #-} + +module Cubical.Categories.Equivalence.WeakEquivalence where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv + renaming (isEquiv to isEquivMap) +open import Cubical.Data.Sigma +open import Cubical.Categories.Category +open import Cubical.Categories.Functor +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Morphism +open import Cubical.Categories.Equivalence +open import Cubical.HITs.PropositionalTruncation.Base + +open Category +open Functor +open NatIso +open CatIso +open NatTrans +open isEquivalence +open _≃ᶜ_ + +private + variable + ℓC ℓC' ℓD ℓD' : Level + C : Category ℓC ℓC' + D : Category ℓD ℓD' + F : Functor C D + + +record isWeakEquivalence {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} + (func : Functor C D) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where + field + + full : isFull func + faith : isFaithful func + surj : isEssentiallySurj func + +record WeakEquivalence (C : Category ℓC ℓC') (D : Category ℓD ℓD') + : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where + field + + func : Functor C D + isWeakEquiv : isWeakEquivalence func + + +open isWeakEquivalence +open WeakEquivalence + + +isEquiv→isWeakEquiv : isEquivalence F → isWeakEquivalence F +isEquiv→isWeakEquiv isequiv .full = isEquiv→Full isequiv +isEquiv→isWeakEquiv isequiv .faith = isEquiv→Faithful isequiv +isEquiv→isWeakEquiv isequiv .surj = isEquiv→Surj isequiv + + +module _ + {C : Category ℓC ℓC'}(isUnivC : isUnivalent C) + {D : Category ℓD ℓD'}(isUnivD : isUnivalent D) + where + + open isUnivalent + + + module _ {F : WeakEquivalence C D} where + + isEquivF-ob : isEquivMap (F .func .F-ob) + isEquivF-ob = {!!} + + + isWeakEquiv→isEquiv : isWeakEquivalence F → isEquivalence F + isWeakEquiv→isEquiv is-w-equiv = {!!} diff --git a/Cubical/Categories/Functor/Base.agda b/Cubical/Categories/Functor/Base.agda index 781a67d496..c5c5441220 100644 --- a/Cubical/Categories/Functor/Base.agda +++ b/Cubical/Categories/Functor/Base.agda @@ -2,6 +2,7 @@ module Cubical.Categories.Functor.Base where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv open import Cubical.Data.Sigma @@ -26,6 +27,7 @@ record Functor (C : Category ℓC ℓC') (D : Category ℓD ℓD') : isFull = (x y : _) (F[f] : D [ F-ob x , F-ob y ]) → ∃[ f ∈ C [ x , y ] ] F-hom f ≡ F[f] isFaithful = (x y : _) (f g : C [ x , y ]) → F-hom f ≡ F-hom g → f ≡ g + isFullyFaithful = (x y : _) → isEquiv (F-hom {x = x} {y = y}) isEssentiallySurj = (d : D .ob) → Σ[ c ∈ C .ob ] CatIso D (F-ob c) d -- preservation of commuting squares and triangles @@ -89,6 +91,10 @@ _⟪_⟫ = F-hom 𝟙⟨ C ⟩ .F-id = refl 𝟙⟨ C ⟩ .F-seq _ _ = refl +Id : {C : Category ℓ ℓ'} → Functor C C +Id = 𝟙⟨ _ ⟩ + + -- functor composition funcComp : ∀ (G : Functor D E) (F : Functor C D) → Functor C E (funcComp G F) .F-ob c = G ⟅ F ⟅ c ⟆ ⟆ diff --git a/Cubical/Categories/Functor/Properties.agda b/Cubical/Categories/Functor/Properties.agda index 952582435d..2e8f8b2dd3 100644 --- a/Cubical/Categories/Functor/Properties.agda +++ b/Cubical/Categories/Functor/Properties.agda @@ -3,9 +3,13 @@ module Cubical.Categories.Functor.Properties where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Equiv.Properties open import Cubical.Foundations.Function renaming (_∘_ to _◍_) open import Cubical.Foundations.GroupoidLaws using (lUnit; rUnit; assoc; cong-∙) open import Cubical.Foundations.HLevels +open import Cubical.Functions.Surjection +open import Cubical.Functions.Embedding open import Cubical.Categories.Category open import Cubical.Categories.Functor.Base @@ -138,3 +142,17 @@ isSetFunctor {D = D} {C = C} isSet-D-ob F G p q = w (λ i i₁ → isProp→isSet (D .isSetHom (F-hom (w i i₁) _) ((F-hom (w i i₁) _) ⋆⟨ D ⟩ (F-hom (w i i₁) _)))) (λ i₁ → F-seq (p i₁) _ _) (λ i₁ → F-seq (q i₁) _ _) refl refl i i₁ + +-- Fully-faithfulness of functors + +module _ {F : Functor C D} where + + isFullyFaithful→Full : isFullyFaithful F → isFull F + isFullyFaithful→Full fullfaith x y = isEquiv→isSurjection (fullfaith x y) + + isFullyFaithful→Faithful : isFullyFaithful F → isFaithful F + isFullyFaithful→Faithful fullfaith x y = isEmbedding→Inj (isEquiv→isEmbedding (fullfaith x y)) + + isFull+Faithful→isFullyFaithful : isFull F → isFaithful F → isFullyFaithful F + isFull+Faithful→isFullyFaithful full faith x y = isEmbedding×isSurjection→isEquiv + (injEmbedding (C .isSetHom) (D .isSetHom) (faith x y _ _) , full x y) diff --git a/Cubical/Functions/Embedding.agda b/Cubical/Functions/Embedding.agda index dc9357a044..f4758b50eb 100644 --- a/Cubical/Functions/Embedding.agda +++ b/Cubical/Functions/Embedding.agda @@ -47,6 +47,14 @@ isEmbedding f = ∀ w x → isEquiv {A = w ≡ x} (cong f) isPropIsEmbedding : isProp (isEmbedding f) isPropIsEmbedding {f = f} = isPropΠ2 λ _ _ → isPropIsEquiv (cong f) +-- Embedding is injection in the aforementioned sense: +isEmbedding→Inj + : {f : A → B} + → isEmbedding f + → ∀ w x → f w ≡ f x → w ≡ x +isEmbedding→Inj {f = f} embb w x p + = equiv-proof (embb w x) p .fst .fst + -- If A and B are h-sets, then injective functions between -- them are embeddings. -- @@ -66,6 +74,7 @@ injEmbedding {f = f} iSA iSB inj w x retr : retract (cong f) inj retr p = iSA w x _ p + -- If `f` is an embedding, we'd expect the fibers of `f` to be -- propositions, like an injective function. hasPropFibers : (A → B) → Type _ From 263332bead50933df28aea88a52073406d13b5bd Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Fri, 3 Jun 2022 17:53:47 +0800 Subject: [PATCH 03/18] more --- Cubical/Categories/Category/Base.agda | 65 +++++++---- Cubical/Categories/Category/Properties.agda | 9 -- .../Categories/Constructions/BinProduct.agda | 10 +- Cubical/Categories/Constructions/Slice.agda | 42 ++++---- .../Categories/Equivalence/Properties.agda | 73 +++++++++++-- .../Equivalence/WeakEquivalence.agda | 26 ++--- Cubical/Categories/Functor/Base.agda | 2 +- Cubical/Categories/Functor/Properties.agda | 81 +++++++++++++- Cubical/Categories/Instances/CommRings.agda | 23 ++-- Cubical/Categories/Instances/Functors.agda | 4 +- Cubical/Categories/Instances/Sets.agda | 22 ++-- Cubical/Categories/Isomorphism.agda | 102 +++++++++++------- Cubical/Categories/Limits/Initial.agda | 10 +- Cubical/Categories/Limits/Terminal.agda | 10 +- Cubical/Categories/Morphism.agda | 25 ++--- .../NaturalTransformation/Base.agda | 17 ++- .../NaturalTransformation/Properties.agda | 4 +- Cubical/Categories/Presheaf/Properties.agda | 4 +- Cubical/Categories/Yoneda.agda | 3 + Cubical/Data/Sigma/Properties.agda | 10 ++ Cubical/Foundations/Equiv/Properties.agda | 13 +++ 21 files changed, 376 insertions(+), 179 deletions(-) diff --git a/Cubical/Categories/Category/Base.agda b/Cubical/Categories/Category/Base.agda index 417646a622..61cad2fc44 100644 --- a/Cubical/Categories/Category/Base.agda +++ b/Cubical/Categories/Category/Base.agda @@ -5,6 +5,7 @@ open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels open import Cubical.Foundations.Equiv open import Cubical.Foundations.Powerset +open import Cubical.Data.Sigma private variable @@ -51,40 +52,63 @@ comp' = _∘_ infixr 16 comp' syntax comp' C g f = g ∘⟨ C ⟩ f + -- Isomorphisms and paths in categories -record CatIso (C : Category ℓ ℓ') (x y : C .ob) : Type ℓ' where - constructor catiso + +record isIso (C : Category ℓ ℓ'){x y : C .ob}(f : C [ x , y ]) : Type ℓ' where + constructor isiso field - mor : C [ x , y ] inv : C [ y , x ] - sec : inv ⋆⟨ C ⟩ mor ≡ C .id - ret : mor ⋆⟨ C ⟩ inv ≡ C .id + sec : inv ⋆⟨ C ⟩ f ≡ C .id + ret : f ⋆⟨ C ⟩ inv ≡ C .id + +open isIso + +isPropIsIso : {C : Category ℓ ℓ'}{x y : C .ob}(f : C [ x , y ]) → isProp (isIso C f) +isPropIsIso {C = C} f p q i .inv = + (sym (C .⋆IdL _) + ∙ (λ i → q .sec (~ i) ⋆⟨ C ⟩ p .inv) + ∙ C .⋆Assoc _ _ _ + ∙ (λ i → q .inv ⋆⟨ C ⟩ p .ret i) + ∙ C .⋆IdR _) i +isPropIsIso {C = C} f p q i .sec j = + isSet→SquareP (λ i j → C .isSetHom) + (p .sec) (q .sec) (λ i → isPropIsIso {C = C} f p q i .inv ⋆⟨ C ⟩ f) refl i j +isPropIsIso {C = C} f p q i .ret j = + isSet→SquareP (λ i j → C .isSetHom) + (p .ret) (q .ret) (λ i → f ⋆⟨ C ⟩ isPropIsIso {C = C} f p q i .inv) refl i j + + +CatIso : (C : Category ℓ ℓ') (x y : C .ob) → Type ℓ' +CatIso C x y = Σ[ f ∈ C [ x , y ] ] isIso C f + +CatIso≡ : {C : Category ℓ ℓ'}{x y : C .ob}(f g : CatIso C x y) → f .fst ≡ g .fst → f ≡ g +CatIso≡ f g = Σ≡Prop isPropIsIso + +-- `constructor` of CatIso +catiso : {C : Category ℓ ℓ'}{x y : C .ob} + → (mor : C [ x , y ]) + → (inv : C [ y , x ]) + → (sec : inv ⋆⟨ C ⟩ mor ≡ C .id) + → (ret : mor ⋆⟨ C ⟩ inv ≡ C .id) + → CatIso C x y +catiso mor inv sec ret = mor , isiso inv sec ret + idCatIso : {C : Category ℓ ℓ'} {x : C .ob} → CatIso C x x -idCatIso {C = C} = (catiso (C .id) (C .id) (C .⋆IdL (C .id)) (C .⋆IdL (C .id))) +idCatIso {C = C} = C .id , isiso (C .id) (C .⋆IdL (C .id)) (C .⋆IdL (C .id)) isSet-CatIso : {C : Category ℓ ℓ'} → ∀ x y → isSet (CatIso C x y) -isSet-CatIso {C = C} x y F G p q = w - where - w : _ - CatIso.mor (w i j) = isSetHom C _ _ (cong CatIso.mor p) (cong CatIso.mor q) i j - CatIso.inv (w i j) = isSetHom C _ _ (cong CatIso.inv p) (cong CatIso.inv q) i j - CatIso.sec (w i j) = - isSet→SquareP - (λ i j → isProp→isSet {A = CatIso.inv (w i j) ⋆⟨ C ⟩ CatIso.mor (w i j) ≡ C .id} (isSetHom C _ _)) - (cong CatIso.sec p) (cong CatIso.sec q) (λ _ → CatIso.sec F) (λ _ → CatIso.sec G) i j - CatIso.ret (w i j) = - isSet→SquareP - (λ i j → isProp→isSet {A = CatIso.mor (w i j) ⋆⟨ C ⟩ CatIso.inv (w i j) ≡ C .id} (isSetHom C _ _)) - (cong CatIso.ret p) (cong CatIso.ret q) (λ _ → CatIso.ret F) (λ _ → CatIso.ret G) i j +isSet-CatIso {C = C} x y = isOfHLevelΣ 2 (C .isSetHom) (λ f → isProp→isSet (isPropIsIso f)) pathToIso : {C : Category ℓ ℓ'} {x y : C .ob} (p : x ≡ y) → CatIso C x y -pathToIso {C = C} p = J (λ z _ → CatIso _ _ z) idCatIso p +pathToIso {C = C} p = J (λ z _ → CatIso C _ z) idCatIso p pathToIso-refl : {C : Category ℓ ℓ'} {x : C .ob} → pathToIso {C = C} {x} refl ≡ idCatIso pathToIso-refl {C = C} {x} = JRefl (λ z _ → CatIso C x z) (idCatIso) + -- Univalent Categories record isUnivalent (C : Category ℓ ℓ') : Type (ℓ-max ℓ ℓ') where field @@ -102,6 +126,7 @@ record isUnivalent (C : Category ℓ ℓ') : Type (ℓ-max ℓ ℓ') where isGroupoid-ob : isGroupoid (C .ob) isGroupoid-ob = isOfHLevelPath'⁻ 2 (λ _ _ → isOfHLevelRespectEquiv 2 (invEquiv (univEquiv _ _)) (isSet-CatIso _ _)) + -- Opposite category _^op : Category ℓ ℓ' → Category ℓ ℓ' ob (C ^op) = ob C diff --git a/Cubical/Categories/Category/Properties.agda b/Cubical/Categories/Category/Properties.agda index bb58df08f3..fbc542bf5f 100644 --- a/Cubical/Categories/Category/Properties.agda +++ b/Cubical/Categories/Category/Properties.agda @@ -29,15 +29,6 @@ module _ {C : Category ℓ ℓ'} where → isOfHLevelDep 2 (λ y → C [ x , y ]) isSetHomP2r = isOfHLevel→isOfHLevelDep 2 (λ a → isSetHom C {y = a}) - open CatIso - - CatIso≡ : {x y : C .ob} (f g : CatIso C x y) → f .mor ≡ g .mor → f .inv ≡ g .inv → f ≡ g - mor (CatIso≡ f g p q i) = p i - inv (CatIso≡ f g p q i) = q i - sec (CatIso≡ f g p q i) j = - isSet→isSet' (isSetHom C) (λ i → seq' C (q i) (p i)) (λ _ → C .id) (sec f) (sec g) j i - ret (CatIso≡ f g p q i) j = - isSet→isSet' (isSetHom C) (λ i → seq' C (p i) (q i)) (λ _ → C .id) (ret f) (ret g) j i -- opposite of opposite is definitionally equal to itself involutiveOp : ∀ {C : Category ℓ ℓ'} → C ^op ^op ≡ C diff --git a/Cubical/Categories/Constructions/BinProduct.agda b/Cubical/Categories/Constructions/BinProduct.agda index 5d3658b45e..c20cb05078 100644 --- a/Cubical/Categories/Constructions/BinProduct.agda +++ b/Cubical/Categories/Constructions/BinProduct.agda @@ -67,10 +67,10 @@ module _ (C : Category ℓC ℓC') -- The isomorphisms in product category - open CatIso + open isIso iso× : {x y : C .ob}{z w : D .ob} → CatIso C x y → CatIso D z w → CatIso (C × D) (x , z) (y , w) - iso× f g .mor = f .mor , g .mor - iso× f g .inv = f .inv , g .inv - iso× f g .sec i = f .sec i , g .sec i - iso× f g .ret i = f .ret i , g .ret i + iso× f g .fst = f .fst , g .fst + iso× f g .snd .inv = f .snd .inv , g .snd .inv + iso× f g .snd .sec i = f .snd .sec i , g .snd .sec i + iso× f g .snd .ret i = f .snd .ret i , g .snd .ret i diff --git a/Cubical/Categories/Constructions/Slice.agda b/Cubical/Categories/Constructions/Slice.agda index faede1e471..779955d53b 100644 --- a/Cubical/Categories/Constructions/Slice.agda +++ b/Cubical/Categories/Constructions/Slice.agda @@ -7,8 +7,8 @@ open import Cubical.Foundations.HLevels open import Cubical.Foundations.Univalence open import Cubical.Foundations.Transport using (transpFill) -open import Cubical.Categories.Category -open import Cubical.Categories.Morphism renaming (isIso to isIsoC) +open import Cubical.Categories.Category renaming (isIso to isIsoC) +open import Cubical.Categories.Morphism open import Cubical.Data.Sigma @@ -148,7 +148,7 @@ isSetHom SliceCat {a} {b} (slicehom f c₁) (slicehom g c₂) p q = cong isoP p' -- SliceCat is univalent if C is univalent module _ ⦃ isU : isUnivalent C ⦄ where - open CatIso + open isIsoC open Iso module _ { xf yg : SliceOb } where @@ -168,12 +168,12 @@ module _ ⦃ isU : isUnivalent C ⦄ where pToIIso' = equivToIso pathIsoEquiv -- the iso in SliceCat we're given induces an iso in C between x and y - module _ ( cIso@(catiso kc lc s r) : CatIso SliceCat xf yg ) where + module _ ( cIso@(kc , isiso lc s r) : CatIso SliceCat xf yg ) where extractIso' : CatIso C x y - extractIso' .mor = kc .S-hom - extractIso' .inv = lc .S-hom - extractIso' .sec i = (s i) .S-hom - extractIso' .ret i = (r i) .S-hom + extractIso' .fst = kc .S-hom + extractIso' .snd .inv = lc .S-hom + extractIso' .snd .sec i = (s i) .S-hom + extractIso' .snd .ret i = (r i) .S-hom instance preservesUnivalenceSlice : isUnivalent SliceCat @@ -187,7 +187,7 @@ module _ ⦃ isU : isUnivalent C ⦄ where -- the meat of the proof sIso : Iso (xf ≡ yg) (CatIso _ xf yg) sIso .fun p = pathToIso p -- we use the normal pathToIso via path induction to get an isomorphism - sIso .inv is@(catiso kc lc s r) = SliceOb-≡-intro x≡y (symP (sym (lc .S-comm) ◁ lf≡f)) + sIso .inv is@(kc , isiso lc s r) = SliceOb-≡-intro x≡y (symP (sym (lc .S-comm) ◁ lf≡f)) where -- we get a path between xf and yg by combining paths between -- x and y, and f and g @@ -210,17 +210,17 @@ module _ ⦃ isU : isUnivalent C ⦄ where -- to show that f ≡ g, we show that l ≡ id -- by using C's isomorphism - pToI≡id : PathP (λ i → C [ x≡y (~ i) , x ]) (pathToIso {C = C} x≡y .inv) (C .id) - pToI≡id = J (λ y p → PathP (λ i → C [ p (~ i) , x ]) (pathToIso {C = C} p .inv) (C .id)) - (λ j → JRefl pToIFam pToIBase j .inv) + pToI≡id : PathP (λ i → C [ x≡y (~ i) , x ]) (pathToIso {C = C} x≡y .snd .inv) (C .id) + pToI≡id = J (λ y p → PathP (λ i → C [ p (~ i) , x ]) (pathToIso {C = C} p .snd .inv) (C .id)) + (λ j → JRefl pToIFam pToIBase j .snd .inv) x≡y where idx = C .id pToIFam = (λ z _ → CatIso C x z) pToIBase = catiso (C .id) idx (C .⋆IdL idx) (C .⋆IdL idx) - l≡pToI : l ≡ pathToIso {C = C} x≡y .inv - l≡pToI i = pToIIso .rightInv extractIso (~ i) .inv + l≡pToI : l ≡ pathToIso {C = C} x≡y .snd .inv + l≡pToI i = pToIIso .rightInv extractIso (~ i) .snd .inv l≡id : PathP (λ i → C [ x≡y (~ i) , x ]) l (C .id) l≡id = l≡pToI ◁ pToI≡id @@ -228,11 +228,11 @@ module _ ⦃ isU : isUnivalent C ⦄ where lf≡f : PathP (λ i → C [ x≡y (~ i) , c ]) (l ⋆⟨ C ⟩ f) f lf≡f = (λ i → (l≡id i) ⋆⟨ C ⟩ f) ▷ C .⋆IdL _ - sIso .rightInv is@(catiso kc lc s r) i = catiso (kc'≡kc i) (lc'≡lc i) (s'≡s i) (r'≡r i) + sIso .rightInv is@(kc , isiso lc s r) i = catiso (kc'≡kc i) (lc'≡lc i) (s'≡s i) (r'≡r i) -- we prove rightInv using a combination of univalence and the fact that homs are an h-set where - kc' = (sIso .fun) (sIso .inv is) .mor - lc' = (sIso .fun) (sIso .inv is) .inv + kc' = (sIso .fun) (sIso .inv is) .fst + lc' = (sIso .fun) (sIso .inv is) .snd .inv k' = kc' .S-hom l' = lc' .S-hom k = kc .S-hom @@ -246,7 +246,7 @@ module _ ⦃ isU : isUnivalent C ⦄ where -- mor k'≡k : k' ≡ k - k'≡k i = (pToIIso .rightInv extractIso) i .mor + k'≡k i = (pToIIso .rightInv extractIso) i .fst kcom'≡kcom : PathP (λ j → (k'≡k j) ⋆⟨ C ⟩ g ≡ f) (kc' .S-comm) (kc .S-comm) kcom'≡kcom = isSetHomP1 {C = C} _ _ λ i → (k'≡k i) ⋆⟨ C ⟩ g @@ -256,7 +256,7 @@ module _ ⦃ isU : isUnivalent C ⦄ where -- inv l'≡l : l' ≡ l - l'≡l i = (pToIIso .rightInv extractIso) i .inv + l'≡l i = (pToIIso .rightInv extractIso) i .snd .inv lcom'≡lcom : PathP (λ j → (l'≡l j) ⋆⟨ C ⟩ f ≡ g) (lc' .S-comm) (lc .S-comm) lcom'≡lcom = isSetHomP1 {C = C} _ _ λ i → (l'≡l i) ⋆⟨ C ⟩ f @@ -266,13 +266,13 @@ module _ ⦃ isU : isUnivalent C ⦄ where -- sec - s' = (sIso .fun) (sIso .inv is) .sec + s' = (sIso .fun) (sIso .inv is) .snd .sec s'≡s : PathP (λ i → lc'≡lc i ⋆⟨ SliceCat ⟩ kc'≡kc i ≡ SliceCat .id) s' s s'≡s = isSetHomP1 {C = SliceCat} _ _ λ i → lc'≡lc i ⋆⟨ SliceCat ⟩ kc'≡kc i -- ret - r' = (sIso .fun) (sIso .inv is) .ret + r' = (sIso .fun) (sIso .inv is) .snd .ret r'≡r : PathP (λ i → kc'≡kc i ⋆⟨ SliceCat ⟩ lc'≡lc i ≡ SliceCat .id) r' r r'≡r = isSetHomP1 {C = SliceCat} _ _ λ i → kc'≡kc i ⋆⟨ SliceCat ⟩ lc'≡lc i diff --git a/Cubical/Categories/Equivalence/Properties.agda b/Cubical/Categories/Equivalence/Properties.agda index c1e73b8deb..059492bf3a 100644 --- a/Cubical/Categories/Equivalence/Properties.agda +++ b/Cubical/Categories/Equivalence/Properties.agda @@ -3,6 +3,8 @@ module Cubical.Categories.Equivalence.Properties where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv + renaming (isEquiv to isEquivMap) open import Cubical.Data.Sigma open import Cubical.Categories.Category open import Cubical.Categories.Functor @@ -14,7 +16,7 @@ open import Cubical.HITs.PropositionalTruncation.Base open Category open Functor open NatIso -open CatIso +open isIso open NatTrans open isEquivalence @@ -34,9 +36,9 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where ; ε = _ } c c' f g p = f ≡⟨ sqRL η ⟩ - cIso .mor ⋆⟨ C ⟩ G ⟪ F ⟪ f ⟫ ⟫ ⋆⟨ C ⟩ c'Iso .inv - ≡⟨ cong (λ v → cIso .mor ⋆⟨ C ⟩ (G ⟪ v ⟫) ⋆⟨ C ⟩ c'Iso .inv) p ⟩ - cIso .mor ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⟫ ⋆⟨ C ⟩ c'Iso .inv + cIso .fst ⋆⟨ C ⟩ G ⟪ F ⟪ f ⟫ ⟫ ⋆⟨ C ⟩ c'Iso .snd .inv + ≡⟨ cong (λ v → cIso .fst ⋆⟨ C ⟩ (G ⟪ v ⟫) ⋆⟨ C ⟩ c'Iso .snd .inv) p ⟩ + cIso .fst ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⟫ ⋆⟨ C ⟩ c'Iso .snd .inv ≡⟨ sym (sqRL η) ⟩ g ∎ @@ -63,30 +65,79 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where cIso⁻ = symCatIso cIso c'Iso⁻ = symCatIso c'Iso - h = cIso .mor ⋆⟨ C ⟩ G ⟪ g ⟫ ⋆⟨ C ⟩ c'Iso .inv + h = cIso .fst ⋆⟨ C ⟩ G ⟪ g ⟫ ⋆⟨ C ⟩ c'Iso .snd .inv -- we show that both `G ⟪ g ⟫` and `G ⟪ F ⟪ h ⟫ ⟫` -- are equal to the same thing -- namely : cIso .inv ⋆⟨ C ⟩ h ⋆⟨ C ⟩ c'Iso .mor - Gg≡ηhη : G ⟪ g ⟫ ≡ cIso .inv ⋆⟨ C ⟩ h ⋆⟨ C ⟩ c'Iso .mor + Gg≡ηhη : G ⟪ g ⟫ ≡ cIso .snd .inv ⋆⟨ C ⟩ h ⋆⟨ C ⟩ c'Iso .fst Gg≡ηhη = invMoveL cAreInv move-c' ∙ sym (C .⋆Assoc _ _ _) where - cAreInv : areInv _ (cIso .mor) (cIso .inv) + cAreInv : areInv _ (cIso .fst) (cIso .snd .inv) cAreInv = CatIso→areInv cIso - c'AreInv : areInv _ (c'Iso .mor) (c'Iso .inv) + c'AreInv : areInv _ (c'Iso .fst) (c'Iso .snd .inv) c'AreInv = CatIso→areInv c'Iso - move-c' : cIso .mor ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ h ⋆⟨ C ⟩ c'Iso .mor + move-c' : cIso .fst ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ h ⋆⟨ C ⟩ c'Iso .fst move-c' = invMoveR (symAreInv c'AreInv) refl GFh≡Gg : G ⟪ F ⟪ h ⟫ ⟫ ≡ G ⟪ g ⟫ GFh≡Gg = G ⟪ F ⟪ h ⟫ ⟫ ≡⟨ sqLR η ⟩ - cIso .inv ⋆⟨ C ⟩ h ⋆⟨ C ⟩ c'Iso .mor + cIso .snd .inv ⋆⟨ C ⟩ h ⋆⟨ C ⟩ c'Iso .fst ≡⟨ sym Gg≡ηhη ⟩ G ⟪ g ⟫ ∎ + isEquiv→FullyFaithful : ∀ {F : Functor C D} → isEquivalence F → isFullyFaithful F + isEquiv→FullyFaithful {F = F} h = isFull+Faithful→isFullyFaithful {F = F} (isEquiv→Full h) (isEquiv→Faithful h) + isEquiv→Surj : ∀ {F : Functor C D} → isEquivalence F → isEssentiallySurj F - isEquiv→Surj isE d = (isE .invFunc ⟅ d ⟆) , isIso→CatIso ((isE .ε .nIso) d) + isEquiv→Surj isE d = ∣ (isE .invFunc ⟅ d ⟆) , isIso→CatIso ((isE .ε .nIso) d) ∣₁ + + +-- A fully-faithful functor that induces equivalences on objects is an equivalence + +Mor : (C : Category ℓC ℓC') → Type _ +Mor C = Σ[ x ∈ C .ob ] Σ[ y ∈ C .ob ] C [ x , y ] + +projMor : {C : Category ℓC ℓC'} → Mor C → C .ob × C .ob +projMor (x , y , _) = x , y + +module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} + {F : Functor C D} where + + F-Mor : Mor C → Mor D + F-Mor (x , y , f) = F .F-ob x , F .F-ob y , F .F-hom f + + isFullyFaithful+isEquivF-ob→isEquiv : isFullyFaithful F → isEquivMap (F .F-ob) → isEquivalence F + isFullyFaithful+isEquivF-ob→isEquiv fullfaith isequiv = w + where + isEquivF-Mor : isEquivMap F-Mor + isEquivF-Mor = {!!} + + w-inv-ob : D .ob → C .ob + w-inv-ob = invIsEq isequiv + + w-hom-path : {x y : D .ob}(f : D [ x , y ]) + → (i : I) → D [ secIsEq isequiv x (~ i) , secIsEq isequiv y (~ i) ] + w-hom-path {x = x} {y = y} f i = + transport-filler (λ i → D [ secIsEq isequiv x (~ i) , secIsEq isequiv y (~ i) ]) f i + + w-inv : Functor D C + w-inv .F-ob = invIsEq isequiv + w-inv .F-hom f = invIsEq (fullfaith _ _) (w-hom-path f i1) + w-inv .F-id = {!!} + w-inv .F-seq = {!!} + + w-η-path : 𝟙⟨ C ⟩ ≡ w-inv ∘F F + w-η-path = Functor≡ (λ x → sym (retIsEq isequiv x)) {!!} + + w-ε-path : F ∘F w-inv ≡ 𝟙⟨ D ⟩ + w-ε-path = Functor≡ (λ x → secIsEq isequiv x) {!!} + + w : isEquivalence F + w .invFunc = w-inv + w .η = pathToNatIso w-η-path + w .ε = pathToNatIso w-ε-path diff --git a/Cubical/Categories/Equivalence/WeakEquivalence.agda b/Cubical/Categories/Equivalence/WeakEquivalence.agda index f40a8a2006..eb4e8718c5 100644 --- a/Cubical/Categories/Equivalence/WeakEquivalence.agda +++ b/Cubical/Categories/Equivalence/WeakEquivalence.agda @@ -5,6 +5,8 @@ module Cubical.Categories.Equivalence.WeakEquivalence where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Equiv renaming (isEquiv to isEquivMap) +open import Cubical.Functions.Surjection +open import Cubical.Functions.Embedding open import Cubical.Data.Sigma open import Cubical.Categories.Category open import Cubical.Categories.Functor @@ -16,7 +18,7 @@ open import Cubical.HITs.PropositionalTruncation.Base open Category open Functor open NatIso -open CatIso +open isIso open NatTrans open isEquivalence open _≃ᶜ_ @@ -33,9 +35,8 @@ record isWeakEquivalence {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (func : Functor C D) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where field - full : isFull func - faith : isFaithful func - surj : isEssentiallySurj func + fullfaith : isFullyFaithful func + esssurj : isEssentiallySurj func record WeakEquivalence (C : Category ℓC ℓC') (D : Category ℓD ℓD') : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where @@ -50,23 +51,22 @@ open WeakEquivalence isEquiv→isWeakEquiv : isEquivalence F → isWeakEquivalence F -isEquiv→isWeakEquiv isequiv .full = isEquiv→Full isequiv -isEquiv→isWeakEquiv isequiv .faith = isEquiv→Faithful isequiv -isEquiv→isWeakEquiv isequiv .surj = isEquiv→Surj isequiv +isEquiv→isWeakEquiv isequiv .fullfaith = isEquiv→FullyFaithful isequiv +isEquiv→isWeakEquiv isequiv .esssurj = isEquiv→Surj isequiv module _ - {C : Category ℓC ℓC'}(isUnivC : isUnivalent C) - {D : Category ℓD ℓD'}(isUnivD : isUnivalent D) + (isUnivC : isUnivalent C) + (isUnivD : isUnivalent D) where open isUnivalent - module _ {F : WeakEquivalence C D} where - - isEquivF-ob : isEquivMap (F .func .F-ob) - isEquivF-ob = {!!} + 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) , + isSurj→isSurj-ob isUnivD {F = F} (is-w-equiv .esssurj)) isWeakEquiv→isEquiv : isWeakEquivalence F → isEquivalence F diff --git a/Cubical/Categories/Functor/Base.agda b/Cubical/Categories/Functor/Base.agda index c5c5441220..d3aa9eb819 100644 --- a/Cubical/Categories/Functor/Base.agda +++ b/Cubical/Categories/Functor/Base.agda @@ -28,7 +28,7 @@ record Functor (C : Category ℓC ℓC') (D : Category ℓD ℓD') : isFull = (x y : _) (F[f] : D [ F-ob x , F-ob y ]) → ∃[ f ∈ C [ x , y ] ] F-hom f ≡ F[f] isFaithful = (x y : _) (f g : C [ x , y ]) → F-hom f ≡ F-hom g → f ≡ g isFullyFaithful = (x y : _) → isEquiv (F-hom {x = x} {y = y}) - isEssentiallySurj = (d : D .ob) → Σ[ c ∈ C .ob ] CatIso D (F-ob c) d + isEssentiallySurj = (d : D .ob) → ∃[ c ∈ C .ob ] CatIso D (F-ob c) d -- preservation of commuting squares and triangles F-square : {x y u v : C .ob} diff --git a/Cubical/Categories/Functor/Properties.agda b/Cubical/Categories/Functor/Properties.agda index 2e8f8b2dd3..362efde99a 100644 --- a/Cubical/Categories/Functor/Properties.agda +++ b/Cubical/Categories/Functor/Properties.agda @@ -10,7 +10,10 @@ open import Cubical.Foundations.GroupoidLaws using (lUnit; rUnit; assoc; cong- open import Cubical.Foundations.HLevels open import Cubical.Functions.Surjection open import Cubical.Functions.Embedding +open import Cubical.HITs.PropositionalTruncation as Prop +open import Cubical.Data.Sigma open import Cubical.Categories.Category +open import Cubical.Categories.Isomorphism open import Cubical.Categories.Functor.Base @@ -88,7 +91,7 @@ module _ {F : Functor C D} where -- functors preserve isomorphisms preserveIsosF : ∀ {x y} → CatIso C x y → CatIso D (F ⟅ x ⟆) (F ⟅ y ⟆) - preserveIsosF {x} {y} (catiso f f⁻¹ sec' ret') = + preserveIsosF {x} {y} (f , isiso f⁻¹ sec' ret') = catiso g g⁻¹ -- sec @@ -143,6 +146,14 @@ isSetFunctor {D = D} {C = C} isSet-D-ob F G p q = w (λ i₁ → F-seq (p i₁) _ _) (λ i₁ → F-seq (q i₁) _ _) refl refl i i₁ +-- Conservative Functor, +-- namely if a morphism f is mapped to an isomorphism, +-- the morphism f is itself isomorphism. + +isConservative : (F : Functor C D) → Type _ +isConservative {C = C} {D = D} F = {x y : C .ob}{f : C [ x , y ]} → isIso D (F .F-hom f) → isIso C f + + -- Fully-faithfulness of functors module _ {F : Functor C D} where @@ -156,3 +167,71 @@ module _ {F : Functor C D} where isFull+Faithful→isFullyFaithful : isFull F → isFaithful F → isFullyFaithful F isFull+Faithful→isFullyFaithful full faith x y = isEmbedding×isSurjection→isEquiv (injEmbedding (C .isSetHom) (D .isSetHom) (faith x y _ _) , full x y) + + + -- Fully-faithful functor is conservative + + open isIso + + isFullyFaithful→Conservative : isFullyFaithful F → isConservative F + isFullyFaithful→Conservative fullfaith {x = x} {y = y} {f = f} isoFf = w + where + w : isIso C f + w .inv = invIsEq (fullfaith _ _) (isoFf .inv) + w .sec = isFullyFaithful→Faithful fullfaith _ _ _ _ + (F .F-seq _ _ + ∙ (λ i → secIsEq (fullfaith _ _) (isoFf .inv) i ⋆⟨ D ⟩ F .F-hom f) + ∙ isoFf .sec + ∙ sym (F .F-id)) + w .ret = isFullyFaithful→Faithful fullfaith _ _ _ _ + (F .F-seq _ _ + ∙ (λ i → F .F-hom f ⋆⟨ D ⟩ secIsEq (fullfaith _ _) (isoFf .inv) i) + ∙ isoFf .ret + ∙ sym (F .F-id)) + + +-- Functors inducing surjection on objects is essentially surjective + +isSurj-ob→isSurj : {F : Functor C D} → isSurjection (F .F-ob) → isEssentiallySurj F +isSurj-ob→isSurj surj y = Prop.map (λ (x , p) → x , pathToIso p) (surj y) + + +-- Fully-faithful functors induce equivalence on isomorphisms + +isFullyFaithful→isEquivF-Iso : {F : Functor C D} + → isFullyFaithful F → ∀ x y → isEquiv (F-Iso {F = F} {x = x} {y = y}) +isFullyFaithful→isEquivF-Iso {F = F} fullfaith x y = + Σ-cong-equiv-prop (_ , fullfaith x y) isPropIsIso isPropIsIso _ + (λ f → isFullyFaithful→Conservative {F = F} fullfaith {f = f}) .snd + + +-- Functors involving univalent categories + +module _ + (isUnivD : isUnivalent D) + where + + open isUnivalent isUnivD + + -- Essentially surjective functor with univalent target induces surjection on objects + + isSurj→isSurj-ob : {F : Functor C D} → isEssentiallySurj F → isSurjection (F .F-ob) + isSurj→isSurj-ob surj y = Prop.map (λ (x , f) → x , CatIsoToPath f) (surj y) + + +module _ + (isUnivC : isUnivalent C) + (isUnivD : isUnivalent D) + {F : Functor C D} + where + + open isUnivalent + + -- 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 = + isEquiv[equivFunA≃B∘f]→isEquiv[f] _ (_ , isUnivD .univ _ _) + (subst isEquiv (F-pathToIso-∘ {F = F}) + (compEquiv (_ , isUnivC .univ _ _) + (_ , isFullyFaithful→isEquivF-Iso {F = F} fullfaith x y) .snd)) diff --git a/Cubical/Categories/Instances/CommRings.agda b/Cubical/Categories/Instances/CommRings.agda index 4933a4cec8..dc8c79aea4 100644 --- a/Cubical/Categories/Instances/CommRings.agda +++ b/Cubical/Categories/Instances/CommRings.agda @@ -29,7 +29,7 @@ open import Cubical.HITs.PropositionalTruncation open Category hiding (_∘_) open isUnivalent -open CatIso +open isIso open Functor open CommRingStr open RingHoms @@ -58,8 +58,8 @@ F-seq forgetfulFunctor f g = funExt (λ _ → refl) open Iso CommRingIsoIsoCatIso : {R S : CommRing ℓ} → Iso (CommRingIso R S) (CatIso CommRingsCategory R S) -mor (fun CommRingIsoIsoCatIso e) = (e .fst .fun) , (e .snd) -inv (fun (CommRingIsoIsoCatIso {R = R} {S}) e) = +(fun CommRingIsoIsoCatIso e) .fst = (e .fst .fun) , (e .snd) +(fun (CommRingIsoIsoCatIso {R = R} {S}) e) .snd .inv = e .fst .inv , makeIsRingHom (sym (cong (e .fst .inv) (pres1 (e .snd))) ∙ e .fst .leftInv _) (λ x y → let rem = e .fst .rightInv _ @@ -70,14 +70,14 @@ inv (fun (CommRingIsoIsoCatIso {R = R} {S}) e) = ∙∙ (λ i → S .snd ._·_ (e .fst .rightInv x (~ i)) (e .fst .rightInv y (~ i))) ∙∙ sym (pres· (e .snd) _ _) in injCommRingIso {R = R} {S} e _ _ rem) -sec (fun CommRingIsoIsoCatIso e) = RingHom≡ (funExt (e .fst .rightInv)) -ret (fun CommRingIsoIsoCatIso e) = RingHom≡ (funExt (e .fst .leftInv)) -fun (fst (inv CommRingIsoIsoCatIso e)) = e .mor .fst -inv (fst (inv CommRingIsoIsoCatIso e)) = e .inv .fst -rightInv (fst (inv CommRingIsoIsoCatIso e)) x i = fst (e .sec i) x -leftInv (fst (inv CommRingIsoIsoCatIso e)) x i = fst (e .ret i) x -snd (inv CommRingIsoIsoCatIso e) = e .mor .snd -rightInv CommRingIsoIsoCatIso x = CatIso≡ _ _ (RingHom≡ refl) (RingHom≡ refl) +(fun CommRingIsoIsoCatIso e) .snd .sec = RingHom≡ (funExt (e .fst .rightInv)) +(fun CommRingIsoIsoCatIso e) .snd .ret = RingHom≡ (funExt (e .fst .leftInv)) +fun (fst (inv CommRingIsoIsoCatIso e)) = e .fst .fst +inv (fst (inv CommRingIsoIsoCatIso e)) = e .snd .inv .fst +rightInv (fst (inv CommRingIsoIsoCatIso e)) x i = fst (e .snd .sec i) x +leftInv (fst (inv CommRingIsoIsoCatIso e)) x i = fst (e .snd .ret i) x +snd (inv CommRingIsoIsoCatIso e) = e .fst .snd +rightInv CommRingIsoIsoCatIso x = CatIso≡ _ _ (RingHom≡ refl) leftInv (CommRingIsoIsoCatIso {R = R} {S}) x = Σ≡Prop (λ x → isPropIsRingHom (CommRingStr→RingStr (R .snd)) (x .fun) @@ -97,7 +97,6 @@ univ isUnivalentCommRingsCategory R S = subst isEquiv (funExt rem) (≡≃CatIso rem : ∀ p → ≡≃CatIso .fst p ≡ pathToIso p rem p = CatIso≡ _ _ (RingHom≡ (funExt λ x → cong (transport (cong fst p)) (sym (transportRefl x)))) - (RingHom≡ refl) TerminalCommRing : Terminal {ℓ-suc ℓ-zero} CommRingsCategory fst TerminalCommRing = UnitCommRing diff --git a/Cubical/Categories/Instances/Functors.agda b/Cubical/Categories/Instances/Functors.agda index dde890a76b..e80a1079c5 100644 --- a/Cubical/Categories/Instances/Functors.agda +++ b/Cubical/Categories/Instances/Functors.agda @@ -2,11 +2,11 @@ module Cubical.Categories.Instances.Functors where -open import Cubical.Categories.Category +open import Cubical.Categories.Category renaming (isIso to isIsoC) open import Cubical.Categories.Functor.Base open import Cubical.Categories.NaturalTransformation.Base open import Cubical.Categories.NaturalTransformation.Properties -open import Cubical.Categories.Morphism renaming (isIso to isIsoC) +open import Cubical.Categories.Morphism open import Cubical.Foundations.Prelude private diff --git a/Cubical/Categories/Instances/Sets.agda b/Cubical/Categories/Instances/Sets.agda index 88fca1f33e..fb598e7849 100644 --- a/Cubical/Categories/Instances/Sets.agda +++ b/Cubical/Categories/Instances/Sets.agda @@ -66,24 +66,24 @@ module _ {C : Category ℓ ℓ'} {F : Functor C (SET ℓ')} where -- properties -- TODO: move to own file -open CatIso renaming (inv to cInv) +open isIso renaming (inv to cInv) open Iso module _ {A B : (SET ℓ) .ob } where Iso→CatIso : Iso (fst A) (fst B) → CatIso (SET ℓ) A B - Iso→CatIso is .mor = is .fun - Iso→CatIso is .cInv = is .inv - Iso→CatIso is .sec = funExt λ b → is .rightInv b -- is .rightInv - Iso→CatIso is .ret = funExt λ b → is .leftInv b -- is .rightInv + Iso→CatIso is .fst = is .fun + Iso→CatIso is .snd .cInv = is .inv + Iso→CatIso is .snd .sec = funExt λ b → is .rightInv b -- is .rightInv + Iso→CatIso is .snd .ret = funExt λ b → is .leftInv b -- is .rightInv CatIso→Iso : CatIso (SET ℓ) A B → Iso (fst A) (fst B) - CatIso→Iso cis .fun = cis .mor - CatIso→Iso cis .inv = cis .cInv - CatIso→Iso cis .rightInv = funExt⁻ λ b → cis .sec b - CatIso→Iso cis .leftInv = funExt⁻ λ b → cis .ret b + CatIso→Iso cis .fun = cis .fst + CatIso→Iso cis .inv = cis .snd .cInv + CatIso→Iso cis .rightInv = funExt⁻ λ b → cis .snd .sec b + CatIso→Iso cis .leftInv = funExt⁻ λ b → cis .snd .ret b Iso-Iso-CatIso : Iso (Iso (fst A) (fst B)) (CatIso (SET ℓ) A B) @@ -110,8 +110,8 @@ isUnivalent.univ isUnivalentSET (A , isSet-A) (B , isSet-B) = invEq (congEquiv (isoToEquiv (invIso Iso-Iso-CatIso))) (SetsIso≡-ext isSet-A isSet-B - (λ x i → transp (λ _ → B) i (ci .mor (transp (λ _ → A) i x))) - (λ x i → transp (λ _ → A) i (ci .cInv (transp (λ _ → B) i x)))) + (λ x i → transp (λ _ → B) i (ci .fst (transp (λ _ → A) i x))) + (λ x i → transp (λ _ → A) i (ci .snd .cInv (transp (λ _ → B) i x)))) -- SET is complete diff --git a/Cubical/Categories/Isomorphism.agda b/Cubical/Categories/Isomorphism.agda index 3af5ef285a..f411ccc015 100644 --- a/Cubical/Categories/Isomorphism.agda +++ b/Cubical/Categories/Isomorphism.agda @@ -3,10 +3,9 @@ module Cubical.Categories.Isomorphism where open import Cubical.Foundations.Prelude open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.Function open import Cubical.Categories.Category - renaming (CatIso≡ to CatIso≡Ext) open import Cubical.Categories.Functor.Base -open import Cubical.Categories.Functor.Properties private variable @@ -16,39 +15,27 @@ private module _ {C : Category ℓC ℓC'} where open Category C - open CatIso + open isIso ⋆Iso : {x y z : ob} → (f : CatIso C x y)(g : CatIso C y z) → CatIso C x z - ⋆Iso f g .mor = f .mor ⋆ g .mor - ⋆Iso f g .inv = g .inv ⋆ f .inv - ⋆Iso f g .sec = sym (⋆Assoc _ _ _) - ∙ (λ i → ⋆Assoc (g .inv) (f .inv) (f .mor) i ⋆ g .mor) - ∙ (λ i → (g .inv ⋆ f .sec i) ⋆ g .mor) - ∙ (λ i → ⋆IdR (g .inv) i ⋆ g .mor) - ∙ g .sec - ⋆Iso f g .ret = sym (⋆Assoc _ _ _) - ∙ (λ i → ⋆Assoc (f .mor) (g .mor) (g .inv) i ⋆ f .inv) - ∙ (λ i → (f .mor ⋆ g .ret i) ⋆ f .inv) - ∙ (λ i → ⋆IdR (f .mor) i ⋆ f .inv) - ∙ f .ret + ⋆Iso f g .fst = f .fst ⋆ g .fst + ⋆Iso f g .snd .inv = g .snd .inv ⋆ f .snd .inv + ⋆Iso f g .snd .sec = sym (⋆Assoc _ _ _) + ∙ (λ i → ⋆Assoc (g .snd .inv) (f .snd .inv) (f .fst) i ⋆ g .fst) + ∙ (λ i → (g .snd .inv ⋆ f .snd .sec i) ⋆ g .fst) + ∙ (λ i → ⋆IdR (g .snd .inv) i ⋆ g .fst) + ∙ g .snd .sec + ⋆Iso f g .snd .ret = sym (⋆Assoc _ _ _) + ∙ (λ i → ⋆Assoc (f .fst) (g .fst) (g .snd .inv) i ⋆ f .snd .inv) + ∙ (λ i → (f .fst ⋆ g .snd .ret i) ⋆ f .snd .inv) + ∙ (λ i → ⋆IdR (f .fst) i ⋆ f .snd .inv) + ∙ f .snd .ret compIso : {x y z : ob} → (g : CatIso C y z)(f : CatIso C x y) → CatIso C x z compIso g f = ⋆Iso f g - CatIso≡ : {x y : ob} (f g : CatIso C x y) → f .mor ≡ g .mor → f ≡ g - CatIso≡ f g p = CatIso≡Ext f g p inv≡ - where - inv≡ : f .inv ≡ g .inv - inv≡ = sym (⋆IdL _) - ∙ (λ i → g .sec (~ i) ⋆ f .inv) - ∙ ⋆Assoc _ _ _ - ∙ (λ i → g .inv ⋆ (p (~ i) ⋆ f .inv)) - ∙ (λ i → g .inv ⋆ f .ret i) - ∙ ⋆IdR _ - - ⋆IsoIdL : {x y : ob} → (f : CatIso C x y) → ⋆Iso idCatIso f ≡ f ⋆IsoIdL _ = CatIso≡ _ _ (⋆IdL _) @@ -66,33 +53,72 @@ module _ {C : Category ℓC ℓC'} where ∙ (λ i → ⋆Iso (pathToIso-refl (~ i)) (pathToIso refl)) + pathToIso-Square : {x y z w : ob} + → (p : x ≡ y)(q : z ≡ w) + → (f : Hom[ x , z ])(g : Hom[ y , w ]) + → PathP (λ i → Hom[ p i , q i ]) f g + → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} p .fst ⋆ g + pathToIso-Square {x = x} {z = z} p q = + J (λ y p → + (w : ob)(q : z ≡ w)(f : Hom[ x , z ])(g : Hom[ y , w ]) + → PathP (λ i → Hom[ p i , q i ]) f g + → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} p .fst ⋆ g) + (λ _ → J (λ w q → + (f : Hom[ x , z ])(g : Hom[ x , w ]) + → PathP (λ i → Hom[ x , q i ]) f g + → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} refl .fst ⋆ g) + sqr-refl) p _ q + where + sqr-refl : {x z : ob} → (f g : Hom[ x , z ]) → f ≡ g + → f ⋆ pathToIso {C = C} refl .fst ≡ pathToIso {C = C} refl .fst ⋆ g + sqr-refl f g p = (λ i → f ⋆ pathToIso-refl {C = C} i .fst) + ∙ ⋆IdR _ ∙ p ∙ sym (⋆IdL _) + ∙ (λ i → pathToIso-refl {C = C} (~ i) .fst ⋆ g) + + module _ {C : Category ℓC ℓC'} where open Category - open CatIso + open isIso op-Iso : {x y : C .ob} → CatIso C x y → CatIso (C ^op) x y - op-Iso f .mor = f .inv - op-Iso f .inv = f .mor - op-Iso f .sec = f .sec - op-Iso f .ret = f .ret + op-Iso f .fst = f .snd .inv + op-Iso f .snd .inv = f .fst + op-Iso f .snd .sec = f .snd .sec + op-Iso f .snd .ret = f .snd .ret module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}{F : Functor C D} where - open Category - open CatIso + open Category hiding (_∘_) + open isIso open Functor + F-PresIsIso : {x y : C .ob}{f : C [ x , y ]} → isIso C f → isIso D (F .F-hom f) + F-PresIsIso f .inv = F . F-hom (f .inv) + F-PresIsIso f .sec = sym (F .F-seq (f .inv) _) ∙ cong (F .F-hom) (f .sec) ∙ F .F-id + F-PresIsIso f .ret = sym (F .F-seq _ (f .inv)) ∙ cong (F .F-hom) (f .ret) ∙ F .F-id + + F-Iso : {x y : C .ob} → CatIso C x y → CatIso D (F .F-ob x) (F .F-ob y) - F-Iso f .mor = F . F-hom (f .mor) - F-Iso f .inv = F . F-hom (f .inv) - F-Iso f .sec = sym (F .F-seq (f .inv) (f .mor)) ∙ cong (F .F-hom) (f .sec) ∙ F .F-id - F-Iso f .ret = sym (F .F-seq (f .mor) (f .inv)) ∙ cong (F .F-hom) (f .ret) ∙ F .F-id + F-Iso f .fst = F . F-hom (f .fst) + F-Iso f .snd = F-PresIsIso (f .snd) F-Iso-PresId : {x : C .ob} → F-Iso (idCatIso {x = x}) ≡ idCatIso F-Iso-PresId = CatIso≡ _ _ (F .F-id) F-Iso-Pres⋆ : {x y z : C .ob} → (f : CatIso C x y)(g : CatIso C y z) → F-Iso (⋆Iso f g) ≡ ⋆Iso (F-Iso f) (F-Iso g) F-Iso-Pres⋆ _ _ = CatIso≡ _ _ (F .F-seq _ _) + + + F-pathToIso : {x y : C .ob} → (p : x ≡ y) → F-Iso (pathToIso p) ≡ pathToIso (cong (F .F-ob) p) + F-pathToIso p = J (λ y p → F-Iso (pathToIso p) ≡ pathToIso (cong (F .F-ob) p)) F-pathToIso-refl p + where + F-pathToIso-refl : {x : C .ob} → F-Iso (pathToIso {x = x} refl) ≡ pathToIso (cong (F .F-ob) refl) + F-pathToIso-refl = cong F-Iso pathToIso-refl + ∙ F-Iso-PresId + ∙ sym pathToIso-refl + + F-pathToIso-∘ : {x y : C .ob} → F-Iso ∘ pathToIso {x = x} {y = y} ≡ pathToIso ∘ cong (F .F-ob) + F-pathToIso-∘ i p = F-pathToIso p i diff --git a/Cubical/Categories/Limits/Initial.agda b/Cubical/Categories/Limits/Initial.agda index a5c06b6a42..4c546ba0ac 100644 --- a/Cubical/Categories/Limits/Initial.agda +++ b/Cubical/Categories/Limits/Initial.agda @@ -47,14 +47,14 @@ module _ (C : Category ℓ ℓ') where isPropIsInitial : (x : ob) → isProp (isInitial x) isPropIsInitial _ = isPropΠ λ _ → isPropIsContr - open CatIso + open isIso -- Objects that are initial are isomorphic. initialToIso : (x y : Initial) → CatIso C (initialOb x) (initialOb y) - mor (initialToIso x y) = initialArrow x (initialOb y) - inv (initialToIso x y) = initialArrow y (initialOb x) - sec (initialToIso x y) = initialEndoIsId y _ - ret (initialToIso x y) = initialEndoIsId x _ + initialToIso x y .fst = initialArrow x (initialOb y) + initialToIso x y .snd .inv = initialArrow y (initialOb x) + initialToIso x y .snd .sec = initialEndoIsId y _ + initialToIso x y .snd .ret = initialEndoIsId x _ open isUnivalent diff --git a/Cubical/Categories/Limits/Terminal.agda b/Cubical/Categories/Limits/Terminal.agda index b9a472ddaa..438ac83c10 100644 --- a/Cubical/Categories/Limits/Terminal.agda +++ b/Cubical/Categories/Limits/Terminal.agda @@ -43,14 +43,14 @@ module _ (C : Category ℓ ℓ') where isPropIsTerminal : (x : ob) → isProp (isTerminal x) isPropIsTerminal _ = isPropΠ λ _ → isPropIsContr - open CatIso + open isIso -- Objects that are initial are isomorphic. terminalToIso : (x y : Terminal) → CatIso C (terminalOb x) (terminalOb y) - mor (terminalToIso x y) = terminalArrow y (terminalOb x) - inv (terminalToIso x y) = terminalArrow x (terminalOb y) - sec (terminalToIso x y) = terminalEndoIsId y _ - ret (terminalToIso x y) = terminalEndoIsId x _ + terminalToIso x y .fst = terminalArrow y (terminalOb x) + terminalToIso x y .snd .inv = terminalArrow x (terminalOb y) + terminalToIso x y .snd .sec = terminalEndoIsId y _ + terminalToIso x y .snd .ret = terminalEndoIsId x _ open isUnivalent diff --git a/Cubical/Categories/Morphism.agda b/Cubical/Categories/Morphism.agda index 0cf33a1c93..58101a3ceb 100644 --- a/Cubical/Categories/Morphism.agda +++ b/Cubical/Categories/Morphism.agda @@ -39,12 +39,6 @@ module _ (C : Category ℓ ℓ') where sec : g ⋆ f ≡ id ret : f ⋆ g ≡ id - record isIso (f : Hom[ x , y ]) : Type ℓ' where - field - inv : Hom[ y , x ] - sec : inv ⋆ f ≡ id - ret : f ⋆ inv ≡ id - -- C can be implicit here module _ {C : Category ℓ ℓ'} where @@ -101,29 +95,24 @@ module _ {C : Category ℓ ℓ'} where sec (isIso→areInv isI) = sec isI ret (isIso→areInv isI) = ret isI - open CatIso - -- isIso agrees with CatIso + -- Back and forth between isIso and CatIso + isIso→CatIso : ∀ {f : C [ x , y ]} → isIso C f → CatIso C x y - mor (isIso→CatIso {f = f} x) = f - inv (isIso→CatIso x) = inv x - sec (isIso→CatIso x) = sec x - ret (isIso→CatIso x) = ret x + isIso→CatIso x = _ , x CatIso→isIso : (cIso : CatIso C x y) - → isIso C (cIso .mor) - inv (CatIso→isIso f) = inv f - sec (CatIso→isIso f) = sec f - ret (CatIso→isIso f) = ret f + → isIso C (cIso .fst) + CatIso→isIso = snd CatIso→areInv : (cIso : CatIso C x y) - → areInv C (cIso .mor) (cIso .inv) + → areInv C (cIso .fst) (cIso .snd .inv) CatIso→areInv cIso = isIso→areInv (CatIso→isIso cIso) -- reverse of an iso is also an iso symCatIso : ∀ {x y} → CatIso C x y → CatIso C y x - symCatIso (catiso mor inv sec ret) = catiso inv mor ret sec + symCatIso (mor , isiso inv sec ret) = inv , isiso mor ret sec diff --git a/Cubical/Categories/NaturalTransformation/Base.agda b/Cubical/Categories/NaturalTransformation/Base.agda index 9056e5b916..eb8b31290b 100644 --- a/Cubical/Categories/NaturalTransformation/Base.agda +++ b/Cubical/Categories/NaturalTransformation/Base.agda @@ -6,11 +6,12 @@ open import Cubical.Foundations.Univalence open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism renaming (iso to iIso) open import Cubical.Data.Sigma -open import Cubical.Categories.Category +open import Cubical.Categories.Category renaming (isIso to isIsoC) open import Cubical.Categories.Functor.Base open import Cubical.Categories.Functor.Properties open import Cubical.Categories.Commutativity -open import Cubical.Categories.Morphism renaming (isIso to isIsoC) +open import Cubical.Categories.Morphism +open import Cubical.Categories.Isomorphism private variable @@ -94,6 +95,18 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where syntax idTrans F = 1[ F ] + -- Natural isomorphism induced by path of functors + + pathToNatTrans : {F G : Functor C D} → F ≡ G → NatTrans F G + pathToNatTrans p .N-ob x = pathToIso {C = D} (λ i → p i .F-ob x) .fst + pathToNatTrans {F = F} {G = G} p .N-hom {x = x} {y = y} f = + pathToIso-Square {C = D} _ _ _ _ (λ i → p i .F-hom f) + + pathToNatIso : {F G : Functor C D} → F ≡ G → NatIso F G + pathToNatIso p .trans = pathToNatTrans p + pathToNatIso p .nIso x = pathToIso {C = D} _ .snd + + -- vertical sequencing seqTrans : {F G H : Functor C D} (α : NatTrans F G) (β : NatTrans G H) → NatTrans F H seqTrans α β .N-ob x = (α .N-ob x) ⋆ᴰ (β .N-ob x) diff --git a/Cubical/Categories/NaturalTransformation/Properties.agda b/Cubical/Categories/NaturalTransformation/Properties.agda index a79e1cc619..19deadb887 100644 --- a/Cubical/Categories/NaturalTransformation/Properties.agda +++ b/Cubical/Categories/NaturalTransformation/Properties.agda @@ -8,9 +8,9 @@ open import Cubical.Foundations.Univalence open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism renaming (iso to iIso) open import Cubical.Data.Sigma -open import Cubical.Categories.Category +open import Cubical.Categories.Category renaming (isIso to isIsoC) open import Cubical.Categories.Functor.Base -open import Cubical.Categories.Morphism renaming (isIso to isIsoC) +open import Cubical.Categories.Morphism open import Cubical.Categories.NaturalTransformation.Base private diff --git a/Cubical/Categories/Presheaf/Properties.agda b/Cubical/Categories/Presheaf/Properties.agda index 5c0833a1e6..bd518975c9 100644 --- a/Cubical/Categories/Presheaf/Properties.agda +++ b/Cubical/Categories/Presheaf/Properties.agda @@ -2,7 +2,7 @@ module Cubical.Categories.Presheaf.Properties where -open import Cubical.Categories.Category +open import Cubical.Categories.Category renaming (isIso to isIsoC) open import Cubical.Categories.NaturalTransformation open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Instances.Functors @@ -232,7 +232,6 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS)) module _ where open Iso - open Morphism renaming (isIso to isIsoC) -- the iso we need -- a type is isomorphic to the disjoint union of all its fibers typeSectionIso : ∀ {A B : Type ℓS} {isSetB : isSet B} → (ϕ : A → B) @@ -286,7 +285,6 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS)) module _ where open Iso - open Morphism renaming (isIso to isIsoC) -- the iso we deserve -- says that a type family at x is isomorphic to the fiber over x of that type family packaged up typeFiberIso : ∀ {ℓ ℓ'} {A : Type ℓ} {isSetA : isSet A} {x} (B : A → Type ℓ') diff --git a/Cubical/Categories/Yoneda.agda b/Cubical/Categories/Yoneda.agda index 150db9c4db..8ab9a0d0e4 100644 --- a/Cubical/Categories/Yoneda.agda +++ b/Cubical/Categories/Yoneda.agda @@ -177,3 +177,6 @@ module _ {C : Category ℓ ℓ} where hcomp (λ j → λ{ (i = i0) → ⋆IdL f j; (i = i1) → ⋆IdL g j}) (yo-yo-yo _ (p i)) + + isFullyFaithfulYO : isFullyFaithful YO + isFullyFaithfulYO = isFull+Faithful→isFullyFaithful {F = YO} isFullYO isFaithfulYO diff --git a/Cubical/Data/Sigma/Properties.agda b/Cubical/Data/Sigma/Properties.agda index bb62a50b25..312a4c2063 100644 --- a/Cubical/Data/Sigma/Properties.agda +++ b/Cubical/Data/Sigma/Properties.agda @@ -260,6 +260,16 @@ leftInv (Σ-cong-iso-snd isom) (x , y') = ΣPathP (refl , leftInv (isom x) y') Σ-cong' : (p : A ≡ A') → PathP (λ i → p i → Type ℓ') B B' → Σ A B ≡ Σ A' B' Σ-cong' p p' = cong₂ (λ (A : Type _) (B : A → Type _) → Σ A B) p p' +Σ-cong-equiv-prop : + (e : A ≃ A') + → ((x : A ) → isProp (B x)) + → ((x : A') → isProp (B' x)) + → ((x : A) → B x → B' (equivFun e x)) + → ((x : A) → B' (equivFun e x) → B x) + → Σ A B ≃ Σ A' B' +Σ-cong-equiv-prop e prop prop' prop→ prop← = + Σ-cong-equiv e (λ x → propBiimpl→Equiv (prop x) (prop' (equivFun e x)) (prop→ x) (prop← x)) + -- Alternative version for path in Σ-types, as in the HoTT book ΣPathTransport : (a b : Σ A B) → Type _ diff --git a/Cubical/Foundations/Equiv/Properties.agda b/Cubical/Foundations/Equiv/Properties.agda index 0c416d94c5..5f7b32325c 100644 --- a/Cubical/Foundations/Equiv/Properties.agda +++ b/Cubical/Foundations/Equiv/Properties.agda @@ -211,3 +211,16 @@ isEquiv[f∘equivFunA≃B]→isEquiv[f] f (g , gIsEquiv) f∘gIsEquiv = w' : isEquiv (g ∘ equivFun (invEquiv (_ , f∘gIsEquiv))) w' = (snd (compEquiv (invEquiv (_ , f∘gIsEquiv) ) (_ , gIsEquiv))) + +isEquiv[equivFunA≃B∘f]→isEquiv[f] : {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} + → (f : C → A) (A≃B : A ≃ B) + → isEquiv (equivFun A≃B ∘ f) + → isEquiv f +isEquiv[equivFunA≃B∘f]→isEquiv[f] f (g , gIsEquiv) g∘fIsEquiv = + composesToId→Equiv _ f w w' + where + w : equivFun (invEquiv (_ , g∘fIsEquiv)) ∘ g ∘ f ≡ idfun _ + w = (cong fst (invEquiv-is-rinv (_ , g∘fIsEquiv))) + + w' : isEquiv (equivFun (invEquiv (_ , g∘fIsEquiv)) ∘ g) + w' = snd (compEquiv (_ , gIsEquiv) (invEquiv (_ , g∘fIsEquiv))) From 45ef2a42c6fbd32180adecd0bd76f8ec7aef80be Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Sat, 4 Jun 2022 22:39:06 +0800 Subject: [PATCH 04/18] done --- .../Categories/Equivalence/Properties.agda | 67 ++++-- .../Equivalence/WeakEquivalence.agda | 31 ++- Cubical/Data/Sigma/Properties.agda | 8 + Cubical/Foundations/Equiv/Dependent.agda | 218 ++++++++++++++++++ Cubical/Foundations/Isomorphism.agda | 13 ++ 5 files changed, 294 insertions(+), 43 deletions(-) create mode 100644 Cubical/Foundations/Equiv/Dependent.agda diff --git a/Cubical/Categories/Equivalence/Properties.agda b/Cubical/Categories/Equivalence/Properties.agda index 059492bf3a..fc3cdae55c 100644 --- a/Cubical/Categories/Equivalence/Properties.agda +++ b/Cubical/Categories/Equivalence/Properties.agda @@ -5,6 +5,8 @@ module Cubical.Categories.Equivalence.Properties where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Equiv renaming (isEquiv to isEquivMap) +open import Cubical.Foundations.Equiv.Dependent +open import Cubical.Foundations.Isomorphism open import Cubical.Data.Sigma open import Cubical.Categories.Category open import Cubical.Categories.Functor @@ -17,7 +19,6 @@ open Category open Functor open NatIso open isIso -open NatTrans open isEquivalence private @@ -97,45 +98,61 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where isEquiv→Surj isE d = ∣ (isE .invFunc ⟅ d ⟆) , isIso→CatIso ((isE .ε .nIso) d) ∣₁ --- A fully-faithful functor that induces equivalences on objects is an equivalence - -Mor : (C : Category ℓC ℓC') → Type _ -Mor C = Σ[ x ∈ C .ob ] Σ[ y ∈ C .ob ] C [ x , y ] - -projMor : {C : Category ℓC ℓC'} → Mor C → C .ob × C .ob -projMor (x , y , _) = x , y +-- A fully-faithful functor that induces equivalence on objects is an equivalence module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} {F : Functor C D} where - F-Mor : Mor C → Mor D - F-Mor (x , y , f) = F .F-ob x , F .F-ob y , F .F-hom f - isFullyFaithful+isEquivF-ob→isEquiv : isFullyFaithful F → isEquivMap (F .F-ob) → isEquivalence F isFullyFaithful+isEquivF-ob→isEquiv fullfaith isequiv = w where - isEquivF-Mor : isEquivMap F-Mor - isEquivF-Mor = {!!} + open Iso + open IsoOver + + MorC : C .ob × C .ob → Type _ + MorC (x , y) = C [ x , y ] + + MorD : D .ob × D .ob → Type _ + MorD (x , y) = D [ x , y ] + + F-Mor : ((x , y) : C .ob × C .ob) → C [ x , y ] → D [ F .F-ob x , F .F-ob y ] + F-Mor _ = F .F-hom - w-inv-ob : D .ob → C .ob - w-inv-ob = invIsEq isequiv + equiv-ob² : C .ob × C .ob ≃ D .ob × D .ob + equiv-ob² = ≃-× (_ , isequiv) (_ , isequiv) - w-hom-path : {x y : D .ob}(f : D [ x , y ]) - → (i : I) → D [ secIsEq isequiv x (~ i) , secIsEq isequiv y (~ i) ] - w-hom-path {x = x} {y = y} f i = - transport-filler (λ i → D [ secIsEq isequiv x (~ i) , secIsEq isequiv y (~ i) ]) f i + iso-ob = equivToIso (_ , isequiv) + iso-hom = equivOver→IsoOver {P = MorC} {Q = MorD} equiv-ob² F-Mor (λ (x , y) → fullfaith x y) w-inv : Functor D C - w-inv .F-ob = invIsEq isequiv - w-inv .F-hom f = invIsEq (fullfaith _ _) (w-hom-path f i1) - w-inv .F-id = {!!} - w-inv .F-seq = {!!} + w-inv .F-ob = iso-ob .inv + w-inv .F-hom = iso-hom .inv _ + w-inv .F-id {x = x} = isFullyFaithful→Faithful {F = F} fullfaith _ _ _ _ (p ∙ sym (F .F-id)) + where + p : _ + p i = + comp + (λ j → D [ iso-ob .rightInv x (~ j) , iso-ob .rightInv x (~ j) ]) + (λ j → λ + { (i = i0) → iso-hom .rightInv _ (D .id {x = x}) (~ j) + ; (i = i1) → D .id {x = iso-ob .rightInv x (~ j)} }) + (D .id {x = x}) + w-inv .F-seq {x = x} {z = z} f g = isFullyFaithful→Faithful {F = F} fullfaith _ _ _ _ (p ∙ sym (F .F-seq _ _)) + where + p : _ + p i = + comp + (λ j → D [ iso-ob .rightInv x (~ j) , iso-ob .rightInv z (~ j) ]) + (λ j → λ + { (i = i0) → iso-hom .rightInv _ (f ⋆⟨ D ⟩ g) (~ j) + ; (i = i1) → iso-hom .rightInv _ f (~ j) ⋆⟨ D ⟩ iso-hom .rightInv _ g (~ j) }) + (f ⋆⟨ D ⟩ g) w-η-path : 𝟙⟨ C ⟩ ≡ w-inv ∘F F - w-η-path = Functor≡ (λ x → sym (retIsEq isequiv x)) {!!} + w-η-path = Functor≡ (λ x → sym (retIsEq isequiv x)) (λ {x} {y} f → (λ i → iso-hom .leftInv (x , y) f (~ i))) w-ε-path : F ∘F w-inv ≡ 𝟙⟨ D ⟩ - w-ε-path = Functor≡ (λ x → secIsEq isequiv x) {!!} + w-ε-path = Functor≡ (λ x → secIsEq isequiv x) (λ {x} {y} f i → iso-hom .rightInv (x , y) f i) w : isEquivalence F w .invFunc = w-inv diff --git a/Cubical/Categories/Equivalence/WeakEquivalence.agda b/Cubical/Categories/Equivalence/WeakEquivalence.agda index eb4e8718c5..78be83e07d 100644 --- a/Cubical/Categories/Equivalence/WeakEquivalence.agda +++ b/Cubical/Categories/Equivalence/WeakEquivalence.agda @@ -6,22 +6,9 @@ open import Cubical.Foundations.Prelude open import Cubical.Foundations.Equiv renaming (isEquiv to isEquivMap) open import Cubical.Functions.Surjection -open import Cubical.Functions.Embedding -open import Cubical.Data.Sigma open import Cubical.Categories.Category open import Cubical.Categories.Functor -open import Cubical.Categories.NaturalTransformation -open import Cubical.Categories.Morphism open import Cubical.Categories.Equivalence -open import Cubical.HITs.PropositionalTruncation.Base - -open Category -open Functor -open NatIso -open isIso -open NatTrans -open isEquivalence -open _≃ᶜ_ private variable @@ -30,6 +17,11 @@ private D : Category ℓD ℓD' F : Functor C D +open Functor + + +-- Weak equivalences of categories, +-- namely fully-faithful and essentially surjective functors record isWeakEquivalence {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (func : Functor C D) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where @@ -45,16 +37,20 @@ record WeakEquivalence (C : Category ℓC ℓC') (D : Category ℓD ℓD') func : Functor C D isWeakEquiv : isWeakEquivalence func - open isWeakEquivalence open WeakEquivalence +-- Equivalence is always weak equivalence. + isEquiv→isWeakEquiv : isEquivalence F → isWeakEquivalence F isEquiv→isWeakEquiv isequiv .fullfaith = isEquiv→FullyFaithful isequiv isEquiv→isWeakEquiv isequiv .esssurj = isEquiv→Surj isequiv +-- Weak equivalence between univalent categories is equivalence, +-- in other words, they admit explicit inverse functor. + module _ (isUnivC : isUnivalent C) (isUnivD : isUnivalent D) @@ -62,12 +58,11 @@ module _ open isUnivalent - 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) , isSurj→isSurj-ob isUnivD {F = F} (is-w-equiv .esssurj)) - - isWeakEquiv→isEquiv : isWeakEquivalence F → isEquivalence F - isWeakEquiv→isEquiv is-w-equiv = {!!} + isWeakEquiv→isEquiv : {F : Functor C D} → isWeakEquivalence F → isEquivalence F + isWeakEquiv→isEquiv is-w-equiv = + isFullyFaithful+isEquivF-ob→isEquiv (is-w-equiv .fullfaith) (isEquivF-ob is-w-equiv) diff --git a/Cubical/Data/Sigma/Properties.agda b/Cubical/Data/Sigma/Properties.agda index 312a4c2063..859369e619 100644 --- a/Cubical/Data/Sigma/Properties.agda +++ b/Cubical/Data/Sigma/Properties.agda @@ -385,6 +385,14 @@ Iso.inv (prodIso iAC iBD) (c , d) = (Iso.inv iAC c) , Iso.inv iBD d Iso.rightInv (prodIso iAC iBD) (c , d) = ΣPathP ((Iso.rightInv iAC c) , (Iso.rightInv iBD d)) Iso.leftInv (prodIso iAC iBD) (a , b) = ΣPathP ((Iso.leftInv iAC a) , (Iso.leftInv iBD b)) +prodEquivToIso : ∀ {ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {D : Type ℓ'''} + → (e : A ≃ C)(e' : B ≃ D) + → prodIso (equivToIso e) (equivToIso e') ≡ equivToIso (≃-× e e') +Iso.fun (prodEquivToIso e e' i) = Iso.fun (equivToIso (≃-× e e')) +Iso.inv (prodEquivToIso e e' i) = Iso.inv (equivToIso (≃-× e e')) +Iso.rightInv (prodEquivToIso e e' i) = Iso.rightInv (equivToIso (≃-× e e')) +Iso.leftInv (prodEquivToIso e e' i) = Iso.leftInv (equivToIso (≃-× e e')) + toProdIso : {B C : A → Type ℓ} → Iso ((a : A) → B a × C a) (((a : A) → B a) × ((a : A) → C a)) Iso.fun toProdIso = λ f → (λ a → fst (f a)) , (λ a → snd (f a)) diff --git a/Cubical/Foundations/Equiv/Dependent.agda b/Cubical/Foundations/Equiv/Dependent.agda new file mode 100644 index 0000000000..3b0f698645 --- /dev/null +++ b/Cubical/Foundations/Equiv/Dependent.agda @@ -0,0 +1,218 @@ +{- + +Dependent version of isomorphisms and equivalences + +-} +{-# OPTIONS --safe #-} +module Cubical.Foundations.Equiv.Dependent where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Equiv.HalfAdjoint +open import Cubical.Foundations.Isomorphism + +private + variable + ℓ ℓ' ℓ'' ℓ''' : Level + A : Type ℓ + B : Type ℓ' + P : A → Type ℓ'' + Q : B → Type ℓ''' + + +-- Relative version of maps and their composition + +mapOver : + (f : A → B) + (P : A → Type ℓ'')(Q : B → Type ℓ''') + → Type _ +mapOver {A = A} f P Q = (a : A) → P a → Q (f a) + +compMapOver : + {ℓA ℓB ℓC ℓP ℓQ ℓR : Level} + {A : Type ℓA}{B : Type ℓB}{C : Type ℓC} + {P : A → Type ℓP}{Q : B → Type ℓQ}{R : C → Type ℓR} + {f : A → B}{g : B → C} + → mapOver f P Q → mapOver g Q R + → mapOver (g ∘ f) P R +compMapOver f g _ p = g _ (f _ p) + + +-- Fiberwise equivalence + +isEquivOver : + {f : A → B} + (F : mapOver f P Q) + → Type _ +isEquivOver {A = A} F = (a : A) → isEquiv (F a) + + +-- Relative version of section and retract + +sectionOver : + {f : A → B}{g : B → A} + (sec : section f g) + (F : mapOver f P Q)(G : mapOver g Q P) + → Type _ +sectionOver {B = B} {Q = Q} sec F G = + (b : B)(q : Q b) → PathP (λ i → Q (sec b i)) (F _ (G _ q)) q + +retractOver : + {f : A → B}{g : B → A} + (ret : retract f g) + (F : mapOver f P Q)(G : mapOver g Q P) + → Type _ +retractOver {A = A} {P = P} ret F G = + (a : A)(p : P a) → PathP (λ i → P (ret a i)) (G _ (F _ p)) p + + +-- Relative version of isomorphism + +open Iso + +record IsoOver {ℓ ℓ'} {A : Type ℓ}{B : Type ℓ'} + (isom : Iso A B)(P : A → Type ℓ'')(Q : B → Type ℓ''') + : Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓ'' ℓ''')) where + no-eta-equality + constructor isoover + field + fun : mapOver (isom .fun) P Q + inv : mapOver (isom .inv) Q P + rightInv : sectionOver (isom .rightInv) fun inv + leftInv : retractOver (isom .leftInv ) fun inv + +record isIsoOver {ℓ ℓ'} {A : Type ℓ}{B : Type ℓ'} + (isom : Iso A B)(P : A → Type ℓ'')(Q : B → Type ℓ''') + (fun : mapOver (isom .fun) P Q) + : Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓ'' ℓ''')) where + no-eta-equality + constructor isisoover + field + inv : mapOver (isom .inv) Q P + rightInv : sectionOver (isom .rightInv) fun inv + leftInv : retractOver (isom .leftInv ) fun inv + +open IsoOver +open isIsoOver + + +isIsoOver→IsoOver : + {isom : Iso A B} + {fun : mapOver (isom .fun) P Q} + → isIsoOver isom P Q fun + → IsoOver isom P Q +isIsoOver→IsoOver {fun = fun} isom .fun = fun +isIsoOver→IsoOver {fun = fun} isom .inv = isom .inv +isIsoOver→IsoOver {fun = fun} isom .rightInv = isom .rightInv +isIsoOver→IsoOver {fun = fun} isom .leftInv = isom .leftInv + +IsoOver→isIsoOver : + {isom : Iso A B} + → (isom' : IsoOver isom P Q) + → isIsoOver isom P Q (isom' .fun) +IsoOver→isIsoOver isom .inv = isom .inv +IsoOver→isIsoOver isom .rightInv = isom .rightInv +IsoOver→isIsoOver isom .leftInv = isom .leftInv + + +compIsoOver : + {ℓA ℓB ℓC ℓP ℓQ ℓR : Level} + {A : Type ℓA}{B : Type ℓB}{C : Type ℓC} + {P : A → Type ℓP}{Q : B → Type ℓQ}{R : C → Type ℓR} + {isom₁ : Iso A B}{isom₂ : Iso B C} + → IsoOver isom₁ P Q → IsoOver isom₂ Q R + → IsoOver (compIso isom₁ isom₂) P R +compIsoOver {A = A} {B} {C} {P} {Q} {R} {isom₁} {isom₂} isoover₁ isoover₂ = w + where + w : IsoOver _ _ _ + w .fun _ = isoover₂ .fun _ ∘ isoover₁ .fun _ + w .inv _ = isoover₁ .inv _ ∘ isoover₂ .inv _ + w .rightInv b q i = + comp + (λ j → R (compPath-filler (cong (isom₂ .fun) (isom₁ .rightInv _)) (isom₂ .rightInv b) j i)) + (λ j → λ + { (i = i0) → w .fun _ (w .inv _ q) + ; (i = i1) → isoover₂ .rightInv _ q j }) + (isoover₂ .fun _ (isoover₁ .rightInv _ (isoover₂ .inv _ q) i)) + w .leftInv a p i = + comp + (λ j → P (compPath-filler (cong (isom₁ .inv) (isom₂ .leftInv _)) (isom₁ .leftInv a) j i)) + (λ j → λ + { (i = i0) → w .inv _ (w .fun _ p) + ; (i = i1) → isoover₁ .leftInv _ p j }) + (isoover₁ .inv _ (isoover₂ .leftInv _ (isoover₁ .fun _ p) i)) + + +-- Special cases + +fiberIso→IsoOver : + {ℓA ℓP ℓQ : Level} + {A : Type ℓA} + {P : A → Type ℓP}{Q : A → Type ℓQ} + → ((a : A) → Iso (P a) (Q a)) + → IsoOver idIso P Q +fiberIso→IsoOver isom .fun a = isom a .fun +fiberIso→IsoOver isom .inv b = isom b .inv +fiberIso→IsoOver isom .rightInv b = isom b .rightInv +fiberIso→IsoOver isom .leftInv a = isom a .leftInv + +-- Only half-adjoint equivalence can be lifted. +-- This is another clue that HAE is more natural than isomorphism. + +open isHAEquiv + +pullbackIsoOver : + {ℓA ℓB ℓP : Level} + {A : Type ℓA}{B : Type ℓB} + {P : B → Type ℓP} + (f : A → B) + (hae : isHAEquiv f) + → IsoOver (isHAEquiv→Iso hae) (P ∘ f) P +pullbackIsoOver {A = A} {B} {P} f hae = w + where + isom = isHAEquiv→Iso hae + + w : IsoOver _ _ _ + w .fun a = idfun _ + w .inv b = subst P (sym (isom .rightInv b)) + w .rightInv b p i = subst-filler P (sym (isom .rightInv b)) p (~ i) + w .leftInv a p i = + comp + (λ j → P (hae .com a (~ j) i)) + (λ j → λ + { (i = i0) → w .inv _ (w .fun _ p) + ; (i = i1) → p }) + (w .rightInv _ p i) + + +-- Lifting isomorphism of bases to isomorphism of families + +-- Since there is no regularity for transport (also no-eta-equality), +-- we have to fix one field manually to make it invariant under transportation. + +liftHAEToIsoOver : + (f : A → B) + (hae : isHAEquiv f) + → ((a : A) → Iso (P a) (Q (f a))) + → IsoOver (isHAEquiv→Iso hae) P Q +liftHAEToIsoOver {P = P} {Q = Q} f hae isom = + isIsoOver→IsoOver + (transport (λ i → isIsoOver (compIsoIdL (isHAEquiv→Iso hae) i) P Q (λ a x → isom a .fun x)) + (IsoOver→isIsoOver (compIsoOver (fiberIso→IsoOver isom) (pullbackIsoOver f hae)))) + +equivOver→IsoOver : + (e : A ≃ B) + (f : mapOver (e .fst) P Q) + → isEquivOver {P = P} {Q = Q} f + → IsoOver (equivToIso e) P Q +equivOver→IsoOver {P = P} {Q = Q} e f equiv = w + where + isom = liftHAEToIsoOver _ (equiv→HAEquiv e .snd) (λ a → equivToIso (_ , equiv a)) + + -- no-eta-equality for Iso, so we have to fill in fields manually + w : IsoOver (equivToIso e) P Q + w .fun = isom .fun + w .inv = isom .inv + w .rightInv = isom .rightInv + w .leftInv = isom .leftInv diff --git a/Cubical/Foundations/Isomorphism.agda b/Cubical/Foundations/Isomorphism.agda index 2d940f11ed..9461bce2a6 100644 --- a/Cubical/Foundations/Isomorphism.agda +++ b/Cubical/Foundations/Isomorphism.agda @@ -13,6 +13,7 @@ module Cubical.Foundations.Isomorphism where open import Cubical.Core.Everything open import Cubical.Foundations.Prelude +open import Cubical.Foundations.GroupoidLaws open import Cubical.Foundations.Function open import Cubical.Foundations.Equiv.Base @@ -135,6 +136,18 @@ inv idIso = idfun _ rightInv idIso _ = refl leftInv idIso _ = refl +compIsoIdL : (isom : Iso A B) → compIso idIso isom ≡ isom +fun (compIsoIdL isom i) = fun isom +inv (compIsoIdL isom i) = inv isom +rightInv (compIsoIdL isom i) b = lUnit (isom .rightInv b) (~ i) +leftInv (compIsoIdL isom i) a = rUnit (isom .leftInv a) (~ i) + +compIsoIdR : (isom : Iso A B) → compIso isom idIso ≡ isom +fun (compIsoIdR isom i) = fun isom +inv (compIsoIdR isom i) = inv isom +rightInv (compIsoIdR isom i) b = rUnit (isom .rightInv b) (~ i) +leftInv (compIsoIdR isom i) a = lUnit (isom .leftInv a) (~ i) + LiftIso : Iso A (Lift {i = ℓ} {j = ℓ'} A) fun LiftIso = lift inv LiftIso = lower From 0e7b12c373e2c6dcd280ee9e94f5ad4b35b6aa6c Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Sat, 4 Jun 2022 22:46:40 +0800 Subject: [PATCH 05/18] comment --- Cubical/Categories/Equivalence/WeakEquivalence.agda | 5 +++++ Cubical/Foundations/Equiv/Dependent.agda | 6 ++++++ 2 files changed, 11 insertions(+) diff --git a/Cubical/Categories/Equivalence/WeakEquivalence.agda b/Cubical/Categories/Equivalence/WeakEquivalence.agda index 78be83e07d..974b6bcbd8 100644 --- a/Cubical/Categories/Equivalence/WeakEquivalence.agda +++ b/Cubical/Categories/Equivalence/WeakEquivalence.agda @@ -1,3 +1,8 @@ +{- + +Weak Equivalence between Categories + +-} {-# OPTIONS --safe #-} module Cubical.Categories.Equivalence.WeakEquivalence where diff --git a/Cubical/Foundations/Equiv/Dependent.agda b/Cubical/Foundations/Equiv/Dependent.agda index 3b0f698645..cb9bc651f8 100644 --- a/Cubical/Foundations/Equiv/Dependent.agda +++ b/Cubical/Foundations/Equiv/Dependent.agda @@ -2,6 +2,12 @@ Dependent version of isomorphisms and equivalences +Extremely useful if one wants to construct explicit isomorphisms between record types +with fields dependent on each other. + +This can be generalize in inumerable ways. +Maybe one day someone will find a common scheme and then computer could automatically generate them. + -} {-# OPTIONS --safe #-} module Cubical.Foundations.Equiv.Dependent where From ad7ec28709e4031b25017c84da0a28ced984f24e Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Sat, 4 Jun 2022 22:55:33 +0800 Subject: [PATCH 06/18] everything --- Cubical/Foundations/Everything.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/Cubical/Foundations/Everything.agda b/Cubical/Foundations/Everything.agda index 48d7e33aa3..798dd6deb0 100644 --- a/Cubical/Foundations/Everything.agda +++ b/Cubical/Foundations/Everything.agda @@ -36,6 +36,7 @@ open import Cubical.Foundations.Equiv.Fiberwise open import Cubical.Foundations.Equiv.PathSplit public open import Cubical.Foundations.Equiv.BiInvertible public open import Cubical.Foundations.Equiv.HalfAdjoint +open import Cubical.Foundations.Equiv.Dependent open import Cubical.Foundations.HLevels public open import Cubical.Foundations.Path public open import Cubical.Foundations.Pointed public From 9795d18f82b54636aedb5358d426e1cec5d6519b Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Sat, 4 Jun 2022 23:23:55 +0800 Subject: [PATCH 07/18] fix --- Cubical/Categories/Limits/RightKan.agda | 4 ++-- Cubical/Categories/Presheaf/Properties.agda | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Cubical/Categories/Limits/RightKan.agda b/Cubical/Categories/Limits/RightKan.agda index 7dd85972e3..af382b0c28 100644 --- a/Cubical/Categories/Limits/RightKan.agda +++ b/Cubical/Categories/Limits/RightKan.agda @@ -7,8 +7,8 @@ open import Cubical.Foundations.HLevels open import Cubical.Foundations.Powerset open import Cubical.Data.Sigma -open import Cubical.Categories.Category -open import Cubical.Categories.Morphism renaming (isIso to isIsoC) +open import Cubical.Categories.Category renaming (isIso to isIsoC) +open import Cubical.Categories.Morphism open import Cubical.Categories.Functor open import Cubical.Categories.NaturalTransformation open import Cubical.Categories.Limits.Limits diff --git a/Cubical/Categories/Presheaf/Properties.agda b/Cubical/Categories/Presheaf/Properties.agda index bd518975c9..623141cf46 100644 --- a/Cubical/Categories/Presheaf/Properties.agda +++ b/Cubical/Categories/Presheaf/Properties.agda @@ -276,7 +276,7 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS)) where isIsoCf : ∀ (c : C .ob) → isIsoC _ (ηTrans .N-ob sob .S-hom ⟦ c ⟧) - isIsoCf c = CatIso→isIso (Iso→CatIso (typeSectionIso {isSetB = snd (F ⟅ c ⟆)} (ϕ ⟦ c ⟧))) + isIsoCf c = Morphism.CatIso→isIso (Iso→CatIso (typeSectionIso {isSetB = snd (F ⟅ c ⟆)} (ϕ ⟦ c ⟧))) -- ======================================== @@ -373,7 +373,7 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS)) where isIsoC' : ∀ (cx : (∫ᴾ F) .ob) → isIsoC (SET _) ((εTrans ⟦ P ⟧) ⟦ cx ⟧) - isIsoC' cx@(c , _) = CatIso→isIso (Iso→CatIso (invIso (typeFiberIso {isSetA = snd (F ⟅ c ⟆)} _))) + isIsoC' cx@(c , _) = Morphism.CatIso→isIso (Iso→CatIso (invIso (typeFiberIso {isSetA = snd (F ⟅ c ⟆)} _))) -- putting it all together From 20c7e5ddb2b32045b8df6d0a5837a781cb90b800 Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Sun, 5 Jun 2022 01:45:36 +0800 Subject: [PATCH 08/18] a bit --- Cubical/Categories/Category/Base.agda | 3 +- Cubical/Categories/Isomorphism.agda | 43 ++++++++++++++++++- .../NaturalTransformation/Base.agda | 2 +- .../NaturalTransformation/Properties.agda | 19 ++++++++ 4 files changed, 62 insertions(+), 5 deletions(-) diff --git a/Cubical/Categories/Category/Base.agda b/Cubical/Categories/Category/Base.agda index 61cad2fc44..119577a9ca 100644 --- a/Cubical/Categories/Category/Base.agda +++ b/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 _ _)) diff --git a/Cubical/Categories/Isomorphism.agda b/Cubical/Categories/Isomorphism.agda index f411ccc015..160a698838 100644 --- a/Cubical/Categories/Isomorphism.agda +++ b/Cubical/Categories/Isomorphism.agda @@ -2,6 +2,7 @@ module Cubical.Categories.Isomorphism where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv open import Cubical.Foundations.GroupoidLaws open import Cubical.Foundations.Function open import Cubical.Categories.Category @@ -53,12 +54,12 @@ module _ {C : Category ℓC ℓC'} where ∙ (λ i → ⋆Iso (pathToIso-refl (~ i)) (pathToIso refl)) - pathToIso-Square : {x y z w : ob} + pathToIso-Comm : {x y z w : ob} → (p : x ≡ y)(q : z ≡ w) → (f : Hom[ x , z ])(g : Hom[ y , w ]) → PathP (λ i → Hom[ p i , q i ]) f g → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} p .fst ⋆ g - pathToIso-Square {x = x} {z = z} p q = + pathToIso-Comm {x = x} {z = z} p q = J (λ y p → (w : ob)(q : z ≡ w)(f : Hom[ x , z ])(g : Hom[ y , w ]) → PathP (λ i → Hom[ p i , q i ]) f g @@ -75,6 +76,44 @@ module _ {C : Category ℓC ℓC'} where ∙ ⋆IdR _ ∙ p ∙ sym (⋆IdL _) ∙ (λ i → pathToIso-refl {C = C} (~ i) .fst ⋆ g) + pathToIso-Square : {x y z w : ob} + → (p : x ≡ y)(q : z ≡ w) + → (f : Hom[ x , z ])(g : Hom[ y , w ]) + → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} p .fst ⋆ g + → PathP (λ i → Hom[ p i , q i ]) f g + pathToIso-Square {x = x} {z = z} p q = + J (λ y p → + (w : ob)(q : z ≡ w)(f : Hom[ x , z ])(g : Hom[ y , w ]) + → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} p .fst ⋆ g + → PathP (λ i → Hom[ p i , q i ]) f g) + (λ _ → J (λ w q → + (f : Hom[ x , z ])(g : Hom[ x , w ]) + → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} refl .fst ⋆ g + → PathP (λ i → Hom[ x , q i ]) f g) + sqr-refl) p _ q + where + sqr-refl : {x z : ob} → (f g : Hom[ x , z ]) + → f ⋆ pathToIso {C = C} refl .fst ≡ pathToIso {C = C} refl .fst ⋆ g + → f ≡ g + sqr-refl f g p = sym (⋆IdR _) + ∙ (λ i → f ⋆ pathToIso-refl {C = C} (~ i) .fst) + ∙ p + ∙ (λ i → pathToIso-refl {C = C} i .fst ⋆ g) + ∙ ⋆IdL _ + + module _ (isUnivC : isUnivalent C) where + + open isUnivalent isUnivC + + isoToPath-Square : {x y z w : ob} + → (p : CatIso C x y)(q : CatIso C z w) + → (f : Hom[ x , z ])(g : Hom[ y , w ]) + → f ⋆ q .fst ≡ p .fst ⋆ g + → PathP (λ i → Hom[ CatIsoToPath p i , CatIsoToPath q i ]) f g + isoToPath-Square p q f g comm = + pathToIso-Square (CatIsoToPath p) (CatIsoToPath q) _ _ + ((λ i → f ⋆ secEq (univEquiv _ _) q i .fst) ∙ comm ∙ (λ i → secEq (univEquiv _ _) p (~ i) .fst ⋆ g)) + module _ {C : Category ℓC ℓC'} where diff --git a/Cubical/Categories/NaturalTransformation/Base.agda b/Cubical/Categories/NaturalTransformation/Base.agda index eb8b31290b..0893bc1d3c 100644 --- a/Cubical/Categories/NaturalTransformation/Base.agda +++ b/Cubical/Categories/NaturalTransformation/Base.agda @@ -100,7 +100,7 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where pathToNatTrans : {F G : Functor C D} → F ≡ G → NatTrans F G pathToNatTrans p .N-ob x = pathToIso {C = D} (λ i → p i .F-ob x) .fst pathToNatTrans {F = F} {G = G} p .N-hom {x = x} {y = y} f = - pathToIso-Square {C = D} _ _ _ _ (λ i → p i .F-hom f) + pathToIso-Comm {C = D} _ _ _ _ (λ i → p i .F-hom f) pathToNatIso : {F G : Functor C D} → F ≡ G → NatIso F G pathToNatIso p .trans = pathToNatTrans p diff --git a/Cubical/Categories/NaturalTransformation/Properties.agda b/Cubical/Categories/NaturalTransformation/Properties.agda index 19deadb887..df45592e2d 100644 --- a/Cubical/Categories/NaturalTransformation/Properties.agda +++ b/Cubical/Categories/NaturalTransformation/Properties.agda @@ -11,6 +11,7 @@ open import Cubical.Data.Sigma open import Cubical.Categories.Category renaming (isIso to isIsoC) open import Cubical.Categories.Functor.Base open import Cubical.Categories.Morphism +open import Cubical.Categories.Isomorphism open import Cubical.Categories.NaturalTransformation.Base private @@ -100,3 +101,21 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where isSetRetract (fun NatTransIsoΣ) (inv NatTransIsoΣ) (leftInv NatTransIsoΣ) (isSetΣSndProp (isSetΠ (λ _ → isSetHom D)) (λ _ → isPropImplicitΠ2 (λ _ _ → isPropΠ (λ _ → isSetHom D _ _)))) + + +module _ + {C : Category ℓC ℓC'} + {D : Category ℓD ℓD'}(isUnivD : isUnivalent D) where + + open isUnivalent isUnivD + + NatIsoToPath : {F G : Functor C D} → NatIso F G → F ≡ G + NatIsoToPath natiso i .F-ob x = CatIsoToPath (_ , natiso .nIso x) i + NatIsoToPath natiso i .F-hom f = isoToPath-Square isUnivD _ _ _ _ (natiso .trans .N-hom f) i + NatIsoToPath {F = F} {G = G} natiso i .F-id j = + isSet→SquareP (λ i j → D .isSetHom {x = NatIsoToPath natiso i .F-ob _} {y = NatIsoToPath natiso i .F-ob _}) + (F .F-id) (G .F-id) (λ i → NatIsoToPath natiso i .F-hom (C .id)) (λ i → D .id) i j + NatIsoToPath {F = F} {G = G} natiso i .F-seq f g j = + isSet→SquareP (λ i j → D .isSetHom {x = NatIsoToPath natiso i .F-ob _} {y = NatIsoToPath natiso i .F-ob _}) + (F .F-seq f g) (G .F-seq f g) (λ i → NatIsoToPath natiso i .F-hom (f ⋆⟨ C ⟩ g)) + (λ i → (NatIsoToPath natiso i .F-hom f) ⋆⟨ D ⟩ (NatIsoToPath natiso i .F-hom g)) i j From 135eec3bd48207722a79d6a69549529a977ad07e Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Tue, 7 Jun 2022 17:21:55 +0800 Subject: [PATCH 09/18] natIso is path --- Cubical/Categories/Functor/Base.agda | 24 +++++++++++++++++ Cubical/Categories/Isomorphism.agda | 27 +++++++------------ .../NaturalTransformation/Base.agda | 9 ++++++- .../NaturalTransformation/Properties.agda | 26 ++++++++++-------- Cubical/Foundations/Prelude.agda | 17 ++++++++++++ 5 files changed, 73 insertions(+), 30 deletions(-) diff --git a/Cubical/Categories/Functor/Base.agda b/Cubical/Categories/Functor/Base.agda index d3aa9eb819..12a7fd0491 100644 --- a/Cubical/Categories/Functor/Base.agda +++ b/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 diff --git a/Cubical/Categories/Isomorphism.agda b/Cubical/Categories/Isomorphism.agda index 160a698838..06c46539c9 100644 --- a/Cubical/Categories/Isomorphism.agda +++ b/Cubical/Categories/Isomorphism.agda @@ -45,8 +45,7 @@ module _ {C : Category ℓC ℓC'} where pathToIso-∙ : {x y z : ob}(p : x ≡ y)(q : y ≡ z) → pathToIso (p ∙ q) ≡ ⋆Iso (pathToIso p) (pathToIso q) - pathToIso-∙ p q = J (λ y p → (z : ob)(q : y ≡ z) → pathToIso (p ∙ q) ≡ ⋆Iso (pathToIso p) (pathToIso q)) - (λ _ q → J (λ z q → pathToIso (refl ∙ q) ≡ ⋆Iso (pathToIso refl) (pathToIso q)) pathToIso-∙-refl q) p _ q + pathToIso-∙ p q = J2 (λ y p z q → pathToIso (p ∙ q) ≡ ⋆Iso (pathToIso p) (pathToIso q)) pathToIso-∙-refl p q where pathToIso-∙-refl : {x : ob} → pathToIso {x = x} (refl ∙ refl) ≡ ⋆Iso (pathToIso refl) (pathToIso refl) pathToIso-∙-refl = cong pathToIso (sym compPathRefl) @@ -60,17 +59,13 @@ module _ {C : Category ℓC ℓC'} where → PathP (λ i → Hom[ p i , q i ]) f g → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} p .fst ⋆ g pathToIso-Comm {x = x} {z = z} p q = - J (λ y p → - (w : ob)(q : z ≡ w)(f : Hom[ x , z ])(g : Hom[ y , w ]) + J2 (λ y p w q → + (f : Hom[ x , z ])(g : Hom[ y , w ]) → PathP (λ i → Hom[ p i , q i ]) f g → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} p .fst ⋆ g) - (λ _ → J (λ w q → - (f : Hom[ x , z ])(g : Hom[ x , w ]) - → PathP (λ i → Hom[ x , q i ]) f g - → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} refl .fst ⋆ g) - sqr-refl) p _ q + sqr-refl p q where - sqr-refl : {x z : ob} → (f g : Hom[ x , z ]) → f ≡ g + sqr-refl : (f g : Hom[ x , z ]) → f ≡ g → f ⋆ pathToIso {C = C} refl .fst ≡ pathToIso {C = C} refl .fst ⋆ g sqr-refl f g p = (λ i → f ⋆ pathToIso-refl {C = C} i .fst) ∙ ⋆IdR _ ∙ p ∙ sym (⋆IdL _) @@ -82,17 +77,13 @@ module _ {C : Category ℓC ℓC'} where → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} p .fst ⋆ g → PathP (λ i → Hom[ p i , q i ]) f g pathToIso-Square {x = x} {z = z} p q = - J (λ y p → - (w : ob)(q : z ≡ w)(f : Hom[ x , z ])(g : Hom[ y , w ]) + J2 (λ y p w q → + (f : Hom[ x , z ])(g : Hom[ y , w ]) → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} p .fst ⋆ g → PathP (λ i → Hom[ p i , q i ]) f g) - (λ _ → J (λ w q → - (f : Hom[ x , z ])(g : Hom[ x , w ]) - → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} refl .fst ⋆ g - → PathP (λ i → Hom[ x , q i ]) f g) - sqr-refl) p _ q + sqr-refl p q where - sqr-refl : {x z : ob} → (f g : Hom[ x , z ]) + sqr-refl : (f g : Hom[ x , z ]) → f ⋆ pathToIso {C = C} refl .fst ≡ pathToIso {C = C} refl .fst ⋆ g → f ≡ g sqr-refl f g p = sym (⋆IdR _) diff --git a/Cubical/Categories/NaturalTransformation/Base.agda b/Cubical/Categories/NaturalTransformation/Base.agda index 0893bc1d3c..a60817a41d 100644 --- a/Cubical/Categories/NaturalTransformation/Base.agda +++ b/Cubical/Categories/NaturalTransformation/Base.agda @@ -94,7 +94,6 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where syntax idTrans F = 1[ F ] - -- Natural isomorphism induced by path of functors pathToNatTrans : {F G : Functor C D} → F ≡ G → NatTrans F G @@ -197,6 +196,14 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where (α .N-hom f) (β .N-hom f) rem = toPathP (D .isSetHom _ _ _ _) + + -- `constructor` for path of natural isomorphisms + NatIso≡ : {F G : Functor C D}{f g : NatIso F G} → f .trans .N-ob ≡ g .trans .N-ob → f ≡ g + NatIso≡ {f = f} {g} p i .trans = makeNatTransPath {α = f .trans} {β = g .trans} p i + NatIso≡ {f = f} {g} p i .nIso x = + isProp→PathP (λ i → isPropIsIso (NatIso≡ {f = f} {g} p i .trans .N-ob x)) (f .nIso _) (g .nIso _) i + + module _ {F F' G G' : Functor C D} {α : NatTrans F G} {β : NatTrans F' G'} where open Category open Functor diff --git a/Cubical/Categories/NaturalTransformation/Properties.agda b/Cubical/Categories/NaturalTransformation/Properties.agda index df45592e2d..dd5902eb1f 100644 --- a/Cubical/Categories/NaturalTransformation/Properties.agda +++ b/Cubical/Categories/NaturalTransformation/Properties.agda @@ -4,6 +4,7 @@ module Cubical.Categories.NaturalTransformation.Properties where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv open import Cubical.Foundations.Univalence open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism renaming (iso to iIso) @@ -103,19 +104,22 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where (λ _ → isPropImplicitΠ2 (λ _ _ → isPropΠ (λ _ → isSetHom D _ _)))) +-- Natural isomorphism is equivalent to path if the target category is univalent. + module _ {C : Category ℓC ℓC'} - {D : Category ℓD ℓD'}(isUnivD : isUnivalent D) where + {D : Category ℓD ℓD'}(isUnivD : isUnivalent D) + {F G : Functor C D} where open isUnivalent isUnivD - NatIsoToPath : {F G : Functor C D} → NatIso F G → F ≡ G - NatIsoToPath natiso i .F-ob x = CatIsoToPath (_ , natiso .nIso x) i - NatIsoToPath natiso i .F-hom f = isoToPath-Square isUnivD _ _ _ _ (natiso .trans .N-hom f) i - NatIsoToPath {F = F} {G = G} natiso i .F-id j = - isSet→SquareP (λ i j → D .isSetHom {x = NatIsoToPath natiso i .F-ob _} {y = NatIsoToPath natiso i .F-ob _}) - (F .F-id) (G .F-id) (λ i → NatIsoToPath natiso i .F-hom (C .id)) (λ i → D .id) i j - NatIsoToPath {F = F} {G = G} natiso i .F-seq f g j = - isSet→SquareP (λ i j → D .isSetHom {x = NatIsoToPath natiso i .F-ob _} {y = NatIsoToPath natiso i .F-ob _}) - (F .F-seq f g) (G .F-seq f g) (λ i → NatIsoToPath natiso i .F-hom (f ⋆⟨ C ⟩ g)) - (λ i → (NatIsoToPath natiso i .F-hom f) ⋆⟨ D ⟩ (NatIsoToPath natiso i .F-hom g)) i j + NatIsoToPath : NatIso F G → F ≡ G + NatIsoToPath niso = + Functor≡ (λ x → CatIsoToPath (_ , niso .nIso x)) + (λ f → isoToPath-Square isUnivD _ _ _ _ (niso .trans .N-hom f)) + + NatIso→Path→NatIso : (niso : NatIso F G) → pathToNatIso (NatIsoToPath niso) ≡ niso + NatIso→Path→NatIso niso = NatIso≡ (λ i x → secEq (univEquiv _ _) (_ , niso .nIso x) i .fst) + + Path→NatIso→Path : (p : F ≡ G) → NatIsoToPath (pathToNatIso p) ≡ p + Path→NatIso→Path p = FunctorPath≡ (λ i j x → retEq (univEquiv _ _) (λ i → p i .F-ob x) i j) diff --git a/Cubical/Foundations/Prelude.agda b/Cubical/Foundations/Prelude.agda index 5dc43bec50..da88442fd0 100644 --- a/Cubical/Foundations/Prelude.agda +++ b/Cubical/Foundations/Prelude.agda @@ -318,6 +318,23 @@ module _ (P : ∀ y → x ≡ y → Type ℓ') (d : P x refl) where (λ j → compPath-filler p q (i ∨ ~ k) j)) (~ k) (J (λ j → compPath-filler p q (~ k) j)) +-- 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 ℓ'') + (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 p = J ΠQ (λ _ → J (Q x refl) r) p _ + + J2Refl : J2 refl refl ≡ r + J2Refl = (λ i → JRefl ΠQ (λ _ → J (Q x refl) r) i _ refl) ∙ JRefl (Q x refl) _ + -- A prefix operator version of J that is more suitable to be nested module _ {P : ∀ y → x ≡ y → Type ℓ'} (d : P x refl) where From 08f2182e90e15ca57da09379775c60b4a37d13b7 Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Tue, 7 Jun 2022 18:24:01 +0800 Subject: [PATCH 10/18] done --- Cubical/Categories/Instances/Functors.agda | 49 +++++++++++++++++++ .../NaturalTransformation/Properties.agda | 9 +++- 2 files changed, 57 insertions(+), 1 deletion(-) diff --git a/Cubical/Categories/Instances/Functors.agda b/Cubical/Categories/Instances/Functors.agda index e80a1079c5..af8cf9285d 100644 --- a/Cubical/Categories/Instances/Functors.agda +++ b/Cubical/Categories/Instances/Functors.agda @@ -8,6 +8,10 @@ open import Cubical.Categories.NaturalTransformation.Base open import Cubical.Categories.NaturalTransformation.Properties open import Cubical.Categories.Morphism open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Equiv.Properties +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Isomorphism private variable @@ -50,3 +54,48 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where areInv-αd = isIso→areInv (is d) FUNCTORIso α is .sec = makeNatTransPath (funExt (λ c → (is c) .sec)) FUNCTORIso α is .ret = makeNatTransPath (funExt (λ c → (is c) .ret)) + + -- iso is componentwise iso in Functor + FUNCTORIso' : ∀ {F G : Functor C D} (α : F ⇒ G) + → isIsoC FUNCTOR α + → ((c : C .ob) → isIsoC D (α ⟦ c ⟧)) + FUNCTORIso' α isom c .invC = isom .invC .N-ob c + FUNCTORIso' α isom c .sec i = isom .sec i .N-ob c + FUNCTORIso' α isom c .ret i = isom .ret i .N-ob c + + open Iso + open NatIso + + Iso→NatIso : {F G : Functor C D} → CatIso FUNCTOR F G → NatIso F G + Iso→NatIso α .trans = α .fst + Iso→NatIso α .nIso = FUNCTORIso' _ (α .snd) + + Path→Iso→NatIso : {F G : Functor C D} → (p : F ≡ G) → pathToNatIso p ≡ Iso→NatIso (pathToIso p) + Path→Iso→NatIso {F = F} p = J (λ _ p → pathToNatIso p ≡ Iso→NatIso (pathToIso p)) (NatIso≡ refl-helper) p + where + refl-helper : _ + refl-helper i x = ((λ i → pathToIso-refl {C = D} {x = F .F-ob x} i .fst) + ∙ (λ i → pathToIso-refl {C = FUNCTOR} {x = F} (~ i) .fst .N-ob x)) i + + Iso-FUNCTORIso-NatIso : {F G : Functor C D} → Iso (CatIso FUNCTOR F G) (NatIso F G) + Iso-FUNCTORIso-NatIso .fun = Iso→NatIso + Iso-FUNCTORIso-NatIso .inv α = α .trans , FUNCTORIso _ (α .nIso) + Iso-FUNCTORIso-NatIso .rightInv α i .trans = α .trans + Iso-FUNCTORIso-NatIso .rightInv α i .nIso = + isProp→PathP (λ i → isPropΠ (λ _ → isPropIsIso _)) (FUNCTORIso' (α .trans) (FUNCTORIso _ (α .nIso))) (α .nIso) i + Iso-FUNCTORIso-NatIso .leftInv α i .fst = α .fst + Iso-FUNCTORIso-NatIso .leftInv α i .snd = + isProp→PathP (λ i → isPropIsIso _) (FUNCTORIso _ (FUNCTORIso' _ (α .snd))) (α .snd) i + + FUNCTORIso≃NatIso : {F G : Functor C D} → CatIso FUNCTOR F G ≃ NatIso F G + FUNCTORIso≃NatIso = isoToEquiv Iso-FUNCTORIso-NatIso + + + -- Functor Category is Univalent if the Target Category is Univalent + + open isUnivalent + + isUnivalentFUNCTOR : isUnivalent D → isUnivalent FUNCTOR + isUnivalentFUNCTOR isUnivD .univ _ _ = + isEquiv[equivFunA≃B∘f]→isEquiv[f] _ FUNCTORIso≃NatIso + (subst isEquiv (λ i p → Path→Iso→NatIso p i) (Path≃NatIso isUnivD .snd)) diff --git a/Cubical/Categories/NaturalTransformation/Properties.agda b/Cubical/Categories/NaturalTransformation/Properties.agda index dd5902eb1f..7f48548954 100644 --- a/Cubical/Categories/NaturalTransformation/Properties.agda +++ b/Cubical/Categories/NaturalTransformation/Properties.agda @@ -5,6 +5,7 @@ module Cubical.Categories.NaturalTransformation.Properties where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Univalence open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism renaming (iso to iIso) @@ -104,7 +105,7 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where (λ _ → isPropImplicitΠ2 (λ _ _ → isPropΠ (λ _ → isSetHom D _ _)))) --- Natural isomorphism is equivalent to path if the target category is univalent. +-- Natural isomorphism is path when the target category is univalent. module _ {C : Category ℓC ℓC'} @@ -123,3 +124,9 @@ module _ Path→NatIso→Path : (p : F ≡ G) → NatIsoToPath (pathToNatIso p) ≡ p Path→NatIso→Path p = FunctorPath≡ (λ i j x → retEq (univEquiv _ _) (λ i → p i .F-ob x) i j) + + Iso-Path-NatIso : Iso (F ≡ G) (NatIso F G) + Iso-Path-NatIso = iso pathToNatIso NatIsoToPath NatIso→Path→NatIso Path→NatIso→Path + + Path≃NatIso : (F ≡ G) ≃ NatIso F G + Path≃NatIso = isoToEquiv Iso-Path-NatIso From 409d390c3ad862a3b70840e61113048b04520c42 Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Tue, 7 Jun 2022 21:02:45 +0800 Subject: [PATCH 11/18] presheaf is univalent --- Cubical/Categories/Presheaf/Base.agda | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/Cubical/Categories/Presheaf/Base.agda b/Cubical/Categories/Presheaf/Base.agda index c1b4e2d7f4..4c36261a78 100644 --- a/Cubical/Categories/Presheaf/Base.agda +++ b/Cubical/Categories/Presheaf/Base.agda @@ -7,7 +7,16 @@ open import Cubical.Categories.Category open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Instances.Functors -PreShv : ∀ {ℓ ℓ'} → Category ℓ ℓ' → (ℓS : Level) +private + variable + ℓ ℓ' ℓS : Level + +PreShv : Category ℓ ℓ' → (ℓS : Level) → Category (ℓ-max (ℓ-max ℓ ℓ') (ℓ-suc ℓS)) (ℓ-max (ℓ-max ℓ ℓ') ℓS) PreShv C ℓS = FUNCTOR (C ^op) (SET ℓS) + +-- Presheaf Category is Univalent + +isUnivalentPreShv : {C : Category ℓ ℓ'} → isUnivalent (PreShv C ℓS) +isUnivalentPreShv = isUnivalentFUNCTOR _ _ isUnivalentSET From 979a521bac5b8dbf7dcf53746a930623be1a02b2 Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Wed, 8 Jun 2022 22:30:18 +0800 Subject: [PATCH 12/18] a bit --- Cubical/Categories/Functor/Compose.agda | 113 ++++++++++++++++++ Cubical/Categories/Isomorphism.agda | 67 +++++++++++ .../NaturalTransformation/Base.agda | 5 + .../NaturalTransformation/Properties.agda | 1 - 4 files changed, 185 insertions(+), 1 deletion(-) diff --git a/Cubical/Categories/Functor/Compose.agda b/Cubical/Categories/Functor/Compose.agda index d413a8f575..336314786d 100644 --- a/Cubical/Categories/Functor/Compose.agda +++ b/Cubical/Categories/Functor/Compose.agda @@ -3,8 +3,12 @@ module Cubical.Categories.Functor.Compose where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Data.Sigma +open import Cubical.HITs.PropositionalTruncation as Prop open import Cubical.Categories.Category +open import Cubical.Categories.Isomorphism open import Cubical.Categories.Functor.Base open import Cubical.Categories.NaturalTransformation.Base @@ -42,3 +46,112 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} ∙∙ G .F-seq (α ⟦ x ⟧) (F₁ ⟪ f ⟫) postcomposeF .F-id = makeNatTransPath (funExt λ _ → G .F-id) postcomposeF .F-seq f g = makeNatTransPath (funExt λ _ → G .F-seq _ _) + + +-- Composition induced by special functors + +module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} + {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (E : Category ℓE ℓE') + {F : Functor C D} + where + + open Category + open Functor + open NatTrans + open isIso + + + isEssSurj→isFaithfulPrecomp : isEssentiallySurj F → isFaithful (precomposeF E F) + isEssSurj→isFaithfulPrecomp surj A B α β p = + makeNatTransPath + (λ i x → Prop.rec (E .isSetHom _ _) + (λ (c , f) → + ⋆InvLMove (F-Iso {F = A} f) (α .N-hom (f .fst)) + ∙ (λ i → F-Iso {F = A} f .snd .inv ⋆⟨ E ⟩ (p i .N-ob c ⋆⟨ E ⟩ B .F-hom (f .fst))) + ∙ sym (⋆InvLMove (F-Iso {F = A} f) (β .N-hom (f .fst)))) + (surj x) i) + + + isEssSurj+Full→isFullPrecomp : isEssentiallySurj F → isFull F → isFull (precomposeF E F) + isEssSurj+Full→isFullPrecomp surj full A B α = ∣ ext , ext≡ ∣₁ + where + Mor : (d : D .ob) → Type _ + Mor d = + Σ[ g ∈ E [ A .F-ob d , B .F-ob d ] ] + ((c : C .ob)(f : CatIso D (F .F-ob c) d) + → α .N-ob c ≡ A .F-hom (f .fst) ⋆⟨ E ⟩ g ⋆⟨ E ⟩ B .F-hom (f .snd .inv)) + + isPropMor : (d : D .ob) → isProp (Mor d) + isPropMor d x y = Σ≡Prop (λ _ → isPropΠ2 (λ _ _ → E .isSetHom _ _)) path + where + path : x .fst ≡ y .fst + path = Prop.rec (E .isSetHom _ _) + (λ (c , f) → + ⋆CancelL (F-Iso {F = A} f) (⋆CancelR (invIso (F-Iso {F = B} f)) + (sym (x .snd c f) ∙ y .snd c f))) + (surj d) + + isContrMor : (d : D .ob) → isContr (Mor d) + isContrMor d = inhProp→isContr inhab (isPropMor d) + where + inhab : Mor d + inhab = Prop.rec (isPropMor d) + (λ (a , h) → + A .F-hom (h .snd .inv) ⋆⟨ E ⟩ α .N-ob a ⋆⟨ E ⟩ B .F-hom (h .fst) , + λ c f → + Prop.rec (E .isSetHom _ _) + (λ (k , p) → + let isom-path = subst-filler (isIso D) (sym p) (⋆Iso f (invIso h) .snd) in + ⋆InvRMove (F-Iso {F = B} (_ , isom-path i1)) (sym (α .N-hom k)) + ∙ (λ i → A .F-hom (p i) ⋆⟨ E ⟩ α .N-ob a ⋆⟨ E ⟩ F-Iso {F = B} (p i , isom-path (~ i)) .snd .inv) + ∙ (λ i → A .F-seq (f .fst) (h .snd .inv) i ⋆⟨ E ⟩ α .N-ob a ⋆⟨ E ⟩ F-Iso-Pres⋆ {F = B} h (invIso f) i .fst) + ∙ sym (E .⋆Assoc _ _ _) + ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _) + ∙ cong (λ x → x ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _)) + (full _ _ (f .fst ⋆⟨ D ⟩ h .snd .inv))) + (surj d) + + mor-eq : (d : D .ob)(c : C .ob)(f : CatIso D (F .F-ob c) d) + → isContrMor d .fst .fst ≡ A .F-hom (f .snd .inv) ⋆⟨ E ⟩ α .N-ob c ⋆⟨ E ⟩ B .F-hom (f .fst) + mor-eq d c f = + ⋆InvLMove (F-Iso {F = A} f) (⋆InvRMove (invIso (F-Iso {F = B} f)) (sym (isContrMor d .fst .snd c f))) + ∙ sym (E .⋆Assoc _ _ _) + + F-seq3 : (F : Functor D E) {x y z w : D .ob} + → {f : D [ x , y ]}{g : D [ y , z ]}{h : D [ z , w ]} + → F .F-hom (f ⋆⟨ D ⟩ g ⋆⟨ D ⟩ h) ≡ F .F-hom f ⋆⟨ E ⟩ F .F-hom g ⋆⟨ E ⟩ F .F-hom h + F-seq3 = {!!} + + ext : NatTrans A B + ext .N-ob d = isContrMor d .fst .fst + ext .N-hom {x = d} {y = d'} f = Prop.rec2 (E .isSetHom _ _) + (λ (c , h) (c' , h') → Prop.rec (E .isSetHom _ _) + (λ (k , p) → + (λ i → A .F-hom f ⋆⟨ E ⟩ mor-eq d' c' h' i) + ∙ cong (λ x → A .F-hom f ⋆⟨ E ⟩ x) (E .⋆Assoc _ _ _) + ∙ sym (E .⋆Assoc _ _ _) ∙ sym (E .⋆Assoc _ _ _) + ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (E .⋆IdL _)) + ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (F-Iso {F = A} h .snd .sec)) + ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _) + ∙ cong (λ x → _ ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (E .⋆Assoc _ _ _)) + ∙ cong (λ x → _ ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (F-seq3 A)) + ∙ cong (λ x → A .F-hom (invIso h .fst) ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (cong (A .F-hom) p)) + ∙ cong (λ x → x ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _) + ∙ cong (λ x → _ ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _) (α .N-hom k) + ∙ cong (λ x → x ⋆⟨ E ⟩ _) (sym (E .⋆Assoc _ _ _)) + ∙ E .⋆Assoc _ _ _ + ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ (x ⋆⟨ E ⟩ B .F-hom (h' .fst))) (cong (B .F-hom) p) + ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ (x ⋆⟨ E ⟩ B .F-hom (h' .fst))) (F-seq3 B) + ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ x) (E .⋆Assoc _ _ _) + ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ (_ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ x)) (F-Iso {F = B} h' .snd .sec) + ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ x) (E .⋆IdR _) + ∙ sym (E .⋆Assoc _ _ _) + ∙ (λ i → mor-eq d c h (~ i) ⋆⟨ E ⟩ B .F-hom f)) + (full _ _ (h .fst ⋆⟨ D ⟩ f ⋆⟨ D ⟩ h' .snd .inv))) + (surj d) (surj d') + + ext≡ : precomposeF E F .F-hom ext ≡ α + ext≡ = makeNatTransPath (λ i c → + (mor-eq _ c idCatIso + ∙ (λ i → A .F-id i ⋆⟨ E ⟩ α .N-ob c ⋆⟨ E ⟩ B .F-id i) + ∙ E .⋆IdR _ ∙ E .⋆IdL _) i) diff --git a/Cubical/Categories/Isomorphism.agda b/Cubical/Categories/Isomorphism.agda index 06c46539c9..dc5075526f 100644 --- a/Cubical/Categories/Isomorphism.agda +++ b/Cubical/Categories/Isomorphism.agda @@ -19,6 +19,16 @@ module _ {C : Category ℓC ℓC'} where open isIso + invIso : {x y : ob} → CatIso C x y → CatIso C y x + invIso f .fst = f .snd .inv + invIso f .snd .inv = f .fst + invIso f .snd .sec = f .snd .ret + invIso f .snd .ret = f .snd .sec + + invIsoIdem : {x y : ob} → (f : CatIso C x y) → invIso (invIso f) ≡ f + invIsoIdem f = refl + + ⋆Iso : {x y z : ob} → (f : CatIso C x y)(g : CatIso C y z) → CatIso C x z ⋆Iso f g .fst = f .fst ⋆ g .fst ⋆Iso f g .snd .inv = g .snd .inv ⋆ f .snd .inv @@ -43,6 +53,9 @@ module _ {C : Category ℓC ℓC'} where ⋆IsoIdR : {x y : ob} → (f : CatIso C x y) → ⋆Iso f idCatIso ≡ f ⋆IsoIdR _ = CatIso≡ _ _ (⋆IdR _) + ⋆IsoInvRev : {x y z : ob} → (f : CatIso C x y)(g : CatIso C y z) → invIso (⋆Iso f g) ≡ ⋆Iso (invIso g) (invIso f) + ⋆IsoInvRev _ _ = refl + pathToIso-∙ : {x y z : ob}(p : x ≡ y)(q : y ≡ z) → pathToIso (p ∙ q) ≡ ⋆Iso (pathToIso p) (pathToIso q) pathToIso-∙ p q = J2 (λ y p z q → pathToIso (p ∙ q) ≡ ⋆Iso (pathToIso p) (pathToIso q)) pathToIso-∙-refl p q @@ -106,6 +119,60 @@ module _ {C : Category ℓC ℓC'} where ((λ i → f ⋆ secEq (univEquiv _ _) q i .fst) ∙ comm ∙ (λ i → secEq (univEquiv _ _) p (~ i) .fst ⋆ g)) +module _ {C : Category ℓC ℓC'} where + + open Category C + open isIso + + ⋆InvLMove : {x y z : ob} + (f : CatIso C x y) + {g : Hom[ y , z ]}{h : Hom[ x , z ]} + → f .fst ⋆ g ≡ h + → g ≡ f .snd .inv ⋆ h + ⋆InvLMove f {g = g} p = + sym (⋆IdL _) + ∙ (λ i → f .snd .sec (~ i) ⋆ g) + ∙ ⋆Assoc _ _ _ + ∙ (λ i → f .snd .inv ⋆ p i) + + ⋆InvRMove : {x y z : ob} + (f : CatIso C y z) + {g : Hom[ x , y ]}{h : Hom[ x , z ]} + → g ⋆ f .fst ≡ h + → g ≡ h ⋆ f .snd .inv + ⋆InvRMove f {g = g} p = + sym (⋆IdR _) + ∙ (λ i → g ⋆ f .snd .ret (~ i)) + ∙ sym (⋆Assoc _ _ _) + ∙ (λ i → p i ⋆ f .snd .inv) + + ⋆CancelL : {x y z : ob} + (f : CatIso C x y){g h : Hom[ y , z ]} + → f .fst ⋆ g ≡ f .fst ⋆ h + → g ≡ h + ⋆CancelL f {g = g} {h = h} p = + sym (⋆IdL _) + ∙ (λ i → f .snd .sec (~ i) ⋆ g) + ∙ ⋆Assoc _ _ _ + ∙ (λ i → f .snd .inv ⋆ p i) + ∙ sym (⋆Assoc _ _ _) + ∙ (λ i → f .snd .sec i ⋆ h) + ∙ ⋆IdL _ + + ⋆CancelR : {x y z : ob} + (f : CatIso C y z){g h : Hom[ x , y ]} + → g ⋆ f .fst ≡ h ⋆ f .fst + → g ≡ h + ⋆CancelR f {g = g} {h = h} p = + sym (⋆IdR _) + ∙ (λ i → g ⋆ f .snd .ret (~ i)) + ∙ sym (⋆Assoc _ _ _) + ∙ (λ i → p i ⋆ f .snd .inv) + ∙ ⋆Assoc _ _ _ + ∙ (λ i → h ⋆ f .snd .ret i) + ∙ ⋆IdR _ + + module _ {C : Category ℓC ℓC'} where open Category diff --git a/Cubical/Categories/NaturalTransformation/Base.agda b/Cubical/Categories/NaturalTransformation/Base.agda index a60817a41d..ca506b461f 100644 --- a/Cubical/Categories/NaturalTransformation/Base.agda +++ b/Cubical/Categories/NaturalTransformation/Base.agda @@ -94,6 +94,11 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where syntax idTrans F = 1[ F ] + idNatIso : (F : Functor C D) → NatIso F F + idNatIso F .trans = idTrans F + idNatIso F .nIso _ = idCatIso .snd + + -- Natural isomorphism induced by path of functors pathToNatTrans : {F G : Functor C D} → F ≡ G → NatTrans F G diff --git a/Cubical/Categories/NaturalTransformation/Properties.agda b/Cubical/Categories/NaturalTransformation/Properties.agda index 7f48548954..d71850ec8b 100644 --- a/Cubical/Categories/NaturalTransformation/Properties.agda +++ b/Cubical/Categories/NaturalTransformation/Properties.agda @@ -97,7 +97,6 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where module _ where open NatTransP - -- if the target category has hom Sets, then any natural transformation is a set isSetNatTrans : {F G : Functor C D} → isSet (NatTrans F G) isSetNatTrans = isSetRetract (fun NatTransIsoΣ) (inv NatTransIsoΣ) (leftInv NatTransIsoΣ) From 51db046ccaeb21a151521b3aafbfc1e56a3f4860 Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Thu, 9 Jun 2022 02:30:58 +0800 Subject: [PATCH 13/18] more --- Cubical/Categories/Functor/Compose.agda | 113 ---------- .../Categories/Functor/ComposeProperty.agda | 200 ++++++++++++++++++ Cubical/Categories/Functor/Properties.agda | 11 + Cubical/Categories/Isomorphism.agda | 21 ++ Cubical/Categories/RezkCompletion.agda | 5 + Cubical/Categories/RezkCompletion/Base.agda | 46 ++++ Cubical/Foundations/HLevels.agda | 7 +- 7 files changed, 289 insertions(+), 114 deletions(-) create mode 100644 Cubical/Categories/Functor/ComposeProperty.agda create mode 100644 Cubical/Categories/RezkCompletion.agda create mode 100644 Cubical/Categories/RezkCompletion/Base.agda diff --git a/Cubical/Categories/Functor/Compose.agda b/Cubical/Categories/Functor/Compose.agda index 336314786d..d413a8f575 100644 --- a/Cubical/Categories/Functor/Compose.agda +++ b/Cubical/Categories/Functor/Compose.agda @@ -3,12 +3,8 @@ module Cubical.Categories.Functor.Compose where open import Cubical.Foundations.Prelude -open import Cubical.Foundations.HLevels -open import Cubical.Data.Sigma -open import Cubical.HITs.PropositionalTruncation as Prop open import Cubical.Categories.Category -open import Cubical.Categories.Isomorphism open import Cubical.Categories.Functor.Base open import Cubical.Categories.NaturalTransformation.Base @@ -46,112 +42,3 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} ∙∙ G .F-seq (α ⟦ x ⟧) (F₁ ⟪ f ⟫) postcomposeF .F-id = makeNatTransPath (funExt λ _ → G .F-id) postcomposeF .F-seq f g = makeNatTransPath (funExt λ _ → G .F-seq _ _) - - --- Composition induced by special functors - -module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} - {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (E : Category ℓE ℓE') - {F : Functor C D} - where - - open Category - open Functor - open NatTrans - open isIso - - - isEssSurj→isFaithfulPrecomp : isEssentiallySurj F → isFaithful (precomposeF E F) - isEssSurj→isFaithfulPrecomp surj A B α β p = - makeNatTransPath - (λ i x → Prop.rec (E .isSetHom _ _) - (λ (c , f) → - ⋆InvLMove (F-Iso {F = A} f) (α .N-hom (f .fst)) - ∙ (λ i → F-Iso {F = A} f .snd .inv ⋆⟨ E ⟩ (p i .N-ob c ⋆⟨ E ⟩ B .F-hom (f .fst))) - ∙ sym (⋆InvLMove (F-Iso {F = A} f) (β .N-hom (f .fst)))) - (surj x) i) - - - isEssSurj+Full→isFullPrecomp : isEssentiallySurj F → isFull F → isFull (precomposeF E F) - isEssSurj+Full→isFullPrecomp surj full A B α = ∣ ext , ext≡ ∣₁ - where - Mor : (d : D .ob) → Type _ - Mor d = - Σ[ g ∈ E [ A .F-ob d , B .F-ob d ] ] - ((c : C .ob)(f : CatIso D (F .F-ob c) d) - → α .N-ob c ≡ A .F-hom (f .fst) ⋆⟨ E ⟩ g ⋆⟨ E ⟩ B .F-hom (f .snd .inv)) - - isPropMor : (d : D .ob) → isProp (Mor d) - isPropMor d x y = Σ≡Prop (λ _ → isPropΠ2 (λ _ _ → E .isSetHom _ _)) path - where - path : x .fst ≡ y .fst - path = Prop.rec (E .isSetHom _ _) - (λ (c , f) → - ⋆CancelL (F-Iso {F = A} f) (⋆CancelR (invIso (F-Iso {F = B} f)) - (sym (x .snd c f) ∙ y .snd c f))) - (surj d) - - isContrMor : (d : D .ob) → isContr (Mor d) - isContrMor d = inhProp→isContr inhab (isPropMor d) - where - inhab : Mor d - inhab = Prop.rec (isPropMor d) - (λ (a , h) → - A .F-hom (h .snd .inv) ⋆⟨ E ⟩ α .N-ob a ⋆⟨ E ⟩ B .F-hom (h .fst) , - λ c f → - Prop.rec (E .isSetHom _ _) - (λ (k , p) → - let isom-path = subst-filler (isIso D) (sym p) (⋆Iso f (invIso h) .snd) in - ⋆InvRMove (F-Iso {F = B} (_ , isom-path i1)) (sym (α .N-hom k)) - ∙ (λ i → A .F-hom (p i) ⋆⟨ E ⟩ α .N-ob a ⋆⟨ E ⟩ F-Iso {F = B} (p i , isom-path (~ i)) .snd .inv) - ∙ (λ i → A .F-seq (f .fst) (h .snd .inv) i ⋆⟨ E ⟩ α .N-ob a ⋆⟨ E ⟩ F-Iso-Pres⋆ {F = B} h (invIso f) i .fst) - ∙ sym (E .⋆Assoc _ _ _) - ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _) - ∙ cong (λ x → x ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _)) - (full _ _ (f .fst ⋆⟨ D ⟩ h .snd .inv))) - (surj d) - - mor-eq : (d : D .ob)(c : C .ob)(f : CatIso D (F .F-ob c) d) - → isContrMor d .fst .fst ≡ A .F-hom (f .snd .inv) ⋆⟨ E ⟩ α .N-ob c ⋆⟨ E ⟩ B .F-hom (f .fst) - mor-eq d c f = - ⋆InvLMove (F-Iso {F = A} f) (⋆InvRMove (invIso (F-Iso {F = B} f)) (sym (isContrMor d .fst .snd c f))) - ∙ sym (E .⋆Assoc _ _ _) - - F-seq3 : (F : Functor D E) {x y z w : D .ob} - → {f : D [ x , y ]}{g : D [ y , z ]}{h : D [ z , w ]} - → F .F-hom (f ⋆⟨ D ⟩ g ⋆⟨ D ⟩ h) ≡ F .F-hom f ⋆⟨ E ⟩ F .F-hom g ⋆⟨ E ⟩ F .F-hom h - F-seq3 = {!!} - - ext : NatTrans A B - ext .N-ob d = isContrMor d .fst .fst - ext .N-hom {x = d} {y = d'} f = Prop.rec2 (E .isSetHom _ _) - (λ (c , h) (c' , h') → Prop.rec (E .isSetHom _ _) - (λ (k , p) → - (λ i → A .F-hom f ⋆⟨ E ⟩ mor-eq d' c' h' i) - ∙ cong (λ x → A .F-hom f ⋆⟨ E ⟩ x) (E .⋆Assoc _ _ _) - ∙ sym (E .⋆Assoc _ _ _) ∙ sym (E .⋆Assoc _ _ _) - ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (E .⋆IdL _)) - ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (F-Iso {F = A} h .snd .sec)) - ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _) - ∙ cong (λ x → _ ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (E .⋆Assoc _ _ _)) - ∙ cong (λ x → _ ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (F-seq3 A)) - ∙ cong (λ x → A .F-hom (invIso h .fst) ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (cong (A .F-hom) p)) - ∙ cong (λ x → x ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _) - ∙ cong (λ x → _ ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _) (α .N-hom k) - ∙ cong (λ x → x ⋆⟨ E ⟩ _) (sym (E .⋆Assoc _ _ _)) - ∙ E .⋆Assoc _ _ _ - ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ (x ⋆⟨ E ⟩ B .F-hom (h' .fst))) (cong (B .F-hom) p) - ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ (x ⋆⟨ E ⟩ B .F-hom (h' .fst))) (F-seq3 B) - ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ x) (E .⋆Assoc _ _ _) - ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ (_ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ x)) (F-Iso {F = B} h' .snd .sec) - ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ x) (E .⋆IdR _) - ∙ sym (E .⋆Assoc _ _ _) - ∙ (λ i → mor-eq d c h (~ i) ⋆⟨ E ⟩ B .F-hom f)) - (full _ _ (h .fst ⋆⟨ D ⟩ f ⋆⟨ D ⟩ h' .snd .inv))) - (surj d) (surj d') - - ext≡ : precomposeF E F .F-hom ext ≡ α - ext≡ = makeNatTransPath (λ i c → - (mor-eq _ c idCatIso - ∙ (λ i → A .F-id i ⋆⟨ E ⟩ α .N-ob c ⋆⟨ E ⟩ B .F-id i) - ∙ E .⋆IdR _ ∙ E .⋆IdL _) i) diff --git a/Cubical/Categories/Functor/ComposeProperty.agda b/Cubical/Categories/Functor/ComposeProperty.agda new file mode 100644 index 0000000000..052315ff1b --- /dev/null +++ b/Cubical/Categories/Functor/ComposeProperty.agda @@ -0,0 +1,200 @@ +{-# OPTIONS --safe #-} + +module Cubical.Categories.Functor.ComposeProperty where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Data.Sigma +open import Cubical.HITs.PropositionalTruncation as Prop + +open import Cubical.Categories.Category +open import Cubical.Categories.Isomorphism +open import Cubical.Categories.Functor +open import Cubical.Categories.NaturalTransformation.Base +open import Cubical.Categories.Equivalence.WeakEquivalence + +open import Cubical.Categories.Instances.Functors + + +-- Composition induced by special functors + +module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} + {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (E : Category ℓE ℓE') + (F : Functor C D) + where + + open Category + open Functor + open NatTrans + open isIso + + + isEssSurj→isFaithfulPrecomp : isEssentiallySurj F → isFaithful (precomposeF E F) + isEssSurj→isFaithfulPrecomp surj A B α β p = + makeNatTransPath + (λ i x → Prop.rec (E .isSetHom _ _) + (λ (c , f) → + ⋆InvLMove (F-Iso {F = A} f) (α .N-hom (f .fst)) + ∙ (λ i → F-Iso {F = A} f .snd .inv ⋆⟨ E ⟩ (p i .N-ob c ⋆⟨ E ⟩ B .F-hom (f .fst))) + ∙ sym (⋆InvLMove (F-Iso {F = A} f) (β .N-hom (f .fst)))) + (surj x) i) + + + isEssSurj+Full→isFullPrecomp : isEssentiallySurj F → isFull F → isFull (precomposeF E F) + isEssSurj+Full→isFullPrecomp surj full A B α = ∣ ext , ext≡ ∣₁ + where + Mor : (d : D .ob) → Type _ + Mor d = + Σ[ g ∈ E [ A .F-ob d , B .F-ob d ] ] + ((c : C .ob)(f : CatIso D (F .F-ob c) d) + → α .N-ob c ≡ A .F-hom (f .fst) ⋆⟨ E ⟩ g ⋆⟨ E ⟩ B .F-hom (f .snd .inv)) + + isPropMor : (d : D .ob) → isProp (Mor d) + isPropMor d x y = Σ≡Prop (λ _ → isPropΠ2 (λ _ _ → E .isSetHom _ _)) path + where + path : x .fst ≡ y .fst + path = Prop.rec (E .isSetHom _ _) + (λ (c , f) → + ⋆CancelL (F-Iso {F = A} f) (⋆CancelR (invIso (F-Iso {F = B} f)) + (sym (x .snd c f) ∙ y .snd c f))) + (surj d) + + isContrMor : (d : D .ob) → isContr (Mor d) + isContrMor d = inhProp→isContr inhab (isPropMor d) + where + inhab : Mor d + inhab = Prop.rec (isPropMor d) + (λ (a , h) → + A .F-hom (h .snd .inv) ⋆⟨ E ⟩ α .N-ob a ⋆⟨ E ⟩ B .F-hom (h .fst) , + λ c f → + Prop.rec (E .isSetHom _ _) + (λ (k , p) → + let isom-path = subst-filler (isIso D) (sym p) (⋆Iso f (invIso h) .snd) in + ⋆InvRMove (F-Iso {F = B} (_ , isom-path i1)) (sym (α .N-hom k)) + ∙ (λ i → A .F-hom (p i) ⋆⟨ E ⟩ α .N-ob a ⋆⟨ E ⟩ F-Iso {F = B} (p i , isom-path (~ i)) .snd .inv) + ∙ (λ i → A .F-seq (f .fst) (h .snd .inv) i ⋆⟨ E ⟩ α .N-ob a ⋆⟨ E ⟩ F-Iso-Pres⋆ {F = B} h (invIso f) i .fst) + ∙ sym (E .⋆Assoc _ _ _) + ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _) + ∙ cong (λ x → x ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _)) + (full _ _ (f .fst ⋆⟨ D ⟩ h .snd .inv))) + (surj d) + + mor-eq : (d : D .ob)(c : C .ob)(f : CatIso D (F .F-ob c) d) + → isContrMor d .fst .fst ≡ A .F-hom (f .snd .inv) ⋆⟨ E ⟩ α .N-ob c ⋆⟨ E ⟩ B .F-hom (f .fst) + mor-eq d c f = + ⋆InvLMove (F-Iso {F = A} f) (⋆InvRMove (invIso (F-Iso {F = B} f)) (sym (isContrMor d .fst .snd c f))) + ∙ sym (E .⋆Assoc _ _ _) + + F-seq3 : (F : Functor D E) {x y z w : D .ob} + → {f : D [ x , y ]}{g : D [ y , z ]}{h : D [ z , w ]} + → F .F-hom (f ⋆⟨ D ⟩ g ⋆⟨ D ⟩ h) ≡ F .F-hom f ⋆⟨ E ⟩ F .F-hom g ⋆⟨ E ⟩ F .F-hom h + F-seq3 F = F .F-seq _ _ ∙ cong (λ x → x ⋆⟨ E ⟩ _) (F .F-seq _ _) + + ext : NatTrans A B + ext .N-ob d = isContrMor d .fst .fst + ext .N-hom {x = d} {y = d'} f = Prop.rec2 (E .isSetHom _ _) + (λ (c , h) (c' , h') → Prop.rec (E .isSetHom _ _) + (λ (k , p) → + (λ i → A .F-hom f ⋆⟨ E ⟩ mor-eq d' c' h' i) + ∙ cong (λ x → A .F-hom f ⋆⟨ E ⟩ x) (E .⋆Assoc _ _ _) + ∙ sym (E .⋆Assoc _ _ _) ∙ sym (E .⋆Assoc _ _ _) + ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (E .⋆IdL _)) + ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (F-Iso {F = A} h .snd .sec)) + ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _) + ∙ cong (λ x → _ ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (E .⋆Assoc _ _ _)) + ∙ cong (λ x → _ ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (F-seq3 A)) + ∙ cong (λ x → A .F-hom (invIso h .fst) ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (cong (A .F-hom) p)) + ∙ cong (λ x → x ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _) + ∙ cong (λ x → _ ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _) (α .N-hom k) + ∙ cong (λ x → x ⋆⟨ E ⟩ _) (sym (E .⋆Assoc _ _ _)) + ∙ E .⋆Assoc _ _ _ + ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ (x ⋆⟨ E ⟩ B .F-hom (h' .fst))) (cong (B .F-hom) p) + ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ (x ⋆⟨ E ⟩ B .F-hom (h' .fst))) (F-seq3 B) + ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ x) (E .⋆Assoc _ _ _) + ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ (_ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ x)) (F-Iso {F = B} h' .snd .sec) + ∙ cong (λ x → _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ x) (E .⋆IdR _) + ∙ sym (E .⋆Assoc _ _ _) + ∙ (λ i → mor-eq d c h (~ i) ⋆⟨ E ⟩ B .F-hom f)) + (full _ _ (h .fst ⋆⟨ D ⟩ f ⋆⟨ D ⟩ h' .snd .inv))) + (surj d) (surj d') + + ext≡ : precomposeF E F .F-hom ext ≡ α + ext≡ = makeNatTransPath (λ i c → + (mor-eq _ c idCatIso + ∙ (λ i → A .F-id i ⋆⟨ E ⟩ α .N-ob c ⋆⟨ E ⟩ B .F-id i) + ∙ E .⋆IdR _ ∙ E .⋆IdL _) i) + + + isEssSurj+Full→isFullyFaithfulPrecomp : isEssentiallySurj F → isFull F → isFullyFaithful (precomposeF E F) + isEssSurj+Full→isFullyFaithfulPrecomp surj full = + isFull+Faithful→isFullyFaithful {F = precomposeF E F} + (isEssSurj+Full→isFullPrecomp surj full) (isEssSurj→isFaithfulPrecomp surj) + + +module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} + {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} + {E : Category ℓE ℓE'} (isUnivE : isUnivalent E) + (F : Functor C D) + where + + open Category + open Functor + open NatTrans + open isIso + open isWeakEquivalence + open isUnivalent isUnivE + + isWeakEquiv→isEssSurjPrecomp : isWeakEquivalence F → isEssentiallySurj (precomposeF E F) + isWeakEquiv→isEssSurjPrecomp w-equiv G = {!!} + where + Obj : (d : D .ob) → Type _ + Obj d = Σ[ e ∈ E .ob ] + Σ[ k ∈ ((c : C .ob)(h : CatIso D (F .F-ob c) d) → CatIso E (G .F-ob c) e) ] + ((c c' : C .ob)(h : CatIso D (F .F-ob c) d)(h' : CatIso D (F .F-ob c') d) + → (f : C [ c , c' ]) + → F .F-hom f ⋆⟨ D ⟩ h' .fst ≡ h .fst + → G .F-hom f ⋆⟨ E ⟩ k c' h' .fst ≡ k c h .fst) + + module _ (d : D .ob)(c₀ : C .ob)(h₀ : CatIso D (F .F-ob c₀) d) where + + g : (c : C .ob)(h : CatIso D (F .F-ob c) d) → CatIso C c c₀ + g c h = liftIso {F = F} (w-equiv .fullfaith) (⋆Iso h (invIso h₀)) + + g-eq : ∀ c h → F .F-hom (g c h .fst) ⋆⟨ D ⟩ h₀ .fst ≡ h .fst + g-eq c h = + cong (λ x → x ⋆⟨ D ⟩ _) (cong fst (liftIso≡ {F = F} (w-equiv .fullfaith) (⋆Iso h (invIso h₀)))) + ∙ D .⋆Assoc _ _ _ + ∙ cong (λ x → _ ⋆⟨ D ⟩ x) (h₀ .snd .sec) + ∙ D .⋆IdR _ + + isContrObj' : isContr (Obj d) + isContrObj' .fst .fst = G .F-ob c₀ + isContrObj' .fst .snd .fst c h = F-Iso {F = G} (g c h) + isContrObj' .fst .snd .snd c c' h h' f p = sym (G .F-seq _ _) ∙ cong (G .F-hom) g-path + where + g-path : f ⋆⟨ C ⟩ g c' h' .fst ≡ g c h .fst + g-path = isFullyFaithful→Faithful {F = F} (w-equiv .fullfaith) _ _ _ _ + (F .F-seq _ _ + ∙ cong (λ x → _ ⋆⟨ D ⟩ x) (cong fst (liftIso≡ {F = F} (w-equiv .fullfaith) (⋆Iso h' (invIso h₀)))) + ∙ sym (D .⋆Assoc _ _ _) + ∙ cong (λ x → x ⋆⟨ D ⟩ invIso h₀ .fst) p + ∙ cong fst (sym (liftIso≡ {F = F} (w-equiv .fullfaith) (⋆Iso h (invIso h₀))))) + isContrObj' .snd (e , k , coh) i .fst = CatIsoToPath (k c₀ h₀) i + isContrObj' .snd (e , k , coh) i .snd .fst c h = + let isom₀ = F-Iso {F = G} (g c h) in + hcomp (λ j → λ + { (i = i0) → isom₀ + ; (i = i1) → CatIso≡ (⋆Iso isom₀ (k c₀ h₀)) (k c h) (coh c c₀ h h₀ (g c h .fst) (g-eq c h)) j }) + (transportIsoToPathIso isUnivE isom₀ _ i) + isContrObj' .snd x@(e , k , coh) i .snd .snd = + isProp→PathP (λ i → isPropΠ6 (λ c c' h h' f _ → + E .isSetHom + (G .F-hom f ⋆⟨ E ⟩ isContrObj' .snd x i .snd .fst c' h' .fst) + (isContrObj' .snd x i .snd .fst c h .fst))) + (isContrObj' .fst .snd .snd) coh i + + isContrObj : (d : D .ob) → isContr (Obj d) + isContrObj d = Prop.rec isPropIsContr (λ (c , h) → isContrObj' d c h) (w-equiv .esssurj d) + + Ext-ob : D .ob → E .ob + Ext-ob d = isContrObj d .fst .fst diff --git a/Cubical/Categories/Functor/Properties.agda b/Cubical/Categories/Functor/Properties.agda index 362efde99a..336139f556 100644 --- a/Cubical/Categories/Functor/Properties.agda +++ b/Cubical/Categories/Functor/Properties.agda @@ -189,6 +189,17 @@ module _ {F : Functor C D} where ∙ isoFf .ret ∙ sym (F .F-id)) + -- Lifting isomorphism upwards a fully faithful functor + + module _ (fullfaith : isFullyFaithful F) where + + liftIso : {x y : C .ob} → CatIso D (F .F-ob x) (F .F-ob y) → CatIso C x y + liftIso f .fst = invEq (_ , fullfaith _ _) (f .fst) + liftIso f .snd = isFullyFaithful→Conservative fullfaith (subst (isIso D) (sym (secEq (_ , fullfaith _ _) (f .fst))) (f .snd)) + + liftIso≡ : {x y : C .ob} → (f : CatIso D (F .F-ob x) (F .F-ob y)) → F-Iso {F = F} (liftIso f) ≡ f + liftIso≡ f = CatIso≡ _ _ (secEq (_ , fullfaith _ _) (f .fst)) + -- Functors inducing surjection on objects is essentially surjective diff --git a/Cubical/Categories/Isomorphism.agda b/Cubical/Categories/Isomorphism.agda index dc5075526f..ca13f619e5 100644 --- a/Cubical/Categories/Isomorphism.agda +++ b/Cubical/Categories/Isomorphism.agda @@ -66,6 +66,11 @@ module _ {C : Category ℓC ℓC'} where ∙ (λ i → ⋆Iso (pathToIso-refl (~ i)) (pathToIso refl)) + transportPathToIso : {x y z : ob}(f : C [ x , y ])(p : y ≡ z) → PathP (λ i → C [ x , p i ]) f (f ⋆ pathToIso {C = C} p .fst) + transportPathToIso {x = x} f = J (λ _ p → PathP (λ i → C [ x , p i ]) f (f ⋆ pathToIso {C = C} p .fst)) + (sym (⋆IdR _) ∙ cong (λ x → f ⋆ x) (sym (cong fst (pathToIso-refl {C = C})))) + + pathToIso-Comm : {x y z w : ob} → (p : x ≡ y)(q : z ≡ w) → (f : Hom[ x , z ])(g : Hom[ y , w ]) @@ -109,6 +114,22 @@ module _ {C : Category ℓC ℓC'} where open isUnivalent isUnivC + + transportIsoToPath : {x y z : ob}(f : C [ x , y ])(p : CatIso C y z) + → PathP (λ i → C [ x , CatIsoToPath p i ]) f (f ⋆ p .fst) + transportIsoToPath f p i = + hcomp (λ j → λ + { (i = i0) → f + ; (i = i1) → f ⋆ secEq (univEquiv _ _) p j .fst }) + (transportPathToIso f (CatIsoToPath p) i) + + transportIsoToPathIso : {x y z : ob}(f : CatIso C x y)(p : CatIso C y z) + → PathP (λ i → CatIso C x (CatIsoToPath p i)) f (⋆Iso f p) + transportIsoToPathIso f p i .fst = transportIsoToPath (f .fst) p i + transportIsoToPathIso f p i .snd = + isProp→PathP (λ i → isPropIsIso (transportIsoToPath (f .fst) p i)) (f .snd) (⋆Iso f p .snd) i + + isoToPath-Square : {x y z w : ob} → (p : CatIso C x y)(q : CatIso C z w) → (f : Hom[ x , z ])(g : Hom[ y , w ]) diff --git a/Cubical/Categories/RezkCompletion.agda b/Cubical/Categories/RezkCompletion.agda new file mode 100644 index 0000000000..67c6e06df2 --- /dev/null +++ b/Cubical/Categories/RezkCompletion.agda @@ -0,0 +1,5 @@ +{-# OPTIONS --safe #-} + +module Cubical.Categories.RezkCompletion where + +open import Cubical.Categories.RezkCompletion.Base public diff --git a/Cubical/Categories/RezkCompletion/Base.agda b/Cubical/Categories/RezkCompletion/Base.agda new file mode 100644 index 0000000000..f2c869751a --- /dev/null +++ b/Cubical/Categories/RezkCompletion/Base.agda @@ -0,0 +1,46 @@ +{- + +The Rezk Completion + +-} +{-# OPTIONS --safe #-} + +module Cubical.Categories.RezkCompletion.Base where + +open import Cubical.Foundations.Prelude + +open import Cubical.Categories.Category +open import Cubical.Categories.Functor +open import Cubical.Categories.Equivalence +open import Cubical.Categories.Equivalence.WeakEquivalence +open import Cubical.Categories.Instances.Functors + +private + variable + ℓC ℓC' ℓD ℓD' : Level + C : Category ℓC ℓC' + D : Category ℓD ℓD' + +-- Rezk Completion of a given category is the initial functor from it towards univalent categories. + +-- It's a bit technical to formulate the universal property of Rezk completion, +-- because the universal property is naturally universal polymorphic, +-- and so the predicate is not inside any universe of finite level. + +-- The product type with one parameter in Typeω +record _×_ {a} (A : Type a) (B : Typeω) : Typeω where + constructor _,_ + field + fst : A + snd : B + +isRezkCompletion : (F : Functor C D) → Typeω +isRezkCompletion {D = D} F = isUnivalent D × ({ℓ ℓ' : Level}{E : Category ℓ ℓ'} → isUnivalent E → isEquivalence (precomposeF E F)) + +-- The critrion of being Rezk completion, c.f. HoTT Book Chapter 9.9. + +open _×_ + +makeIsRezkCompletion : {F : Functor C D} → isUnivalent D → isWeakEquivalence F → isRezkCompletion F +makeIsRezkCompletion univ w-equiv .fst = univ +makeIsRezkCompletion univ w-equiv .snd univE = {!!} diff --git a/Cubical/Foundations/HLevels.agda b/Cubical/Foundations/HLevels.agda index 8ac4970082..5568a513c6 100644 --- a/Cubical/Foundations/HLevels.agda +++ b/Cubical/Foundations/HLevels.agda @@ -36,6 +36,7 @@ private D : (x : A) (y : B x) → C x y → Type ℓ E : (x : A) (y : B x) → (z : C x y) → D x y z → Type ℓ F : (x : A) (y : B x) (z : C x y) (w : D x y z) (v : E x y z w) → Type ℓ + G : (x : A) (y : B x) (z : C x y) (w : D x y z) (v : E x y z w) (u : F x y z w v) → Type ℓ w x y z : A n : HLevel @@ -433,9 +434,13 @@ isPropΠ4 : (h : (x : A) (y : B x) (z : C x y) (w : D x y z) → isProp (E x y z isPropΠ4 h = isPropΠ λ _ → isPropΠ3 (h _) isPropΠ5 : (h : (x : A) (y : B x) (z : C x y) (w : D x y z) (v : E x y z w) → isProp (F x y z w v)) - → isProp ((x : A) (y : B x) (z : C x y) (w : D x y z) (v : E x y z w) → F x y z w v) + → isProp ((x : A) (y : B x) (z : C x y) (w : D x y z) (v : E x y z w) → F x y z w v) isPropΠ5 h = isPropΠ λ _ → isPropΠ4 (h _) +isPropΠ6 : (h : (x : A) (y : B x) (z : C x y) (w : D x y z) (v : E x y z w) (u : F x y z w v) → isProp (G x y z w v u)) + → isProp ((x : A) (y : B x) (z : C x y) (w : D x y z) (v : E x y z w) (u : F x y z w v) → G x y z w v u) +isPropΠ6 h = isPropΠ λ _ → isPropΠ5 (h _) + isPropImplicitΠ : (h : (x : A) → isProp (B x)) → isProp ({x : A} → B x) isPropImplicitΠ h f g i {x} = h x (f {x}) (g {x}) i From b1da2985789012bbded665a98a035e18d03e1d8b Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Thu, 9 Jun 2022 08:08:59 +0800 Subject: [PATCH 14/18] more --- .../Categories/Functor/ComposeProperty.agda | 180 ++++++++++++++++-- .../PropositionalTruncation/Properties.agda | 6 + 2 files changed, 173 insertions(+), 13 deletions(-) diff --git a/Cubical/Categories/Functor/ComposeProperty.agda b/Cubical/Categories/Functor/ComposeProperty.agda index 052315ff1b..ab677d05db 100644 --- a/Cubical/Categories/Functor/ComposeProperty.agda +++ b/Cubical/Categories/Functor/ComposeProperty.agda @@ -4,6 +4,8 @@ module Cubical.Categories.Functor.ComposeProperty where open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Equiv + open import Cubical.Data.Sigma open import Cubical.HITs.PropositionalTruncation as Prop @@ -16,7 +18,7 @@ open import Cubical.Categories.Equivalence.WeakEquivalence open import Cubical.Categories.Instances.Functors --- Composition induced by special functors +-- Composition by functor with special properties module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (E : Category ℓE ℓE') @@ -29,6 +31,8 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} open isIso + -- If F is essential surjective, (- ∘ F) is faithful. + isEssSurj→isFaithfulPrecomp : isEssentiallySurj F → isFaithful (precomposeF E F) isEssSurj→isFaithfulPrecomp surj A B α β p = makeNatTransPath @@ -40,6 +44,8 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} (surj x) i) + -- If F is essential surjective and full, (- ∘ F) is full. + isEssSurj+Full→isFullPrecomp : isEssentiallySurj F → isFull F → isFull (precomposeF E F) isEssSurj+Full→isFullPrecomp surj full A B α = ∣ ext , ext≡ ∣₁ where @@ -125,6 +131,8 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} ∙ E .⋆IdR _ ∙ E .⋆IdL _) i) + -- As a corollary, if F is essential surjective and full, (- ∘ F) is fully faithfull. + isEssSurj+Full→isFullyFaithfulPrecomp : isEssentiallySurj F → isFull F → isFullyFaithful (precomposeF E F) isEssSurj+Full→isFullyFaithfulPrecomp surj full = isFull+Faithful→isFullyFaithful {F = precomposeF E F} @@ -144,6 +152,9 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} open isWeakEquivalence open isUnivalent isUnivE + + -- If F is weak equivalence and the target category is univalent, (- ∘ F) is essentially surjective. + isWeakEquiv→isEssSurjPrecomp : isWeakEquivalence F → isEssentiallySurj (precomposeF E F) isWeakEquiv→isEssSurjPrecomp w-equiv G = {!!} where @@ -155,36 +166,41 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} → F .F-hom f ⋆⟨ D ⟩ h' .fst ≡ h .fst → G .F-hom f ⋆⟨ E ⟩ k c' h' .fst ≡ k c h .fst) - module _ (d : D .ob)(c₀ : C .ob)(h₀ : CatIso D (F .F-ob c₀) d) where + module _ {d} {c c'} (h : CatIso D (F .F-ob c) d)(h' : CatIso D (F .F-ob c') d) where + + liftH : CatIso C c c' + liftH = liftIso {F = F} (w-equiv .fullfaith) (⋆Iso h (invIso h')) - g : (c : C .ob)(h : CatIso D (F .F-ob c) d) → CatIso C c c₀ - g c h = liftIso {F = F} (w-equiv .fullfaith) (⋆Iso h (invIso h₀)) + liftH-eq' : F .F-hom (liftH .fst) ≡ h .fst ⋆⟨ D ⟩ h' .snd .inv + liftH-eq' = cong fst (liftIso≡ {F = F} (w-equiv .fullfaith) (⋆Iso h (invIso h'))) - g-eq : ∀ c h → F .F-hom (g c h .fst) ⋆⟨ D ⟩ h₀ .fst ≡ h .fst - g-eq c h = - cong (λ x → x ⋆⟨ D ⟩ _) (cong fst (liftIso≡ {F = F} (w-equiv .fullfaith) (⋆Iso h (invIso h₀)))) + liftH-eq : F .F-hom (liftH .fst) ⋆⟨ D ⟩ h' .fst ≡ h .fst + liftH-eq = + cong (λ x → x ⋆⟨ D ⟩ _) liftH-eq' ∙ D .⋆Assoc _ _ _ - ∙ cong (λ x → _ ⋆⟨ D ⟩ x) (h₀ .snd .sec) + ∙ cong (λ x → _ ⋆⟨ D ⟩ x) (h' .snd .sec) ∙ D .⋆IdR _ + module _ (d : D .ob)(c₀ : C .ob)(h₀ : CatIso D (F .F-ob c₀) d) where + isContrObj' : isContr (Obj d) isContrObj' .fst .fst = G .F-ob c₀ - isContrObj' .fst .snd .fst c h = F-Iso {F = G} (g c h) + isContrObj' .fst .snd .fst c h = F-Iso {F = G} (liftH h h₀) isContrObj' .fst .snd .snd c c' h h' f p = sym (G .F-seq _ _) ∙ cong (G .F-hom) g-path where - g-path : f ⋆⟨ C ⟩ g c' h' .fst ≡ g c h .fst + g-path : f ⋆⟨ C ⟩ liftH h' h₀ .fst ≡ liftH h h₀ .fst g-path = isFullyFaithful→Faithful {F = F} (w-equiv .fullfaith) _ _ _ _ (F .F-seq _ _ - ∙ cong (λ x → _ ⋆⟨ D ⟩ x) (cong fst (liftIso≡ {F = F} (w-equiv .fullfaith) (⋆Iso h' (invIso h₀)))) + ∙ cong (λ x → _ ⋆⟨ D ⟩ x) (liftH-eq' h' h₀) ∙ sym (D .⋆Assoc _ _ _) ∙ cong (λ x → x ⋆⟨ D ⟩ invIso h₀ .fst) p ∙ cong fst (sym (liftIso≡ {F = F} (w-equiv .fullfaith) (⋆Iso h (invIso h₀))))) isContrObj' .snd (e , k , coh) i .fst = CatIsoToPath (k c₀ h₀) i isContrObj' .snd (e , k , coh) i .snd .fst c h = - let isom₀ = F-Iso {F = G} (g c h) in + let isom₀ = F-Iso {F = G} (liftH h h₀) in hcomp (λ j → λ { (i = i0) → isom₀ - ; (i = i1) → CatIso≡ (⋆Iso isom₀ (k c₀ h₀)) (k c h) (coh c c₀ h h₀ (g c h .fst) (g-eq c h)) j }) + ; (i = i1) → CatIso≡ (⋆Iso isom₀ (k c₀ h₀)) (k c h) (coh c c₀ h h₀ (liftH h h₀ .fst) (liftH-eq h h₀)) j }) (transportIsoToPathIso isUnivE isom₀ _ i) isContrObj' .snd x@(e , k , coh) i .snd .snd = isProp→PathP (λ i → isPropΠ6 (λ c c' h h' f _ → @@ -198,3 +214,141 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} Ext-ob : D .ob → E .ob Ext-ob d = isContrObj d .fst .fst + + k : {d : D .ob}{c : C .ob}(h : CatIso D (F .F-ob c) d) → CatIso E (G .F-ob c) (Ext-ob d) + k = isContrObj _ .fst .snd .fst _ + + k-eq : {d : D .ob}{c c' : C .ob} + (h : CatIso D (F .F-ob c) d)(h' : CatIso D (F .F-ob c') d) + → (f : C [ c , c' ]) + → F .F-hom f ⋆⟨ D ⟩ h' .fst ≡ h .fst + → G .F-hom f ⋆⟨ E ⟩ k h' .fst ≡ k h .fst + k-eq = isContrObj _ .fst .snd .snd _ _ + + Mor : (d d' : D .ob)(f : D [ d , d' ]) → Type _ + Mor d d' f = + Σ[ g ∈ E [ Ext-ob d , Ext-ob d' ] ] + ((c c' : C .ob)(h : CatIso D (F .F-ob c) d)(h' : CatIso D (F .F-ob c') d') + → (l : C [ c , c' ]) + → F .F-hom l ⋆⟨ D ⟩ h' .fst ≡ h .fst ⋆⟨ D ⟩ f + → G .F-hom l ⋆⟨ E ⟩ k h' .fst ≡ k h .fst ⋆⟨ E ⟩ g) + + module _ (d d' : D .ob)(f : D [ d , d' ]) + (c₀ : C .ob)(h₀ : CatIso D (F .F-ob c₀) d ) + (c₁ : C .ob)(h₁ : CatIso D (F .F-ob c₁) d') + (l₀ : C [ c₀ , c₁ ])(p₀ : F .F-hom l₀ ⋆⟨ D ⟩ h₁ .fst ≡ h₀ .fst ⋆⟨ D ⟩ f) + where + + g₀ = k h₀ .snd .inv ⋆⟨ E ⟩ G .F-hom l₀ ⋆⟨ E ⟩ k h₁ .fst + + isContrMor' : isContr (Mor d d' f) + isContrMor' .fst .fst = g₀ + isContrMor' .fst .snd c c' h h' l p = + cong (λ x → _ ⋆⟨ E ⟩ x) (⋆InvLMove (F-Iso {F = G} m') (k-eq h₁ h' _ m'-eq)) + ∙ sym (E .⋆Assoc _ _ _) + ∙ cong (λ x → x ⋆⟨ E ⟩ k h₁ .fst) Gm-path' + ∙ cong (λ x → x ⋆⟨ E ⟩ G .F-hom l₀ ⋆⟨ E ⟩ k h₁ .fst) m-eq' + ∙ E .⋆Assoc _ _ _ ∙ E .⋆Assoc _ _ _ + ∙ cong (λ x → k h .fst ⋆⟨ E ⟩ x) (sym (E .⋆Assoc _ _ _)) + where + m = liftH h₀ h + m-eq = liftH-eq h₀ h + m' = liftH h₁ h' + m'-eq = liftH-eq h₁ h' + + m-eq' : G .F-hom (m .snd .inv) ≡ k h .fst ⋆⟨ E ⟩ k h₀ .snd .inv + m-eq' = ⋆InvRMove (k h₀) (sym (⋆InvLMove (F-Iso {F = G} m) (k-eq h₀ h _ m-eq))) + + Fm-path : F .F-hom (l₀ ⋆⟨ C ⟩ m' .fst) ≡ F .F-hom (m .fst ⋆⟨ C ⟩ l) + Fm-path = + F .F-seq _ _ + ∙ cong (λ x → F .F-hom l₀ ⋆⟨ D ⟩ x) (liftH-eq' h₁ h') + ∙ sym (D .⋆Assoc _ _ _) + ∙ cong (λ x → x ⋆⟨ D ⟩ _) p₀ + ∙ cong (λ x → x ⋆⟨ D ⟩ _ ⋆⟨ D ⟩ _) (sym (D .⋆IdR _)) + ∙ cong (λ x → _ ⋆⟨ D ⟩ x ⋆⟨ D ⟩ _ ⋆⟨ D ⟩ _) (sym (h .snd .sec)) + ∙ cong (λ x → x ⋆⟨ D ⟩ _ ⋆⟨ D ⟩ _) (sym (D .⋆Assoc _ _ _)) + ∙ cong (λ x → x ⋆⟨ D ⟩ _) (D .⋆Assoc _ _ _) + ∙ D .⋆Assoc _ _ _ + ∙ (λ i → ⋆InvRMove h m-eq (~ i) ⋆⟨ D ⟩ ⋆InvRMove h' p (~ i)) + ∙ sym (F .F-seq _ _) + + m-path : l₀ ⋆⟨ C ⟩ m' .fst ≡ m .fst ⋆⟨ C ⟩ l + m-path = isFullyFaithful→Faithful {F = F} (w-equiv .fullfaith) _ _ _ _ Fm-path + + Gm-path : G .F-hom l₀ ⋆⟨ E ⟩ G .F-hom (m' .fst) ≡ G .F-hom (m .fst) ⋆⟨ E ⟩ G .F-hom l + Gm-path = sym (G .F-seq _ _) ∙ cong (G .F-hom) m-path ∙ G .F-seq _ _ + + Gm-path' : G .F-hom l ⋆⟨ E ⟩ G .F-hom (m' .snd .inv) ≡ G .F-hom (m .snd .inv) ⋆⟨ E ⟩ G .F-hom l₀ + Gm-path' = ⋆InvLMove (F-Iso {F = G} m) (sym (⋆InvRMove (F-Iso {F = G} m') Gm-path ∙ E .⋆Assoc _ _ _)) + + isContrMor' .snd (g₁ , coh₁) i .fst = + (⋆InvLMove (k h₀) (sym (isContrMor' .fst .snd c₀ c₁ h₀ h₁ l₀ p₀)) + ∙ sym (⋆InvLMove (k h₀) (sym (coh₁ c₀ c₁ h₀ h₁ l₀ p₀)))) i + isContrMor' .snd x@(g₁ , coh₁) i .snd = + isProp→PathP (λ i → isPropΠ6 (λ c c' h h' l _ → + E .isSetHom + (G .F-hom l ⋆⟨ E ⟩ k h' .fst) + (k h .fst ⋆⟨ E ⟩ isContrMor' .snd x i .fst))) + (isContrMor' .fst .snd) coh₁ i + + module _ {c c'} {d d'} + (f : D [ d , d' ])(h : CatIso D (F .F-ob c) d)(h' : CatIso D (F .F-ob c') d') + where + + liftL : C [ c , c' ] + liftL = invEq (_ , w-equiv .fullfaith _ _) (h .fst ⋆⟨ D ⟩ f ⋆⟨ D ⟩ h' .snd .inv) + + liftL-eq : F .F-hom liftL ⋆⟨ D ⟩ h' .fst ≡ h .fst ⋆⟨ D ⟩ f + liftL-eq = + sym (⋆InvRMove (invIso h') + (sym (secEq (_ , w-equiv .fullfaith _ _) (h .fst ⋆⟨ D ⟩ f ⋆⟨ D ⟩ h' .snd .inv)))) + + isContrMor : (d d' : D .ob)(f : D [ d , d' ]) → isContr (Mor d d' f) + isContrMor d d' f = Prop.rec2 isPropIsContr + (λ (c₀ , h₀) (c₁ , h₁) → + isContrMor' d d' f c₀ h₀ c₁ h₁ (liftL f h₀ h₁) (liftL-eq f h₀ h₁)) + (w-equiv .esssurj d) (w-equiv .esssurj d') + + Ext-hom : {d d' : D .ob}(f : D [ d , d' ]) → E [ Ext-ob d , Ext-ob d' ] + Ext-hom f = isContrMor _ _ f .fst .fst + + liftL⋆ : ∀ {c c' c''} {d d' d''} + (f : D [ d , d' ])(g : D [ d' , d'' ]) + (h : CatIso D (F .F-ob c) d)(h' : CatIso D (F .F-ob c') d')(h'' : CatIso D (F .F-ob c'') d'') + → liftL (f ⋆⟨ D ⟩ g) h h'' ≡ liftL f h h' ⋆⟨ C ⟩ liftL g h' h'' + liftL⋆ f g h h' h'' = isFullyFaithful→Faithful {F = F} (w-equiv .fullfaith) _ _ _ _ + (⋆CancelR h'' path ∙ sym (F .F-seq _ _)) + where + path : _ + path = liftL-eq (f ⋆⟨ D ⟩ g) h h'' + ∙ sym (D .⋆Assoc _ _ _) + ∙ cong (λ x → x ⋆⟨ D ⟩ _) (sym (liftL-eq f h h')) + ∙ D .⋆Assoc _ _ _ + ∙ cong (λ x → F .F-hom (liftL f h h') ⋆⟨ D ⟩ x) (sym (liftL-eq g h' h'')) + ∙ sym (D .⋆Assoc _ _ _) + + Ext : Functor D E + Ext .F-ob = Ext-ob + Ext .F-hom = Ext-hom + Ext .F-id {x = d} = Prop.rec (E .isSetHom _ _) + (λ (c , h) → + let r = isContrMor _ _ (D .id {x = d}) .fst .snd _ _ h h (C .id) + (cong (λ x → x ⋆⟨ D ⟩ _) (F .F-id) ∙ D .⋆IdL _ ∙ sym (D .⋆IdR _)) + in ⋆CancelL (k h) (sym r ∙ cong (λ x → x ⋆⟨ E ⟩ (k h .fst)) (G .F-id) ∙ E .⋆IdL _ ∙ sym (E .⋆IdR _))) + (w-equiv .esssurj d) + Ext .F-seq {x = a} {y = b} {z = c} f g = + Prop.rec3 (E .isSetHom _ _) + (λ (_ , ha) (_ , hb) (_ , hc) → + let rf = isContrMor _ _ _ .fst .snd _ _ ha hb (liftL f ha hb) (liftL-eq f ha hb) + rg = isContrMor _ _ _ .fst .snd _ _ hb hc (liftL g hb hc) (liftL-eq g hb hc) + rfg = isContrMor _ _ _ .fst .snd _ _ ha hc (liftL (f ⋆⟨ D ⟩ g) ha hc) (liftL-eq (f ⋆⟨ D ⟩ g) ha hc) + in ⋆CancelL (k ha) + (sym rfg + ∙ cong (λ x → x ⋆⟨ E ⟩ k hc .fst) (cong (G .F-hom) (liftL⋆ f g ha hb hc) ∙ G .F-seq _ _) + ∙ E .⋆Assoc _ _ _ + ∙ cong (λ x → G .F-hom _ ⋆⟨ E ⟩ x) rg + ∙ sym (E .⋆Assoc _ _ _) + ∙ cong (λ x → x ⋆⟨ E ⟩ Ext-hom g) rf + ∙ E .⋆Assoc _ _ _)) + (w-equiv .esssurj a) (w-equiv .esssurj b) (w-equiv .esssurj c) diff --git a/Cubical/HITs/PropositionalTruncation/Properties.agda b/Cubical/HITs/PropositionalTruncation/Properties.agda index 2be49c28b9..e71ed7cbee 100644 --- a/Cubical/HITs/PropositionalTruncation/Properties.agda +++ b/Cubical/HITs/PropositionalTruncation/Properties.agda @@ -40,6 +40,12 @@ rec2 Pprop f ∣ x ∣₁ ∣ y ∣₁ = f x y rec2 Pprop f ∣ x ∣₁ (squash₁ y z i) = Pprop (rec2 Pprop f ∣ x ∣₁ y) (rec2 Pprop f ∣ x ∣₁ z) i rec2 Pprop f (squash₁ x y i) z = Pprop (rec2 Pprop f x z) (rec2 Pprop f y z) i +rec3 : {P : Type ℓ} → isProp P → (A → B → C → P) → ∥ A ∥₁ → ∥ B ∥₁ → ∥ C ∥₁ → P +rec3 Pprop f ∣ x ∣₁ ∣ y ∣₁ ∣ z ∣₁ = f x y z +rec3 Pprop f ∣ x ∣₁ ∣ y ∣₁ (squash₁ z w i) = Pprop (rec3 Pprop f ∣ x ∣₁ ∣ y ∣₁ z) (rec3 Pprop f ∣ x ∣₁ ∣ y ∣₁ w) i +rec3 Pprop f ∣ x ∣₁ (squash₁ y z i) w = Pprop (rec3 Pprop f ∣ x ∣₁ y w) (rec3 Pprop f ∣ x ∣₁ z w) i +rec3 Pprop f (squash₁ x y i) z w = Pprop (rec3 Pprop f x z w) (rec3 Pprop f y z w) i + -- Old version -- rec2 : ∀ {P : Type ℓ} → isProp P → (A → A → P) → ∥ A ∥ → ∥ A ∥ → P -- rec2 Pprop f = rec (isProp→ Pprop) (λ a → rec Pprop (f a)) From dbd2cd98aafec58ca9900ebbcbc4cd4e0910fc16 Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Thu, 9 Jun 2022 10:09:46 +0800 Subject: [PATCH 15/18] done --- .../Categories/Functor/ComposeProperty.agda | 80 +++++++++++++++++-- Cubical/Categories/Instances/Functors.agda | 5 +- Cubical/Categories/RezkCompletion/Base.agda | 3 +- 3 files changed, 79 insertions(+), 9 deletions(-) diff --git a/Cubical/Categories/Functor/ComposeProperty.agda b/Cubical/Categories/Functor/ComposeProperty.agda index ab677d05db..a7e8380ff4 100644 --- a/Cubical/Categories/Functor/ComposeProperty.agda +++ b/Cubical/Categories/Functor/ComposeProperty.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe #-} +{-# OPTIONS --safe --experimental-lossy-unification #-} module Cubical.Categories.Functor.ComposeProperty where @@ -13,6 +13,7 @@ open import Cubical.Categories.Category open import Cubical.Categories.Isomorphism open import Cubical.Categories.Functor open import Cubical.Categories.NaturalTransformation.Base +open import Cubical.Categories.Equivalence open import Cubical.Categories.Equivalence.WeakEquivalence open import Cubical.Categories.Instances.Functors @@ -131,12 +132,12 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} ∙ E .⋆IdR _ ∙ E .⋆IdL _) i) - -- As a corollary, if F is essential surjective and full, (- ∘ F) is fully faithfull. + -- As a corollary, if F is essential surjective and full, (- ∘ F) is fully faithfull. - isEssSurj+Full→isFullyFaithfulPrecomp : isEssentiallySurj F → isFull F → isFullyFaithful (precomposeF E F) - isEssSurj+Full→isFullyFaithfulPrecomp surj full = - isFull+Faithful→isFullyFaithful {F = precomposeF E F} - (isEssSurj+Full→isFullPrecomp surj full) (isEssSurj→isFaithfulPrecomp surj) + isEssSurj+Full→isFullyFaithfulPrecomp : isEssentiallySurj F → isFull F → isFullyFaithful (precomposeF E F) + isEssSurj+Full→isFullyFaithfulPrecomp surj full = + isFull+Faithful→isFullyFaithful {F = precomposeF E F} + (isEssSurj+Full→isFullPrecomp surj full) (isEssSurj→isFaithfulPrecomp surj) module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} @@ -156,7 +157,7 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} -- If F is weak equivalence and the target category is univalent, (- ∘ F) is essentially surjective. isWeakEquiv→isEssSurjPrecomp : isWeakEquivalence F → isEssentiallySurj (precomposeF E F) - isWeakEquiv→isEssSurjPrecomp w-equiv G = {!!} + isWeakEquiv→isEssSurjPrecomp w-equiv G = ∣ Ext , Ext≃ ∣₁ where Obj : (d : D .ob) → Type _ Obj d = Σ[ e ∈ E .ob ] @@ -352,3 +353,68 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} ∙ cong (λ x → x ⋆⟨ E ⟩ Ext-hom g) rf ∙ E .⋆Assoc _ _ _)) (w-equiv .esssurj a) (w-equiv .esssurj b) (w-equiv .esssurj c) + + objFc : (c : C .ob) → Obj (F .F-ob c) + objFc c₀ .fst = G .F-ob c₀ + objFc c₀ .snd .fst c h = F-Iso {F = G} (liftIso {F = F} (w-equiv .fullfaith) h) + objFc c₀ .snd .snd c c' h h' f p = sym (G .F-seq _ _) + ∙ cong (G .F-hom) (isFullyFaithful→Faithful {F = F} (w-equiv .fullfaith) _ _ _ _ path) + where + path : _ + path = + F .F-seq _ _ + ∙ cong (λ x → _ ⋆⟨ D ⟩ x) (cong fst (liftIso≡ {F = F} (w-equiv .fullfaith) h')) + ∙ p ∙ sym (cong fst (liftIso≡ {F = F} (w-equiv .fullfaith) h)) + + Ext-ob≡ : (c : C .ob) → Ext-ob (F .F-ob c) ≡ G .F-ob c + Ext-ob≡ c₀ = cong fst (isContrObj _ .snd (objFc c₀)) + + Ext-hom≡ : {c c' : C .ob}(f : C [ c , c' ]) + → PathP (λ i → E [ Ext-ob≡ c i , Ext-ob≡ c' i ]) (Ext-hom (F .F-hom f)) (G .F-hom f) + Ext-hom≡ {c = c} {c' = c'} f i = + hcomp (λ j → λ + { (i = i0) → isContrMor _ _ _ .snd morFf (~ j) .fst + ; (i = i1) → G .F-hom f }) + (transpGf-filler (~ i)) + where + transpGf-filler = transport-filler (λ i → E [ Ext-ob≡ c (~ i) , Ext-ob≡ c' (~ i) ]) (G .F-hom f) + + morFf : Mor _ _ (F .F-hom f) + morFf .fst = transpGf-filler i1 + morFf .snd c c' h h' l p = + transport (λ i → G .F-hom l ⋆⟨ E ⟩ isContrObj _ .snd (objFc _) (~ i) .snd .fst c' h' .fst + ≡ isContrObj _ .snd (objFc _) (~ i) .snd .fst c h .fst ⋆⟨ E ⟩ transpGf-filler i) G-path + where + F-path : _ + F-path = + F .F-seq _ _ + ∙ cong (λ x → _ ⋆⟨ D ⟩ x) (cong fst (liftIso≡ {F = F} (w-equiv .fullfaith) h')) ∙ p + ∙ cong (λ x → x ⋆⟨ D ⟩ _) (sym (cong fst (liftIso≡ {F = F} (w-equiv .fullfaith) h))) + ∙ sym (F .F-seq _ _) + + G-path : _ + G-path = + sym (G .F-seq _ _) + ∙ cong (G .F-hom) (isFullyFaithful→Faithful {F = F} (w-equiv .fullfaith) _ _ _ _ F-path) + ∙ G .F-seq _ _ + + Ext≡ : precomposeF E F .F-ob Ext ≡ G + Ext≡ = Functor≡ Ext-ob≡ Ext-hom≡ + + Ext≃ : CatIso _ (precomposeF E F .F-ob Ext) G + Ext≃ = NatIso→Iso _ _ (pathToNatIso Ext≡) + + + -- As a corollary, if F is weak equivalence and the target category is univalent, (- ∘ F) is an weak equivalence. + + isWeakEquiv→isWeakEquivPrecomp : isWeakEquivalence F → isWeakEquivalence (precomposeF E F) + isWeakEquiv→isWeakEquivPrecomp w-equiv .fullfaith = + isEssSurj+Full→isFullyFaithfulPrecomp E F (w-equiv .esssurj) (isFullyFaithful→Full {F = F} (w-equiv .fullfaith)) + isWeakEquiv→isWeakEquivPrecomp w-equiv .esssurj = isWeakEquiv→isEssSurjPrecomp w-equiv + + -- Moreover, using assumption of being univalent, (- ∘ F) is actually an equivalence. + + isWeakEquiv→isEquivPrecomp : isWeakEquivalence F → isEquivalence (precomposeF E F) + isWeakEquiv→isEquivPrecomp w-equiv = + isWeakEquiv→isEquiv (isUnivalentFUNCTOR _ _ isUnivE) (isUnivalentFUNCTOR _ _ isUnivE) + (isWeakEquiv→isWeakEquivPrecomp w-equiv) diff --git a/Cubical/Categories/Instances/Functors.agda b/Cubical/Categories/Instances/Functors.agda index af8cf9285d..db2aaa8a69 100644 --- a/Cubical/Categories/Instances/Functors.agda +++ b/Cubical/Categories/Instances/Functors.agda @@ -70,6 +70,9 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where Iso→NatIso α .trans = α .fst Iso→NatIso α .nIso = FUNCTORIso' _ (α .snd) + NatIso→Iso : {F G : Functor C D} → NatIso F G → CatIso FUNCTOR F G + NatIso→Iso α = α .trans , FUNCTORIso _ (α .nIso) + Path→Iso→NatIso : {F G : Functor C D} → (p : F ≡ G) → pathToNatIso p ≡ Iso→NatIso (pathToIso p) Path→Iso→NatIso {F = F} p = J (λ _ p → pathToNatIso p ≡ Iso→NatIso (pathToIso p)) (NatIso≡ refl-helper) p where @@ -79,7 +82,7 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where Iso-FUNCTORIso-NatIso : {F G : Functor C D} → Iso (CatIso FUNCTOR F G) (NatIso F G) Iso-FUNCTORIso-NatIso .fun = Iso→NatIso - Iso-FUNCTORIso-NatIso .inv α = α .trans , FUNCTORIso _ (α .nIso) + Iso-FUNCTORIso-NatIso .inv = NatIso→Iso Iso-FUNCTORIso-NatIso .rightInv α i .trans = α .trans Iso-FUNCTORIso-NatIso .rightInv α i .nIso = isProp→PathP (λ i → isPropΠ (λ _ → isPropIsIso _)) (FUNCTORIso' (α .trans) (FUNCTORIso _ (α .nIso))) (α .nIso) i diff --git a/Cubical/Categories/RezkCompletion/Base.agda b/Cubical/Categories/RezkCompletion/Base.agda index f2c869751a..9adffd08e0 100644 --- a/Cubical/Categories/RezkCompletion/Base.agda +++ b/Cubical/Categories/RezkCompletion/Base.agda @@ -11,6 +11,7 @@ open import Cubical.Foundations.Prelude open import Cubical.Categories.Category open import Cubical.Categories.Functor +open import Cubical.Categories.Functor.ComposeProperty open import Cubical.Categories.Equivalence open import Cubical.Categories.Equivalence.WeakEquivalence open import Cubical.Categories.Instances.Functors @@ -43,4 +44,4 @@ open _×_ makeIsRezkCompletion : {F : Functor C D} → isUnivalent D → isWeakEquivalence F → isRezkCompletion F makeIsRezkCompletion univ w-equiv .fst = univ -makeIsRezkCompletion univ w-equiv .snd univE = {!!} +makeIsRezkCompletion univ w-equiv .snd univE = isWeakEquiv→isEquivPrecomp univE _ w-equiv From 4f21e54db096d6a653da4aa31a5849da79c92577 Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Thu, 9 Jun 2022 11:39:59 +0800 Subject: [PATCH 16/18] done --- .../Constructions/EssentialImage.agda | 63 ++++++++++++++++++ .../Constructions/FullSubcategory.agda | 65 +++++++++++++++++++ .../Equivalence/WeakEquivalence.agda | 2 +- Cubical/Categories/Functor/Properties.agda | 4 +- Cubical/Categories/RezkCompletion/Base.agda | 8 +-- 5 files changed, 135 insertions(+), 7 deletions(-) create mode 100644 Cubical/Categories/Constructions/EssentialImage.agda diff --git a/Cubical/Categories/Constructions/EssentialImage.agda b/Cubical/Categories/Constructions/EssentialImage.agda new file mode 100644 index 0000000000..282e6023ec --- /dev/null +++ b/Cubical/Categories/Constructions/EssentialImage.agda @@ -0,0 +1,63 @@ +{- + +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 + + + isUnivalentEssentialImage : isUnivalent D → isUnivalent EssentialImage + isUnivalentEssentialImage = isUnivalentFullSub _ isPropIsInEssentialImage diff --git a/Cubical/Categories/Constructions/FullSubcategory.agda b/Cubical/Categories/Constructions/FullSubcategory.agda index b9daf4ca5d..f05b966ea7 100644 --- a/Cubical/Categories/Constructions/FullSubcategory.agda +++ b/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)) diff --git a/Cubical/Categories/Equivalence/WeakEquivalence.agda b/Cubical/Categories/Equivalence/WeakEquivalence.agda index 974b6bcbd8..deed6b4b13 100644 --- a/Cubical/Categories/Equivalence/WeakEquivalence.agda +++ b/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 diff --git a/Cubical/Categories/Functor/Properties.agda b/Cubical/Categories/Functor/Properties.agda index 336139f556..90c64870a5 100644 --- a/Cubical/Categories/Functor/Properties.agda +++ b/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 _ _) diff --git a/Cubical/Categories/RezkCompletion/Base.agda b/Cubical/Categories/RezkCompletion/Base.agda index 9adffd08e0..3c9f571521 100644 --- a/Cubical/Categories/RezkCompletion/Base.agda +++ b/Cubical/Categories/RezkCompletion/Base.agda @@ -29,19 +29,19 @@ private -- and so the predicate is not inside any universe of finite level. -- The product type with one parameter in Typeω -record _×_ {a} (A : Type a) (B : Typeω) : Typeω where +record _×ω_ {a} (A : Type a) (B : Typeω) : Typeω where constructor _,_ field fst : A snd : B +open _×ω_ public + isRezkCompletion : (F : Functor C D) → Typeω -isRezkCompletion {D = D} F = isUnivalent D × ({ℓ ℓ' : Level}{E : Category ℓ ℓ'} → isUnivalent E → isEquivalence (precomposeF E F)) +isRezkCompletion {D = D} F = isUnivalent D ×ω ({ℓ ℓ' : Level}{E : Category ℓ ℓ'} → isUnivalent E → isEquivalence (precomposeF E F)) -- The critrion of being Rezk completion, c.f. HoTT Book Chapter 9.9. -open _×_ - makeIsRezkCompletion : {F : Functor C D} → isUnivalent D → isWeakEquivalence F → isRezkCompletion F makeIsRezkCompletion univ w-equiv .fst = univ makeIsRezkCompletion univ w-equiv .snd univE = isWeakEquiv→isEquivPrecomp univE _ w-equiv From 7f758e9719bf984ec00ca04e08238d94f2bbcf98 Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Thu, 9 Jun 2022 12:00:46 +0800 Subject: [PATCH 17/18] supplement --- Cubical/Categories/Constructions/EssentialImage.agda | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Cubical/Categories/Constructions/EssentialImage.agda b/Cubical/Categories/Constructions/EssentialImage.agda index 282e6023ec..3ea8f2c8c1 100644 --- a/Cubical/Categories/Constructions/EssentialImage.agda +++ b/Cubical/Categories/Constructions/EssentialImage.agda @@ -59,5 +59,9 @@ module _ isFullyFaithfulFromEssentialImage = isFullyFaithfulIncl D isInEssentialImage + isFullyFaithfulToEssentialImage : isFullyFaithful F → isFullyFaithful ToEssentialImage + isFullyFaithfulToEssentialImage fullfaith = fullfaith + + isUnivalentEssentialImage : isUnivalent D → isUnivalent EssentialImage isUnivalentEssentialImage = isUnivalentFullSub _ isPropIsInEssentialImage From 172322b4df9d1c08f5d839b0babc058f86538ce8 Mon Sep 17 00:00:00 2001 From: KANG Rongji Date: Fri, 12 Aug 2022 07:09:51 +0800 Subject: [PATCH 18/18] modify --- .../Constructions/EssentialImage.agda | 6 +++--- .../Categories/Functor/ComposeProperty.agda | 4 ---- Cubical/Categories/Instances/Functors.agda | 21 ------------------- Cubical/Categories/RezkCompletion/Base.agda | 20 ------------------ Cubical/Foundations/Prelude.agda | 6 +++--- 5 files changed, 6 insertions(+), 51 deletions(-) diff --git a/Cubical/Categories/Constructions/EssentialImage.agda b/Cubical/Categories/Constructions/EssentialImage.agda index 3ea8f2c8c1..cd4eaae49f 100644 --- a/Cubical/Categories/Constructions/EssentialImage.agda +++ b/Cubical/Categories/Constructions/EssentialImage.agda @@ -8,7 +8,7 @@ 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.HITs.PropositionalTruncation as PropTrunc open import Cubical.Categories.Category open import Cubical.Categories.Functor @@ -27,7 +27,7 @@ module _ open Functor - isInEssentialImage : D .ob → Type(ℓ-max ℓC ℓD') + 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) @@ -53,7 +53,7 @@ module _ isEssentiallySurjToEssentialImage : isEssentiallySurj ToEssentialImage - isEssentiallySurjToEssentialImage (d , p) = Prop.map (λ (c , f) → c , Incl-Iso-inv _ _ _ _ f) p + isEssentiallySurjToEssentialImage (d , p) = PropTrunc.map (λ (c , f) → c , Incl-Iso-inv _ _ _ _ f) p isFullyFaithfulFromEssentialImage : isFullyFaithful FromEssentialImage isFullyFaithfulFromEssentialImage = isFullyFaithfulIncl D isInEssentialImage diff --git a/Cubical/Categories/Functor/ComposeProperty.agda b/Cubical/Categories/Functor/ComposeProperty.agda index 381f2d6f07..57face5f4d 100644 --- a/Cubical/Categories/Functor/ComposeProperty.agda +++ b/Cubical/Categories/Functor/ComposeProperty.agda @@ -402,11 +402,7 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} Ext≡ = Functor≡ Ext-ob≡ Ext-hom≡ Ext≃ : CatIso _ (precomposeF E F .F-ob Ext) G -<<<<<<< HEAD - Ext≃ = NatIso→Iso _ _ (pathToNatIso Ext≡) -======= Ext≃ = NatIso→FUNCTORIso _ _ (pathToNatIso Ext≡) ->>>>>>> master -- As a corollary, if F is weak equivalence and the target category is univalent, (- ∘ F) is an weak equivalence. diff --git a/Cubical/Categories/Instances/Functors.agda b/Cubical/Categories/Instances/Functors.agda index c9399f507d..327fb95ede 100644 --- a/Cubical/Categories/Instances/Functors.agda +++ b/Cubical/Categories/Instances/Functors.agda @@ -66,17 +66,6 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where open Iso open NatIso -<<<<<<< HEAD - Iso→NatIso : {F G : Functor C D} → CatIso FUNCTOR F G → NatIso F G - Iso→NatIso α .trans = α .fst - Iso→NatIso α .nIso = FUNCTORIso' _ (α .snd) - - NatIso→Iso : {F G : Functor C D} → NatIso F G → CatIso FUNCTOR F G - NatIso→Iso α = α .trans , FUNCTORIso _ (α .nIso) - - Path→Iso→NatIso : {F G : Functor C D} → (p : F ≡ G) → pathToNatIso p ≡ Iso→NatIso (pathToIso p) - Path→Iso→NatIso {F = F} p = J (λ _ p → pathToNatIso p ≡ Iso→NatIso (pathToIso p)) (NatIso≡ refl-helper) p -======= FUNCTORIso→NatIso : {F G : Functor C D} → CatIso FUNCTOR F G → NatIso F G FUNCTORIso→NatIso α .trans = α .fst FUNCTORIso→NatIso α .nIso = FUNCTORIso' _ (α .snd) @@ -86,20 +75,14 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where Path→FUNCTORIso→NatIso : {F G : Functor C D} → (p : F ≡ G) → pathToNatIso p ≡ FUNCTORIso→NatIso (pathToIso p) Path→FUNCTORIso→NatIso {F = F} p = J (λ _ p → pathToNatIso p ≡ FUNCTORIso→NatIso (pathToIso p)) (NatIso≡ refl-helper) p ->>>>>>> master where refl-helper : _ refl-helper i x = ((λ i → pathToIso-refl {C = D} {x = F .F-ob x} i .fst) ∙ (λ i → pathToIso-refl {C = FUNCTOR} {x = F} (~ i) .fst .N-ob x)) i Iso-FUNCTORIso-NatIso : {F G : Functor C D} → Iso (CatIso FUNCTOR F G) (NatIso F G) -<<<<<<< HEAD - Iso-FUNCTORIso-NatIso .fun = Iso→NatIso - Iso-FUNCTORIso-NatIso .inv = NatIso→Iso -======= Iso-FUNCTORIso-NatIso .fun = FUNCTORIso→NatIso Iso-FUNCTORIso-NatIso .inv = NatIso→FUNCTORIso ->>>>>>> master Iso-FUNCTORIso-NatIso .rightInv α i .trans = α .trans Iso-FUNCTORIso-NatIso .rightInv α i .nIso = isProp→PathP (λ i → isPropΠ (λ _ → isPropIsIso _)) (FUNCTORIso' (α .trans) (FUNCTORIso _ (α .nIso))) (α .nIso) i @@ -118,8 +101,4 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where isUnivalentFUNCTOR : isUnivalent D → isUnivalent FUNCTOR isUnivalentFUNCTOR isUnivD .univ _ _ = isEquiv[equivFunA≃B∘f]→isEquiv[f] _ FUNCTORIso≃NatIso -<<<<<<< HEAD - (subst isEquiv (λ i p → Path→Iso→NatIso p i) (Path≃NatIso isUnivD .snd)) -======= (subst isEquiv (λ i p → Path→FUNCTORIso→NatIso p i) (Path≃NatIso isUnivD .snd)) ->>>>>>> master diff --git a/Cubical/Categories/RezkCompletion/Base.agda b/Cubical/Categories/RezkCompletion/Base.agda index 6aeff9feaf..1927d5188f 100644 --- a/Cubical/Categories/RezkCompletion/Base.agda +++ b/Cubical/Categories/RezkCompletion/Base.agda @@ -15,10 +15,7 @@ open import Cubical.Categories.Functor.ComposeProperty open import Cubical.Categories.Equivalence open import Cubical.Categories.Equivalence.WeakEquivalence open import Cubical.Categories.Instances.Functors -<<<<<<< HEAD -======= open import Cubical.Data.Prod ->>>>>>> master private variable @@ -32,22 +29,6 @@ private -- because the universal property is naturally universal polymorphic, -- and so the predicate is not inside any universe of finite level. -<<<<<<< HEAD --- The product type with one parameter in Typeω -record _×ω_ {a} (A : Type a) (B : Typeω) : Typeω where - constructor _,_ - field - fst : A - snd : B - -open _×ω_ public - -isRezkCompletion : (F : Functor C D) → Typeω -isRezkCompletion {D = D} F = isUnivalent D ×ω ({ℓ ℓ' : Level}{E : Category ℓ ℓ'} → isUnivalent E → isEquivalence (precomposeF E F)) - --- The critrion of being Rezk completion, c.f. HoTT Book Chapter 9.9. -======= - isRezkCompletion : (F : Functor C D) → Typeω isRezkCompletion {D = D} F = isUnivalent D @@ -56,7 +37,6 @@ isRezkCompletion {D = D} F = -- The criterion of being Rezk completion, c.f. HoTT Book Chapter 9.9. open _×ω_ ->>>>>>> master makeIsRezkCompletion : {F : Functor C D} → isUnivalent D → isWeakEquivalence F → isRezkCompletion F makeIsRezkCompletion univ w-equiv .fst = univ diff --git a/Cubical/Foundations/Prelude.agda b/Cubical/Foundations/Prelude.agda index da88442fd0..fc7cc9fa1f 100644 --- a/Cubical/Foundations/Prelude.agda +++ b/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