From 92ccbff9f5aa1039ff642a76688a9f978e0a1705 Mon Sep 17 00:00:00 2001 From: Marcin Grzybowski Date: Mon, 4 Dec 2023 20:36:25 +0100 Subject: [PATCH 01/17] new modules: * Cubical/Categories/Category/Path.agda Helper representation of Path between categories to deal with ineficiency in WeakEquivalence.agda * Cubical/Relation/Binary/Setoid.agda Setoid - Pair of hSet and propositional equivalence relation * Cubical/Categories/Instances/Setoids.agda Univalent Category of Setoids changes: * Cubical/Categories/Adjoint.agda added composiiton of adjunctions * Cubical/Categories/Equivalence/WeakEquivalence.agda Equivalence equivalent to Path for Univalent Categories * Cubical/Categories/Instances/Functors.agda currying of functors is an isomorphism. * Cubical/Foundations/Transport.agda transport-filler-ua = ua-gluePath + some other minor helpers --- Cubical/Categories/Adjoint.agda | 20 +- Cubical/Categories/Category/Base.agda | 4 + Cubical/Categories/Category/Path.agda | 139 ++++++++++ .../Categories/Constructions/BinProduct.agda | 7 + .../Constructions/FullSubcategory.agda | 3 +- Cubical/Categories/Equivalence/Base.agda | 1 + .../Equivalence/WeakEquivalence.agda | 134 +++++++++- Cubical/Categories/Functor/Properties.agda | 68 +++-- Cubical/Categories/Instances/Functors.agda | 27 +- Cubical/Categories/Instances/Setoids.agda | 241 ++++++++++++++++++ Cubical/Foundations/Equiv.agda | 7 +- Cubical/Foundations/Function.agda | 7 +- Cubical/Foundations/HLevels.agda | 23 ++ Cubical/Foundations/Prelude.agda | 8 + Cubical/Foundations/Transport.agda | 53 +++- .../HITs/CumulativeHierarchy/Properties.agda | 2 +- Cubical/HITs/SetQuotients/Properties.agda | 8 +- Cubical/Relation/Binary/Base.agda | 103 +++++++- Cubical/Relation/Binary/Properties.agda | 105 ++++++-- Cubical/Relation/Binary/Setoid.agda | 79 ++++++ 20 files changed, 983 insertions(+), 56 deletions(-) create mode 100644 Cubical/Categories/Category/Path.agda create mode 100644 Cubical/Categories/Instances/Setoids.agda create mode 100644 Cubical/Relation/Binary/Setoid.agda diff --git a/Cubical/Categories/Adjoint.agda b/Cubical/Categories/Adjoint.agda index 5d6c102ac3..fb0e4e4191 100644 --- a/Cubical/Categories/Adjoint.agda +++ b/Cubical/Categories/Adjoint.agda @@ -31,7 +31,7 @@ equivalence. private variable - ℓC ℓC' ℓD ℓD' : Level + ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level {- ============================================== @@ -69,6 +69,7 @@ private variable C : Category ℓC ℓC' D : Category ℓC ℓC' + E : Category ℓE ℓE' module _ {F : Functor C D} {G : Functor D C} where @@ -189,6 +190,9 @@ module NaturalBijection where field adjIso : ∀ {c d} → Iso (D [ F ⟅ c ⟆ , d ]) (C [ c , G ⟅ d ⟆ ]) + adjEquiv : ∀ {c d} → (D [ F ⟅ c ⟆ , d ]) ≃ (C [ c , G ⟅ d ⟆ ]) + adjEquiv = isoToEquiv adjIso + infix 40 _♭ infix 40 _♯ _♭ : ∀ {c d} → (D [ F ⟅ c ⟆ , d ]) → (C [ c , G ⟅ d ⟆ ]) @@ -232,6 +236,20 @@ module NaturalBijection where isRightAdjoint : {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (G : Functor D C) → Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) isRightAdjoint {C = C}{D} G = Σ[ F ∈ Functor C D ] F ⊣ G +module Compose {F : Functor C D} {G : Functor D C} + {L : Functor D E} {R : Functor E D} + where + open NaturalBijection + module _ (F⊣G : F ⊣ G) (L⊣R : L ⊣ R) where + open _⊣_ + + LF⊣GR : (L ∘F F) ⊣ (G ∘F R) + adjIso LF⊣GR = compIso (adjIso L⊣R) (adjIso F⊣G) + adjNatInD LF⊣GR f k = + cong (adjIso F⊣G .fun) (adjNatInD L⊣R _ _) ∙ adjNatInD F⊣G _ _ + adjNatInC LF⊣GR f k = + cong (adjIso L⊣R .inv) (adjNatInC F⊣G _ _) ∙ adjNatInC L⊣R _ _ + {- ============================================== Proofs of equivalence diff --git a/Cubical/Categories/Category/Base.agda b/Cubical/Categories/Category/Base.agda index 37c36ab20f..7656b21a73 100644 --- a/Cubical/Categories/Category/Base.agda +++ b/Cubical/Categories/Category/Base.agda @@ -124,6 +124,10 @@ record isUnivalent (C : Category ℓ ℓ') : Type (ℓ-max ℓ ℓ') where isGroupoid-ob : isGroupoid (C .ob) isGroupoid-ob = isOfHLevelPath'⁻ 2 (λ _ _ → isOfHLevelRespectEquiv 2 (invEquiv (univEquiv _ _)) (isSet-CatIso _ _)) +isPropIsUnivalent : {C : Category ℓ ℓ'} → isProp (isUnivalent C) +isPropIsUnivalent = + isPropRetract isUnivalent.univ _ (λ _ → refl) + (isPropΠ2 λ _ _ → isPropIsEquiv _ ) -- Opposite category _^op : Category ℓ ℓ' → Category ℓ ℓ' diff --git a/Cubical/Categories/Category/Path.agda b/Cubical/Categories/Category/Path.agda new file mode 100644 index 0000000000..b87b0b54dd --- /dev/null +++ b/Cubical/Categories/Category/Path.agda @@ -0,0 +1,139 @@ +{- + +This module represents a path between categories (defined as records) as equivalent +to records of paths between fields. +It omits contractible fields for efficiency. + +This helps greatly with efficiency in Cubical.Categories.Equivalence.WeakEquivalence. + +This construction can be viewed as repeated application of `ΣPath≃PathΣ` and `Σ-contractSnd`. + +-} + +{-# OPTIONS --safe #-} +module Cubical.Categories.Category.Path where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Path + +open import Cubical.Relation.Binary.Base + +open import Cubical.Categories.Category.Base + + + +open Category + +private + variable + ℓ ℓ' : Level + +record CategoryPath (C C' : Category ℓ ℓ') : Type (ℓ-suc (ℓ-max ℓ ℓ')) where + constructor categoryPath + field + ob≡ : C .ob ≡ C' .ob + Hom≡ : PathP (λ i → ob≡ i → ob≡ i → Type ℓ') (C .Hom[_,_]) (C' .Hom[_,_]) + id≡ : PathP (λ i → BinaryRelation.isRefl' (Hom≡ i)) (C .id) (C' .id) + ⋆≡ : PathP (λ i → BinaryRelation.isTrans' (Hom≡ i)) (C ._⋆_) (C' ._⋆_) + + + isSetHom≡ : PathP (λ i → ∀ {x y} → isSet (Hom≡ i x y)) + (C .isSetHom) (C' .isSetHom) + isSetHom≡ = isProp→PathP (λ _ → isPropImplicitΠ2 λ _ _ → isPropIsSet) _ _ + + mk≡ : C ≡ C' + ob (mk≡ i) = ob≡ i + Hom[_,_] (mk≡ i) = Hom≡ i + id (mk≡ i) = id≡ i + _⋆_ (mk≡ i) = ⋆≡ i + ⋆IdL (mk≡ i) = + isProp→PathP + (λ i → isPropImplicitΠ2 λ x y → isPropΠ + λ f → isOfHLevelPath' 1 (isSetHom≡ i {x} {y}) (⋆≡ i (id≡ i) f) f) + (C .⋆IdL) (C' .⋆IdL) i + ⋆IdR (mk≡ i) = + isProp→PathP + (λ i → isPropImplicitΠ2 λ x y → isPropΠ + λ f → isOfHLevelPath' 1 (isSetHom≡ i {x} {y}) (⋆≡ i f (id≡ i)) f) + (C .⋆IdR) (C' .⋆IdR) i + ⋆Assoc (mk≡ i) = + isProp→PathP + (λ i → isPropImplicitΠ4 λ x y z w → isPropΠ3 + λ f f' f'' → isOfHLevelPath' 1 (isSetHom≡ i {x} {w}) + (⋆≡ i (⋆≡ i {x} {y} {z} f f') f'') (⋆≡ i f (⋆≡ i f' f''))) + (C .⋆Assoc) (C' .⋆Assoc) i + isSetHom (mk≡ i) = isSetHom≡ i + + +module _ {C C' : Category ℓ ℓ'} where + + open CategoryPath + + ≡→CategoryPath : C ≡ C' → CategoryPath C C' + ≡→CategoryPath pa = c + where + c : CategoryPath C C' + ob≡ c = cong ob pa + Hom≡ c = cong Hom[_,_] pa + id≡ c = cong id pa + ⋆≡ c = cong _⋆_ pa + + CategoryPathIso : Iso (CategoryPath C C') (C ≡ C') + Iso.fun CategoryPathIso = CategoryPath.mk≡ + Iso.inv CategoryPathIso = ≡→CategoryPath + Iso.rightInv CategoryPathIso b i j = c + where + cp = ≡→CategoryPath b + b' = CategoryPath.mk≡ cp + module _ (j : I) where + module c' = Category (b j) + + c : Category ℓ ℓ' + ob c = c'.ob j + Hom[_,_] c = c'.Hom[_,_] j + id c = c'.id j + _⋆_ c = c'._⋆_ j + ⋆IdL c = isProp→SquareP (λ i j → + isPropImplicitΠ2 λ x y → isPropΠ λ f → + (isSetHom≡ cp j {x} {y}) + (c'._⋆_ j (c'.id j) f) f) + refl refl (λ j → b' j .⋆IdL) (λ j → c'.⋆IdL j) i j + ⋆IdR c = isProp→SquareP (λ i j → + isPropImplicitΠ2 λ x y → isPropΠ λ f → + (isSetHom≡ cp j {x} {y}) + (c'._⋆_ j f (c'.id j)) f) + refl refl (λ j → b' j .⋆IdR) (λ j → c'.⋆IdR j) i j + ⋆Assoc c = isProp→SquareP (λ i j → + isPropImplicitΠ4 λ x y z w → isPropΠ3 λ f g h → + (isSetHom≡ cp j {x} {w}) + (c'._⋆_ j (c'._⋆_ j {x} {y} {z} f g) h) + (c'._⋆_ j f (c'._⋆_ j g h))) + refl refl (λ j → b' j .⋆Assoc) (λ j → c'.⋆Assoc j) i j + isSetHom c = isProp→SquareP (λ i j → + isPropImplicitΠ2 λ x y → isPropIsSet {A = c'.Hom[_,_] j x y}) + refl refl (λ j → b' j .isSetHom) (λ j → c'.isSetHom j) i j + Iso.leftInv CategoryPathIso a = refl + + CategoryPath≡ : {cp cp' : CategoryPath C C'} → + (p≡ : ob≡ cp ≡ ob≡ cp') → + SquareP (λ i j → (p≡ i) j → (p≡ i) j → Type ℓ') + (Hom≡ cp) (Hom≡ cp') (λ _ → C .Hom[_,_]) (λ _ → C' .Hom[_,_]) + → cp ≡ cp' + ob≡ (CategoryPath≡ p≡ _ i) = p≡ i + Hom≡ (CategoryPath≡ p≡ h≡ i) = h≡ i + id≡ (CategoryPath≡ {cp = cp} {cp'} p≡ h≡ i) j {x} = isSet→SquareP + (λ i j → isProp→PathP (λ i → + isPropIsSet {A = BinaryRelation.isRefl' (h≡ i j)}) + (isSetImplicitΠ λ x → isSetHom≡ cp j {x} {x}) + (isSetImplicitΠ λ x → isSetHom≡ cp' j {x} {x}) i) + (id≡ cp) (id≡ cp') (λ _ → C .id) (λ _ → C' .id) + i j {x} + ⋆≡ (CategoryPath≡ {cp = cp} {cp'} p≡ h≡ i) j {x} {y} {z} = isSet→SquareP + (λ i j → isProp→PathP (λ i → + isPropIsSet {A = BinaryRelation.isTrans' (h≡ i j)}) + (isSetImplicitΠ3 (λ x _ z → isSetΠ2 λ _ _ → isSetHom≡ cp j {x} {z})) + (isSetImplicitΠ3 (λ x _ z → isSetΠ2 λ _ _ → isSetHom≡ cp' j {x} {z})) i) + (⋆≡ cp) (⋆≡ cp') (λ _ → C ._⋆_) (λ _ → C' ._⋆_) + i j {x} {y} {z} diff --git a/Cubical/Categories/Constructions/BinProduct.agda b/Cubical/Categories/Constructions/BinProduct.agda index 1dc25f1605..145d7b39d2 100644 --- a/Cubical/Categories/Constructions/BinProduct.agda +++ b/Cubical/Categories/Constructions/BinProduct.agda @@ -45,6 +45,13 @@ F-hom (Snd C D) = snd F-id (Snd C D) = refl F-seq (Snd C D) _ _ = refl +Swap : (C : Category ℓC ℓC') → (D : Category ℓD ℓD') → Σ (Functor (C ×C D) (D ×C C)) isFullyFaithful +F-ob (fst (Swap C D)) = _ +F-hom (fst (Swap C D)) = _ +F-id (fst (Swap C D)) = refl +F-seq (fst (Swap C D)) _ _ = refl +snd (Swap C D) _ _ = snd Σ-swap-≃ + module _ where private variable diff --git a/Cubical/Categories/Constructions/FullSubcategory.agda b/Cubical/Categories/Constructions/FullSubcategory.agda index f05b966ea7..bc1b258741 100644 --- a/Cubical/Categories/Constructions/FullSubcategory.agda +++ b/Cubical/Categories/Constructions/FullSubcategory.agda @@ -19,7 +19,7 @@ private variable ℓC ℓC' ℓD ℓD' ℓE ℓE' ℓP ℓQ ℓR : Level -module _ (C : Category ℓC ℓC') (P : Category.ob C → Type ℓP) where +module FullSubcategory (C : Category ℓC ℓC') (P : Category.ob C → Type ℓP) where private module C = Category C open Category @@ -71,6 +71,7 @@ module _ (C : Category ℓC ℓC') (P : Category.ob C → Type ℓP) where isEquivIncl-Iso : isEquiv Incl-Iso isEquivIncl-Iso = Incl-Iso≃ .snd +open FullSubcategory public module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') (Q : Category.ob D → Type ℓQ) where diff --git a/Cubical/Categories/Equivalence/Base.agda b/Cubical/Categories/Equivalence/Base.agda index 433ae6d2e7..08805b6cfb 100644 --- a/Cubical/Categories/Equivalence/Base.agda +++ b/Cubical/Categories/Equivalence/Base.agda @@ -33,6 +33,7 @@ isEquivalence func = ∥ WeakInverse func ∥₁ record _≃ᶜ_ (C : Category ℓC ℓC') (D : Category ℓD ℓD') : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where + constructor equivᶜ field func : Functor C D isEquiv : isEquivalence func diff --git a/Cubical/Categories/Equivalence/WeakEquivalence.agda b/Cubical/Categories/Equivalence/WeakEquivalence.agda index deed6b4b13..bad20dd855 100644 --- a/Cubical/Categories/Equivalence/WeakEquivalence.agda +++ b/Cubical/Categories/Equivalence/WeakEquivalence.agda @@ -3,17 +3,28 @@ Weak Equivalence between Categories -} -{-# OPTIONS --safe #-} +{-# OPTIONS --safe --lossy-unification #-} module Cubical.Categories.Equivalence.WeakEquivalence where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Structure +open import Cubical.Foundations.Transport hiding (pathToIso) open import Cubical.Foundations.Equiv - renaming (isEquiv to isEquivMap) + renaming (isEquiv to isEquivMap ; equivFun to _≃$_) +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv.Properties +open import Cubical.Foundations.Function renaming (_∘_ to _∘f_) open import Cubical.Functions.Surjection open import Cubical.Categories.Category +open import Cubical.Categories.Category.Path open import Cubical.Categories.Functor open import Cubical.Categories.Equivalence +open import Cubical.Relation.Binary +open import Cubical.Data.Sigma +open import Cubical.HITs.PropositionalTruncation private variable @@ -37,6 +48,7 @@ record isWeakEquivalence {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} record WeakEquivalence (C : Category ℓC ℓC') (D : Category ℓD ℓD') : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where + constructor weakEquivalence field func : Functor C D @@ -45,6 +57,24 @@ record WeakEquivalence (C : Category ℓC ℓC') (D : Category ℓD ℓD') open isWeakEquivalence open WeakEquivalence +isPropIsWeakEquivalence : isProp (isWeakEquivalence F) +isPropIsWeakEquivalence = + isPropRetract (λ x → fullfaith x , esssurj x) _ (λ _ → refl) + (isProp× (isPropΠ2 λ _ _ → isPropIsEquiv _) + (isPropΠ λ _ → squash₁)) + + +isWeakEquivalenceTransportFunctor : (p : C ≡ D) → isWeakEquivalence (TransportFunctor p) +fullfaith (isWeakEquivalenceTransportFunctor {C = C} p) x y = isEquivTransport + λ i → cong Category.Hom[_,_] p i + (transport-filler (cong Category.ob p) x i) + (transport-filler (cong Category.ob p) y i) +esssurj (isWeakEquivalenceTransportFunctor {C = C} p) d = + ∣ (subst⁻ Category.ob p d) , pathToIso (substSubst⁻ Category.ob p _) ∣₁ + +≡→WeakEquivlance : C ≡ D → WeakEquivalence C D +func (≡→WeakEquivlance _) = _ +isWeakEquiv (≡→WeakEquivlance b) = isWeakEquivalenceTransportFunctor b -- Equivalence is always weak equivalence. @@ -71,3 +101,103 @@ module _ 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) + + Equivalence≃WeakEquivalence : C ≃ᶜ D ≃ WeakEquivalence C D + Equivalence≃WeakEquivalence = + isoToEquiv (iso _ (uncurry equivᶜ) (λ _ → refl) λ _ → refl) + ∙ₑ Σ-cong-equiv-snd + (λ _ → propBiimpl→Equiv squash₁ isPropIsWeakEquivalence + isEquiv→isWeakEquiv isWeakEquiv→isEquiv) + ∙ₑ isoToEquiv (iso (uncurry weakEquivalence) _ (λ _ → refl) λ _ → refl) + +module _ + {C C' : Category ℓC ℓC'} + (isUnivC : isUnivalent C) + (isUnivC' : isUnivalent C') + where + + open CategoryPath + + module 𝑪 = Category C + module 𝑪' = Category C' + + module _ {F} (we : isWeakEquivalence {C = C} {C'} F) where + + open Category + + ob≃ : 𝑪.ob ≃ 𝑪'.ob + ob≃ = _ , isEquivF-ob isUnivC isUnivC' we + + Hom≃ : ∀ x y → 𝑪.Hom[ x , y ] ≃ 𝑪'.Hom[ ob≃ ≃$ x , ob≃ ≃$ y ] + Hom≃ _ _ = F-hom F , fullfaith we _ _ + + HomPathP : PathP (λ i → ua ob≃ i → ua ob≃ i → Type ℓC') + 𝑪.Hom[_,_] 𝑪'.Hom[_,_] + HomPathP = RelPathP _ Hom≃ + + WeakEquivlance→CategoryPath : CategoryPath C C' + ob≡ WeakEquivlance→CategoryPath = ua ob≃ + Hom≡ WeakEquivlance→CategoryPath = HomPathP + id≡ WeakEquivlance→CategoryPath = EquivJRel {_∻_ = 𝑪'.Hom[_,_]} + (λ Ob e H[_,_] h[_,_] → + (id* : ∀ {x : Ob} → H[ x , x ]) → + ({x : Ob} → (h[ x , _ ] ≃$ id*) ≡ C' .id {e ≃$ x} ) + → PathP (λ i → {x : ua e i} → RelPathP e {_} {𝑪'.Hom[_,_]} h[_,_] i x x) id* λ {x} → C' .id {x}) + (λ _ x i → glue (λ {(i = i0) → _ ; (i = i1) → _ }) (x i)) _ _ Hom≃ (C .id) (F-id F) + + ⋆≡ WeakEquivlance→CategoryPath = EquivJRel {_∻_ = 𝑪'.Hom[_,_]} + (λ Ob e H[_,_] h[_,_] → (⋆* : BinaryRelation.isTrans' H[_,_]) → + (∀ {x y z : Ob} f g → (h[ x , z ] ≃$ (⋆* f g)) ≡ + C' ._⋆_ (h[ x , _ ] ≃$ f) (h[ y , _ ] ≃$ g) ) + → PathP (λ i → BinaryRelation.isTrans' (RelPathP e h[_,_] i)) + (⋆*) (λ {x y z} → C' ._⋆_ {x} {y} {z})) + (λ _ x i f g → glue + (λ {(i = i0) → _ ; (i = i1) → _ }) (x (unglue (i ∨ ~ i) f) (unglue (i ∨ ~ i) g) i )) + _ _ Hom≃ (C ._⋆_) (F-seq F) + + open Iso + + IsoCategoryPath : Iso (WeakEquivalence C C') (CategoryPath C C') + fun IsoCategoryPath = WeakEquivlance→CategoryPath ∘f isWeakEquiv + inv IsoCategoryPath = ≡→WeakEquivlance ∘f mk≡ + rightInv IsoCategoryPath b = CategoryPath≡ + (λ i j → + Glue _ {φ = ~ j ∨ j ∨ i} + (λ _ → _ , equivPathP + {e = ob≃ (isWeakEquivalenceTransportFunctor (mk≡ b))} {f = idEquiv _} + (transport-fillerExt⁻ (ob≡ b)) j)) + λ i j x y → + Glue (𝑪'.Hom[ unglue _ x , unglue _ y ]) + λ { (j = i0) → _ , Hom≃ (isWeakEquivalenceTransportFunctor (mk≡ b)) _ _ + ;(j = i1) → _ , idEquiv _ + ;(i = i1) → _ , _ + , isProp→PathP (λ j → isPropΠ2 λ x y → + isPropIsEquiv (transp (λ i₂ → + let tr = transp (λ j' → ob≡ b (j ∨ (i₂ ∧ j'))) (~ i₂ ∨ j) + in Hom≡ b (i₂ ∨ j) (tr x) (tr y)) j)) + (λ _ _ → snd (Hom≃ (isWeakEquivalenceTransportFunctor (mk≡ b)) _ _)) + (λ _ _ → snd (idEquiv _)) j x y } + + leftInv IsoCategoryPath we = cong₂ weakEquivalence + (Functor≡ (transportRefl ∘f (F-ob (func we))) + λ {c} {c'} f → (λ j → transport + (λ i → HomPathP (isWeakEquiv we) i + (transport-filler-ua (ob≃ (isWeakEquiv we)) c j i) + (transport-filler-ua (ob≃ (isWeakEquiv we)) c' j i)) + f) ▷ transportRefl _ ) + (isProp→PathP (λ _ → isPropIsWeakEquivalence) _ _ ) + + WeakEquivalence≃Path : WeakEquivalence C C' ≃ (C ≡ C') + WeakEquivalence≃Path = + isoToEquiv (compIso IsoCategoryPath CategoryPathIso) + + Equivalence≃Path : C ≃ᶜ C' ≃ (C ≡ C') + Equivalence≃Path = Equivalence≃WeakEquivalence isUnivC isUnivC' ∙ₑ WeakEquivalence≃Path + +is2GroupoidUnivalentCategory : is2Groupoid (Σ (Category ℓC ℓC') isUnivalent) +is2GroupoidUnivalentCategory (C , isUnivalentC) (C' , isUnivalentC') = + isOfHLevelRespectEquiv 3 + (isoToEquiv (iso (uncurry weakEquivalence) _ (λ _ → refl) λ _ → refl) + ∙ₑ WeakEquivalence≃Path isUnivalentC isUnivalentC' ∙ₑ Σ≡PropEquiv λ _ → isPropIsUnivalent) + λ _ _ → isOfHLevelRespectEquiv 2 (Σ≡PropEquiv λ _ → isPropIsWeakEquivalence) + (isOfHLevelFunctor 1 (isUnivalent.isGroupoid-ob isUnivalentC') _ _) diff --git a/Cubical/Categories/Functor/Properties.agda b/Cubical/Categories/Functor/Properties.agda index a6d378dea1..d899ba410a 100644 --- a/Cubical/Categories/Functor/Properties.agda +++ b/Cubical/Categories/Functor/Properties.agda @@ -7,11 +7,14 @@ open import Cubical.Foundations.Equiv open import Cubical.Foundations.Equiv.Properties open import Cubical.Foundations.Function hiding (_∘_) open import Cubical.Foundations.GroupoidLaws using (lUnit; rUnit; assoc; cong-∙) +open import Cubical.Foundations.Path open import Cubical.Foundations.HLevels +import Cubical.Foundations.Isomorphism as Iso 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.Data.Nat open import Cubical.Categories.Category open import Cubical.Categories.Isomorphism open import Cubical.Categories.Morphism @@ -103,26 +106,34 @@ module _ {F : Functor C D} where → PathP (λ i → D [ F .F-ob (p i) , F. F-ob (q i) ]) (F .F-hom f) (F .F-hom g) functorCongP r i = F .F-hom (r i) -isSetFunctor : isSet (D .ob) → isSet (Functor C D) -isSetFunctor {D = D} {C = C} isSet-D-ob F G p q = w - where - w : _ - F-ob (w i i₁) = isSetΠ (λ _ → isSet-D-ob) _ _ (cong F-ob p) (cong F-ob q) i i₁ - F-hom (w i i₁) z = - isSet→SquareP - (λ i i₁ → D .isSetHom {(F-ob (w i i₁) _)} {(F-ob (w i i₁) _)}) - (λ i₁ → F-hom (p i₁) z) (λ i₁ → F-hom (q i₁) z) refl refl i i₁ - - F-id (w i i₁) = - isSet→SquareP - (λ i i₁ → isProp→isSet (D .isSetHom (F-hom (w i i₁) _) (D .id))) - (λ i₁ → F-id (p i₁)) (λ i₁ → F-id (q i₁)) refl refl i i₁ - F-seq (w i i₁) _ _ = - isSet→SquareP - (λ 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₁ +isEquivFunctor≡ : ∀ {F} {G} → isEquiv (uncurry (Functor≡ {C = C} {D = D} {F = F} {G = G})) +isEquivFunctor≡ {C = C} {D = D} = Iso.isoToIsEquiv ww + where + + ww : Iso.Iso _ _ + Iso.Iso.fun ww = _ + Iso.Iso.inv ww x = (λ c i → F-ob (x i) c) , λ {c} {c'} f i → F-hom (x i) {c} {c'} f + F-ob (Iso.Iso.rightInv ww b i i₁) = F-ob (b i₁) + F-hom (Iso.Iso.rightInv ww b i i₁) = F-hom (b i₁) + F-id (Iso.Iso.rightInv ww b i i₁) = isProp→SquareP + (λ i i₁ → D .isSetHom (F-hom (b i₁) (C .id)) (D .id)) refl refl + (isProp→PathP (λ j → isSetHom D _ _) _ _) (λ i₁ → F-id (b i₁)) i i₁ + F-seq (Iso.Iso.rightInv ww b i i₁) f g = isProp→SquareP + (λ i i₁ → D .isSetHom (F-hom (b i₁) _) (seq' D (F-hom (b i₁) f) _)) + refl refl (isProp→PathP (λ j → isSetHom D _ _) _ _) (λ i₁ → F-seq (b i₁) f g) i i₁ + Iso.Iso.leftInv ww _ = refl + +isOfHLevelFunctor : ∀ hLevel → isOfHLevel (2 + hLevel) (D .ob) + → isOfHLevel (2 + hLevel) (Functor C D) +isOfHLevelFunctor {D = D} {C = C} hLevel x _ _ = + isOfHLevelRespectEquiv (1 + hLevel) (_ , isEquivFunctor≡) + (isOfHLevelΣ (1 + hLevel) (isOfHLevelΠ (1 + hLevel) (λ _ → x _ _)) + λ _ → isOfHLevelPlus' 1 (isPropImplicitΠ2 + λ _ _ → isPropΠ λ _ → isOfHLevelPathP' 1 (λ _ _ → D .isSetHom _ _) _ _ )) +isSetFunctor : isSet (D .ob) → isSet (Functor C D) +isSetFunctor = isOfHLevelFunctor 0 -- Conservative Functor, -- namely if a morphism f is mapped to an isomorphism, @@ -232,3 +243,24 @@ module _ (subst isEquiv (F-pathToIso-∘ {F = F}) (compEquiv (_ , isUnivC .univ _ _) (_ , isFullyFaithful→isEquivF-Iso {F = F} fullfaith x y) .snd)) + +TransportFunctor : (C ≡ D) → Functor C D +F-ob (TransportFunctor p) = subst ob p +F-hom (TransportFunctor p) {x} {y} = + transport λ i → cong Hom[_,_] p i + (transport-filler (cong ob p) x i) + (transport-filler (cong ob p) y i) +F-id (TransportFunctor p) {x} i = + transp (λ jj → Hom[ p (i ∨ jj) , transport-filler (λ i₁ → ob (p i₁)) x (i ∨ jj) ] + (transport-filler (λ i₁ → ob (p i₁)) x (i ∨ jj))) i + (id (p i) {(transport-filler (cong ob p) x i)}) + +F-seq (TransportFunctor p) {x} {y} {z} f g i = + let q : ∀ {x y} → _ ≡ _ + q = λ {x y} → λ i₁ → + Hom[ p i₁ , transport-filler (λ i₂ → ob (p i₂)) x i₁ ] + (transport-filler (λ i₂ → ob (p i₂)) y i₁) + in transp (λ jj → Hom[ p (i ∨ jj) + , transport-filler (λ i₁ → ob (p i₁)) x (i ∨ jj) ] + (transport-filler (λ i₁ → ob (p i₁)) z (i ∨ jj))) i + (_⋆_ (p i) (transport-filler q f i) (transport-filler q g i)) diff --git a/Cubical/Categories/Instances/Functors.agda b/Cubical/Categories/Instances/Functors.agda index eb3498dfe0..0a220f92a0 100644 --- a/Cubical/Categories/Instances/Functors.agda +++ b/Cubical/Categories/Instances/Functors.agda @@ -6,9 +6,8 @@ Includes the following - isos in FUNCTOR are precisely the pointwise isos - FUNCTOR C D is univalent when D is - - currying of functors + - Isomorphism of functors currying - TODO: show that currying of functors is an isomorphism. -} module Cubical.Categories.Instances.Functors where @@ -18,6 +17,7 @@ open import Cubical.Foundations.Equiv open import Cubical.Foundations.Equiv.Properties open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function renaming (_∘_ to _∘→_) open import Cubical.Categories.Category renaming (isIso to isIsoC) open import Cubical.Categories.Constructions.BinProduct @@ -169,3 +169,26 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where F ⟪ g ∘⟨ E ⟩ f , C .id ∘⟨ C ⟩ C .id ⟫ ≡⟨ F .F-seq (f , C .id) (g , C .id) ⟩ (F ⟪ g , C .id ⟫) ∘⟨ D ⟩ (F ⟪ f , C .id ⟫) ∎ + + λF⁻ : Functor E FUNCTOR → Functor (E ×C C) D + F-ob (λF⁻ a) = uncurry (F-ob ∘→ F-ob a) + F-hom (λF⁻ a) _ = N-ob (F-hom a _) _ ∘⟨ D ⟩ (F-hom (F-ob a _)) _ + F-id (λF⁻ a) = cong₂ (seq' D) (F-id (F-ob a _)) + (cong (flip N-ob _) (F-id a)) ∙ D .⋆IdL _ + F-seq (λF⁻ a) _ (eG , cG) = + cong₂ (seq' D) (F-seq (F-ob a _) _ _) (cong (flip N-ob _) + (F-seq a _ _)) + ∙ AssocCong₂⋆R {C = D} _ + (N-hom ((F-hom a _) ●ᵛ (F-hom a _)) _ ∙ + (⋆Assoc D _ _ _) ∙ + cong (seq' D _) (sym (N-hom (F-hom a eG) cG))) + + isoλF : Iso (Functor (E ×C C) D) (Functor E FUNCTOR) + fun isoλF = λF + inv isoλF = λF⁻ + rightInv isoλF b = Functor≡ (λ _ → Functor≡ (λ _ → refl) + λ _ → cong (seq' D _) (congS (flip N-ob _) (F-id b)) ∙ D .⋆IdR _) + λ _ → toPathP (makeNatTransPath (transportRefl _ ∙ + funExt λ _ → cong (flip (seq' D) _) (F-id (F-ob b _)) ∙ D .⋆IdL _)) + leftInv isoλF a = Functor≡ (λ _ → refl) λ _ → sym (F-seq a _ _) + ∙ cong (F-hom a) (cong₂ _,_ (E .⋆IdL _) (C .⋆IdR _)) diff --git a/Cubical/Categories/Instances/Setoids.agda b/Cubical/Categories/Instances/Setoids.agda new file mode 100644 index 0000000000..265608b3c8 --- /dev/null +++ b/Cubical/Categories/Instances/Setoids.agda @@ -0,0 +1,241 @@ +{-# OPTIONS --safe #-} + +module Cubical.Categories.Instances.Setoids where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Equiv.Properties +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Transport hiding (pathToIso) +open import Cubical.Foundations.Function +open import Cubical.Functions.FunExtEquiv +open import Cubical.Functions.Logic hiding (_⇒_) +open import Cubical.Data.Unit +open import Cubical.Data.Sigma +open import Cubical.Categories.Category +open import Cubical.Categories.Morphism +open import Cubical.Categories.Functor +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Equivalence.WeakEquivalence +open import Cubical.Categories.Adjoint +open import Cubical.Categories.Functors.HomFunctor +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.Constructions.BinProduct +open import Cubical.Categories.Constructions.FullSubcategory +open import Cubical.Categories.Instances.Functors +open import Cubical.Relation.Binary +open import Cubical.Relation.Binary.Setoid + +open import Cubical.HITs.SetQuotients as / +open import Cubical.HITs.PropositionalTruncation + +open Category hiding (_∘_) +open Functor + + +module _ ℓ where + SETOID : Category (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ)) (ℓ-max ℓ ℓ) + ob SETOID = Setoid ℓ ℓ + Hom[_,_] SETOID = SetoidMor + fst (id SETOID) _ = _ + snd (id SETOID) r = r + fst ((SETOID ⋆ _) _) = _ + snd ((SETOID ⋆ (_ , f)) (_ , g)) = g ∘ f + ⋆IdL SETOID _ = refl + ⋆IdR SETOID _ = refl + ⋆Assoc SETOID _ _ _ = refl + isSetHom SETOID {y = (_ , isSetB) , ((_ , isPropR) , _)} = + isSetΣ (isSet→ isSetB) (isProp→isSet ∘ isPropRespects isPropR ) + + open Iso + + IsoPathCatIsoSETOID : ∀ {x y} → Iso (x ≡ y) (CatIso SETOID x y) + fun (IsoPathCatIsoSETOID) = pathToIso + inv (IsoPathCatIsoSETOID {y = _ , ((y , _) , _) }) ((_ , r) , ci) = + cong₂ _,_ + (TypeOfHLevel≡ 2 (isoToPath i)) + (toPathP (EquivPropRel≡ + ( substRel y ((cong fst c.sec ≡$ _) ∙_ ∘ transportRefl) ∘ r + , snd c.inv ∘ substRel y (sym ∘ transportRefl)) + )) + where + module c = isIso ci + i : Iso _ _ + fun i = _ ; inv i = fst c.inv + rightInv i = cong fst c.sec ≡$_ ; leftInv i = cong fst c.ret ≡$_ + + rightInv (IsoPathCatIsoSETOID {x = x} {y = y}) ((f , _) , _) = + CatIso≡ _ _ (SetoidMor≡ x y + (funExt λ _ → transportRefl _ ∙ cong f (transportRefl _))) + leftInv (IsoPathCatIsoSETOID) a = + ΣSquareSet (λ _ → isSetEquivPropRel) + (TypeOfHLevelPath≡ 2 (λ _ → + transportRefl _ ∙ cong (subst (fst ∘ fst) a) (transportRefl _))) + + isUnivalentSETOID : isUnivalent SETOID + isUnivalent.univ isUnivalentSETOID _ _ = + isoToIsEquiv IsoPathCatIsoSETOID + + + Quot Forget : Functor SETOID (SET ℓ) + IdRel FullRel : Functor (SET ℓ) SETOID + + + F-ob Quot (_ , ((R , _) , _)) = (_ / R) , squash/ + F-hom Quot (f , r) = /.rec squash/ ([_] ∘ f) λ _ _ → eq/ _ _ ∘ r + F-id Quot = funExt (/.elim (λ _ → isProp→isSet (squash/ _ _)) + (λ _ → refl) λ _ _ _ _ → refl) + F-seq Quot _ _ = funExt (/.elim (λ _ → isProp→isSet (squash/ _ _)) + (λ _ → refl) λ _ _ _ _ → refl) + + F-ob IdRel A = A , (_ , snd A) , isEquivRelIdRel + F-hom IdRel = _, cong _ + F-id IdRel = refl + F-seq IdRel _ _ = refl + + F-ob Forget = fst + F-hom Forget = fst + F-id Forget = refl + F-seq Forget _ _ = refl + + F-ob FullRel = _, fullEquivPropRel + F-hom FullRel = _, _ + F-id FullRel = refl + F-seq FullRel _ _ = refl + + isFullyFaithfulIdRel : isFullyFaithful IdRel + isFullyFaithfulIdRel x y = isoToIsEquiv + (iso _ fst + (λ _ → SetoidMor≡ (IdRel ⟅ x ⟆) (IdRel ⟅ y ⟆) refl) + λ _ → refl) + + isFullyFaithfulFullRel : isFullyFaithful FullRel + isFullyFaithfulFullRel x y = isoToIsEquiv + (iso _ fst (λ _ → refl) λ _ → refl) + + IdRel⇒FullRel : IdRel ⇒ FullRel + NatTrans.N-ob IdRel⇒FullRel x = idfun _ , _ + NatTrans.N-hom IdRel⇒FullRel f = refl + + + open Cubical.Categories.Adjoint.NaturalBijection + open _⊣_ + + Quot⊣IdRel : Quot ⊣ IdRel + adjIso Quot⊣IdRel {d = (_ , isSetD)} = setQuotUniversalIso isSetD + adjNatInD Quot⊣IdRel {c = c} {d' = d'} f k = SetoidMor≡ c (IdRel ⟅ d' ⟆) refl + adjNatInC Quot⊣IdRel {d = d} g h = + funExt (/.elimProp (λ _ → snd d _ _) λ _ → refl) + + IdRel⊣Forget : IdRel ⊣ Forget + fun (adjIso IdRel⊣Forget) = fst + inv (adjIso IdRel⊣Forget {d = d}) f = + f , J (λ x' p → fst (fst (snd d)) (f _) (f x')) + (BinaryRelation.isEquivRel.reflexive (snd (snd d)) (f _)) + rightInv (adjIso IdRel⊣Forget) _ = refl + leftInv (adjIso IdRel⊣Forget {c = c} {d = d}) _ = + SetoidMor≡ (IdRel ⟅ c ⟆) d refl + adjNatInD IdRel⊣Forget _ _ = refl + adjNatInC IdRel⊣Forget _ _ = refl + + Forget⊣FullRel : Forget ⊣ FullRel + fun (adjIso Forget⊣FullRel) = _ + inv (adjIso Forget⊣FullRel) = fst + rightInv (adjIso Forget⊣FullRel) _ = refl + leftInv (adjIso Forget⊣FullRel) _ = refl + adjNatInD Forget⊣FullRel _ _ = refl + adjNatInC Forget⊣FullRel _ _ = refl + + + pieces : Functor SETOID SETOID + pieces = IdRel ∘F Quot + + points : Functor SETOID SETOID + points = IdRel ∘F Forget + + pieces⊣points : pieces ⊣ points + pieces⊣points = Compose.LF⊣GR Quot⊣IdRel IdRel⊣Forget + + points→pieces : points ⇒ pieces + points→pieces = + ε (adj'→adj _ _ IdRel⊣Forget) + ●ᵛ η (adj'→adj _ _ Quot⊣IdRel) + where open UnitCounit._⊣_ + + piecesHavePoints : ∀ A → + isEpic SETOID {points ⟅ A ⟆ } {pieces ⟅ A ⟆} + (points→pieces ⟦ A ⟧) + piecesHavePoints A {z = z@((_ , isSetZ) , _) } = + SetoidMor≡ (pieces ⟅ A ⟆) z ∘ + (funExt ∘ /.elimProp (λ _ → isSetZ _ _) ∘ funExt⁻ ∘ cong fst) + + pieces→≃→points : (A B : Setoid ℓ ℓ) → + SetoidMor (pieces ⟅ A ⟆) B + ≃ SetoidMor A (points ⟅ B ⟆) + pieces→≃→points A B = + NaturalBijection._⊣_.adjEquiv + (pieces⊣points) + {c = A} {d = B} + + -⊗- : Functor (SETOID ×C SETOID) SETOID + F-ob -⊗- = uncurry _⊗_ + fst (F-hom -⊗- _) = _ + snd (F-hom -⊗- (f , g)) (x , y) = snd f x , snd g y + F-id -⊗- = refl + F-seq -⊗- _ _ = refl + + InternalHomFunctor : Functor (SETOID ^op ×C SETOID) SETOID + F-ob InternalHomFunctor = uncurry _⟶_ + fst (F-hom InternalHomFunctor (f , g )) (_ , y) = _ , snd g ∘ y ∘ (snd f) + snd (F-hom InternalHomFunctor (f , g)) q = snd g ∘ q ∘ fst f + F-id InternalHomFunctor = refl + F-seq InternalHomFunctor _ _ = refl + + -^_ : ∀ X → Functor SETOID SETOID + -^_ X = (λF SETOID _ (SETOID ^op) InternalHomFunctor ⟅ X ⟆) + + -⊗_ : ∀ X → Functor SETOID SETOID + -⊗_ X = (λF SETOID _ (SETOID) (-⊗- ∘F fst (Swap SETOID SETOID)) ⟅ X ⟆) + + ⊗⊣^ : ∀ X → (-⊗ X) ⊣ (-^ X) + adjIso (⊗⊣^ X) {A} {B} = setoidCurryIso X A B + adjNatInD (⊗⊣^ X) {A} {d' = C} _ _ = SetoidMor≡ A (X ⟶ C) refl + adjNatInC (⊗⊣^ X) {A} {d = C} _ _ = SetoidMor≡ (A ⊗ X) C refl + + + open WeakEquivalence + open isWeakEquivalence + + module FullRelationsSubcategory = FullSubcategory SETOID + (BinaryRelation.isFull ∘ EquivPropRel→Rel ∘ snd) + + FullRelationsSubcategory : Category _ _ + FullRelationsSubcategory = FullRelationsSubcategory.FullSubcategory + + FullRelationsSubcategory≅SET : WeakEquivalence FullRelationsSubcategory (SET ℓ) + func FullRelationsSubcategory≅SET = Forget ∘F FullRelationsSubcategory.FullInclusion + fullfaith (isWeakEquiv FullRelationsSubcategory≅SET) x y@(_ , is-full-rel) = + isoToIsEquiv (iso _ (_, λ _ → is-full-rel _ _) (λ _ → refl) + λ _ → SetoidMor≡ (fst x) (fst y) refl) + esssurj (isWeakEquiv FullRelationsSubcategory≅SET) d = + ∣ (FullRel ⟅ d ⟆ , _) , idCatIso ∣₁ + + module IdRelationsSubcategory = FullSubcategory SETOID + (BinaryRelation.impliesIdentity ∘ EquivPropRel→Rel ∘ snd) + + IdRelationsSubcategory : Category _ _ + IdRelationsSubcategory = IdRelationsSubcategory.FullSubcategory + + IdRelationsSubcategory≅SET : WeakEquivalence IdRelationsSubcategory (SET ℓ) + func IdRelationsSubcategory≅SET = Forget ∘F IdRelationsSubcategory.FullInclusion + fullfaith (isWeakEquiv IdRelationsSubcategory≅SET) + x@(_ , implies-id) y@((_ , ((rel , _) , is-equiv-rel)) , _) = + isoToIsEquiv (iso _ (λ f → f , λ z → + isRefl→impliedByIdentity rel reflexive (cong f (implies-id z))) (λ _ → refl) + λ _ → SetoidMor≡ (fst x) (fst y) refl) + where open BinaryRelation ; open isEquivRel is-equiv-rel + + esssurj (isWeakEquiv IdRelationsSubcategory≅SET) d = + ∣ (IdRel ⟅ d ⟆ , idfun _) , idCatIso ∣₁ diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda index 0529733212..bd95c010e3 100644 --- a/Cubical/Foundations/Equiv.agda +++ b/Cubical/Foundations/Equiv.agda @@ -63,8 +63,13 @@ equiv-proof (isPropIsEquiv f p q i) y = ; (j = i1) → w }) (p2 w (i ∨ j)) +equivPathP : {A : I → Type ℓ} {B : I → Type ℓ'} {e : A i0 ≃ B i0} {f : A i1 ≃ B i1} + → (h : PathP (λ i → A i → B i) (e .fst) (f .fst)) → PathP (λ i → A i ≃ B i) e f +equivPathP {e = e} {f = f} h = + λ i → (h i) , isProp→PathP (λ i → isPropIsEquiv (h i)) (e .snd) (f .snd) i + equivEq : {e f : A ≃ B} → (h : e .fst ≡ f .fst) → e ≡ f -equivEq {e = e} {f = f} h = λ i → (h i) , isProp→PathP (λ i → isPropIsEquiv (h i)) (e .snd) (f .snd) i +equivEq = equivPathP module _ {f : A → B} (equivF : isEquiv f) where funIsEq : A → B diff --git a/Cubical/Foundations/Function.agda b/Cubical/Foundations/Function.agda index 2df2ee16b3..e8b874fb62 100644 --- a/Cubical/Foundations/Function.agda +++ b/Cubical/Foundations/Function.agda @@ -9,7 +9,7 @@ open import Cubical.Foundations.Prelude private variable ℓ ℓ' ℓ'' : Level - A : Type ℓ + A A' A'' : Type ℓ B : A → Type ℓ C : (a : A) → B a → Type ℓ D : (a : A) (b : B a) → C a b → Type ℓ @@ -32,6 +32,11 @@ _∘_ : (g : {a : A} → (b : B a) → C a b) → (f : (a : A) → B a) → (a : g ∘ f = λ x → g (f x) {-# INLINE _∘_ #-} +_∘S_ : (A' → A'') → (A → A') → A → A'' +g ∘S f = λ x → g (f x) +{-# INLINE _∘S_ #-} + + ∘-assoc : (h : {a : A} {b : B a} → (c : C a b) → D a b c) (g : {a : A} → (b : B a) → C a b) (f : (a : A) → B a) diff --git a/Cubical/Foundations/HLevels.agda b/Cubical/Foundations/HLevels.agda index 0432511505..d2f0e11d65 100644 --- a/Cubical/Foundations/HLevels.agda +++ b/Cubical/Foundations/HLevels.agda @@ -448,6 +448,14 @@ isPropImplicitΠ h f g i {x} = h x (f {x}) (g {x}) i isPropImplicitΠ2 : (h : (x : A) (y : B x) → isProp (C x y)) → isProp ({x : A} {y : B x} → C x y) isPropImplicitΠ2 h = isPropImplicitΠ (λ x → isPropImplicitΠ (λ y → h x y)) +isPropImplicitΠ3 : (h : (x : A) (y : B x) (z : C x y) → isProp (D x y z)) → + isProp ({x : A} {y : B x} {z : C x y} → D x y z) +isPropImplicitΠ3 h = isPropImplicitΠ (λ x → isPropImplicitΠ2 (λ y → h x y)) + +isPropImplicitΠ4 : (h : (x : A) (y : B x) (z : C x y) (w : D x y z) → isProp (E x y z w)) → + isProp ({x : A} {y : B x} {z : C x y} {w : D x y z} → E x y z w) +isPropImplicitΠ4 h = isPropImplicitΠ (λ x → isPropImplicitΠ3 (λ y → h x y)) + isProp→ : {A : Type ℓ} {B : Type ℓ'} → isProp B → isProp (A → B) isProp→ pB = isPropΠ λ _ → pB @@ -457,6 +465,13 @@ isSetΠ = isOfHLevelΠ 2 isSetImplicitΠ : (h : (x : A) → isSet (B x)) → isSet ({x : A} → B x) isSetImplicitΠ h f g F G i j {x} = h x (f {x}) (g {x}) (λ i → F i {x}) (λ i → G i {x}) i j +isSetImplicitΠ2 : (h : (x : A) → (y : B x) → isSet (C x y)) → isSet ({x : A} → {y : B x} → C x y) +isSetImplicitΠ2 h = isSetImplicitΠ (λ x → isSetImplicitΠ (λ y → h x y)) + +isSetImplicitΠ3 : (h : (x : A) → (y : B x) → (z : C x y) → isSet (D x y z)) → + isSet ({x : A} → {y : B x} → {z : C x y} → D x y z) +isSetImplicitΠ3 h = isSetImplicitΠ (λ x → isSetImplicitΠ2 (λ y → λ z → h x y z)) + isSet→ : isSet A' → isSet (A → A') isSet→ isSet-A' = isOfHLevelΠ 2 (λ _ → isSet-A') @@ -709,6 +724,14 @@ snd (ΣSquareSet {B = B} pB {p = p} {q = q} {r = r} {s = s} sq i j) = lem i j (cong snd p) (cong snd r) (cong snd s) (cong snd q) lem = toPathP (isOfHLevelPathP' 1 (pB _) _ _ _ _) + +TypeOfHLevelPath≡ : (n : HLevel) {X Y : TypeOfHLevel ℓ n} → + {p q : X ≡ Y} → (∀ x → subst fst p x ≡ subst fst q x) → p ≡ q +TypeOfHLevelPath≡ _ p = + ΣSquareSet (isProp→isSet ∘ λ _ → isPropIsOfHLevel _ ) + (isInjectiveTransport (funExt p)) + + module _ (isSet-A : isSet A) (isSet-A' : isSet A') where diff --git a/Cubical/Foundations/Prelude.agda b/Cubical/Foundations/Prelude.agda index d5796056f3..8a8a9b7fc7 100644 --- a/Cubical/Foundations/Prelude.agda +++ b/Cubical/Foundations/Prelude.agda @@ -87,6 +87,14 @@ cong₂ : {C : (a : A) → (b : B a) → Type ℓ} → cong₂ f p q i = f (p i) (q i) {-# INLINE cong₂ #-} +congS₂ : ∀ {B : Type ℓ} {C : Type ℓ'} → + (f : A → B → C) → + (p : x ≡ y) → + {u v : B} (q : u ≡ v) → + (f x u) ≡ (f y v) +congS₂ f p q i = f (p i) (q i) +{-# INLINE congS₂ #-} + congP₂ : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ'} {C : (i : I) (a : A i) → B i a → Type ℓ''} (f : (i : I) → (a : A i) → (b : B i a) → C i a b) diff --git a/Cubical/Foundations/Transport.agda b/Cubical/Foundations/Transport.agda index 88ec373930..06f2e9f3eb 100644 --- a/Cubical/Foundations/Transport.agda +++ b/Cubical/Foundations/Transport.agda @@ -12,7 +12,7 @@ open import Cubical.Foundations.Equiv as Equiv hiding (transpEquiv) open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Univalence open import Cubical.Foundations.GroupoidLaws -open import Cubical.Foundations.Function using (_∘_) +open import Cubical.Foundations.Function using (_∘_ ; homotopyNatural) -- Direct definition of transport filler, note that we have to -- explicitly tell Agda that the type is constant (like in CHM) @@ -63,6 +63,14 @@ transportTransport⁻ : ∀ {ℓ} {A B : Type ℓ} → (p : A ≡ B) → (b : B) transport p (transport⁻ p b) ≡ b transportTransport⁻ p b j = transport-fillerExt⁻ p j (transport⁻-fillerExt⁻ p j b) + +transportFillerExt[refl]∘TransportFillerExt⁻[refl] : ∀ {ℓ} {A : Type ℓ} → + (λ i → transp (λ j → A) (~ i) ∘ (transp (λ j → A) i)) ≡ refl +transportFillerExt[refl]∘TransportFillerExt⁻[refl] = + cong₂Funct (λ f g → f ∘ g) (transport-fillerExt refl) (transport-fillerExt⁻ refl) + ∙ cong funExt (funExt λ x → leftright _ _ ∙ + cong sym (sym (homotopyNatural transportRefl (sym (transportRefl x))) ∙ (rCancel _))) + subst⁻Subst : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} (B : A → Type ℓ') (p : x ≡ y) → (u : B x) → subst⁻ B p (subst B p u) ≡ u subst⁻Subst {x = x} {y = y} B p u = transport⁻Transport {A = B x} {B = B y} (cong B p) u @@ -205,3 +213,46 @@ module _ {ℓ : Level} {A : Type ℓ} {a x1 x2 : A} (p : x1 ≡ x2) where ≡⟨ assoc (sym p) q refl ⟩ (sym p ∙ q) ∙ refl ≡⟨ sym (rUnit (sym p ∙ q))⟩ sym p ∙ q ∎ + + + +comp-const : ∀ {ℓ} {A : Type ℓ} {a b c d : A} (p : a ≡ b) (q : b ≡ c) (r : c ≡ d) + → (p ∙∙ q ∙∙ r) ≡ λ i → comp (λ _ → A) (doubleComp-faces p r i) (q i) +comp-const {A = A} p q r j i = + hcomp (doubleComp-faces + (λ i₁ → transp (λ _ → A) (~ j ∨ ~ i₁) (p i₁)) + (λ i₁ → transp (λ _ → A) (~ j ∨ i₁) (r i₁)) i) + (transp (λ _ → A) (~ j) (q i)) + + +cong-transport-uaIdEquiv : ∀ {ℓ} {A : Type ℓ} → refl ≡ cong transport (uaIdEquiv {A = A}) +cong-transport-uaIdEquiv = + cong funExt (funExt λ x → + cong (cong (transport refl)) (lUnit _) + ∙ cong-∙∙ (transport refl) refl refl refl + ∙∙ congS (refl ∙∙_∙∙ refl) + (lUnit _ ∙ cong (refl ∙_) + λ i j → transportFillerExt[refl]∘TransportFillerExt⁻[refl] (~ i) (~ j) x) + ∙∙ comp-const refl _ refl) + + +transport-filler-ua : ∀ {ℓ} {A B : Type ℓ} (e : A ≃ B) (x : A) → + SquareP (λ _ i → ua e i) + (transport-filler (ua e) x) + (ua-gluePath e refl) + refl + (transportRefl (fst e x)) +transport-filler-ua {B = B} e x = + EquivJ (λ A e → ∀ x → SquareP (λ _ i → ua e i) (transport-filler (ua e) x) + (ua-gluePath e refl) refl (transportRefl (fst e x))) + (λ x j i → comp + (λ k → uaIdEquiv {A = B} (~ k) (~ i)) + (λ k → λ where + (i = i1) → transp (λ _ → B) j x + (i = i0) → transp (λ _ → B) (k ∨ j) x + (j = i0) → let d = transp (λ k' → Glue B {φ = ~ k' ∨ ~ i ∨ ~ k ∨ (k' ∧ i)} + λ _ → B , idEquiv B) (k ∧ ~ i) x + in hcomp (λ k' → primPOr _ (~ i ∨ k ∨ ~ k) + (λ where (i = i1) → cong-transport-uaIdEquiv (~ k') (~ k) x) λ _ → d) d + (j = i1) → glue (λ where (i = i0) → x ; (i = i1) → x ;(k = i0) → x) x + ) (transp (λ _ → B) j x)) e x diff --git a/Cubical/HITs/CumulativeHierarchy/Properties.agda b/Cubical/HITs/CumulativeHierarchy/Properties.agda index 65e3585c36..a71af74c83 100644 --- a/Cubical/HITs/CumulativeHierarchy/Properties.agda +++ b/Cubical/HITs/CumulativeHierarchy/Properties.agda @@ -151,7 +151,7 @@ sett-repr {ℓ} X ix = (Rep , ixRep , isEmbIxRep) , seteq X Rep ix ixRep eqImIxR Rep : Type ℓ Rep = X / Kernel ixRep : Rep → V ℓ - ixRep = invEq (setQuotUniversal setIsSet) (ix , λ _ _ → equivFun identityPrinciple) + ixRep = invEq (setQuotUniversal setIsSet) (ix , equivFun identityPrinciple) isEmbIxRep : isEmbedding ixRep isEmbIxRep = hasPropFibers→isEmbedding propFibers where propFibers : ∀ y → (a b : Σ[ p ∈ Rep ] (ixRep p ≡ y)) → a ≡ b diff --git a/Cubical/HITs/SetQuotients/Properties.agda b/Cubical/HITs/SetQuotients/Properties.agda index 02ca17a0f3..16273bf0fa 100644 --- a/Cubical/HITs/SetQuotients/Properties.agda +++ b/Cubical/HITs/SetQuotients/Properties.agda @@ -188,9 +188,9 @@ module rec→Gpd {B : Type ℓ''} (Bgpd : isGroupoid B) setQuotUniversalIso : isSet B - → Iso (A / R → B) (Σ[ f ∈ (A → B) ] ((a b : A) → R a b → f a ≡ f b)) -Iso.fun (setQuotUniversalIso Bset) g = (λ a → g [ a ]) , λ a b r i → g (eq/ a b r i) -Iso.inv (setQuotUniversalIso Bset) h = rec Bset (fst h) (snd h) + → Iso (A / R → B) (Σ[ f ∈ (A → B) ] ({a b : A} → R a b → f a ≡ f b)) +Iso.fun (setQuotUniversalIso Bset) g = (λ a → g [ a ]) , λ r i → g (eq/ _ _ r i) +Iso.inv (setQuotUniversalIso Bset) h = rec Bset (fst h) (λ _ _ → snd h) Iso.rightInv (setQuotUniversalIso Bset) h = refl Iso.leftInv (setQuotUniversalIso Bset) g = funExt λ x → @@ -203,7 +203,7 @@ Iso.leftInv (setQuotUniversalIso Bset) g = out = Iso.inv (setQuotUniversalIso Bset) setQuotUniversal : isSet B - → (A / R → B) ≃ (Σ[ f ∈ (A → B) ] ((a b : A) → R a b → f a ≡ f b)) + → (A / R → B) ≃ (Σ[ f ∈ (A → B) ] ({a b : A} → R a b → f a ≡ f b)) setQuotUniversal Bset = isoToEquiv (setQuotUniversalIso Bset) open BinaryRelation diff --git a/Cubical/Relation/Binary/Base.agda b/Cubical/Relation/Binary/Base.agda index 2f78c4dbf5..2087184dc9 100644 --- a/Cubical/Relation/Binary/Base.agda +++ b/Cubical/Relation/Binary/Base.agda @@ -6,13 +6,16 @@ open import Cubical.Core.Everything open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function open import Cubical.Foundations.Equiv open import Cubical.Foundations.Equiv.Fiberwise open import Cubical.Functions.Embedding -open import Cubical.Functions.Logic using (_⊔′_) +open import Cubical.Functions.Logic using (_⊔′_;⇔toPath) +open import Cubical.Functions.FunExtEquiv open import Cubical.Data.Empty as ⊥ open import Cubical.Data.Sigma +open import Cubical.Data.Unit open import Cubical.Data.Sum.Base as ⊎ open import Cubical.HITs.SetQuotients.Base open import Cubical.HITs.PropositionalTruncation as ∥₁ @@ -22,6 +25,7 @@ open import Cubical.Relation.Nullary.Base private variable ℓA ℓ≅A ℓA' ℓ≅A' : Level + A A' : Type ℓA Rel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ')) Rel A B ℓ' = A → B → Type ℓ' @@ -29,10 +33,31 @@ Rel A B ℓ' = A → B → Type ℓ' PropRel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ')) PropRel A B ℓ' = Σ[ R ∈ Rel A B ℓ' ] ∀ a b → isProp (R a b) +isSetPropRel : isSet (PropRel A A' ℓ≅A) +isSetPropRel {A = A} {A' = A'} = isOfHLevelRetract 2 _ + (λ r → _ , λ x y → snd (r x y) ) (λ _ → refl) (isSet→ (isSet→ isSetHProp) ) + +PropRel≡ : {R R' : PropRel A A' ℓ≅A} → + (∀ {x y} → ((fst R) x y → (fst R') x y) × + ((fst R') x y → (fst R) x y)) + → (R ≡ R') +PropRel≡ {R = _ , R} {_ , R'} x = + (Σ≡Prop (λ _ → isPropΠ2 λ _ _ → isPropIsProp) + (funExt₂ λ _ _ → cong fst (⇔toPath + {P = _ , R _ _} + {_ , R' _ _} (fst x) (snd x)))) + +idRel : Rel A A _ +idRel = _≡_ + idPropRel : ∀ {ℓ} (A : Type ℓ) → PropRel A A ℓ idPropRel A .fst a a' = ∥ a ≡ a' ∥₁ idPropRel A .snd _ _ = squash₁ +fullPropRel : PropRel A A' ℓ≅A +fst fullPropRel _ _ = Unit* +snd fullPropRel _ _ = isPropUnit* + invPropRel : ∀ {ℓ ℓ'} {A B : Type ℓ} → PropRel A B ℓ' → PropRel B A ℓ' invPropRel R .fst b a = R .fst a b @@ -54,6 +79,10 @@ module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where isRefl : Type (ℓ-max ℓ ℓ') isRefl = (a : A) → R a a + isRefl' : Type (ℓ-max ℓ ℓ') + isRefl' = {a : A} → R a a + + isIrrefl : Type (ℓ-max ℓ ℓ') isIrrefl = (a : A) → ¬ R a a @@ -69,6 +98,9 @@ module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where isTrans : Type (ℓ-max ℓ ℓ') isTrans = (a b c : A) → R a b → R b c → R a c + isTrans' : Type (ℓ-max ℓ ℓ') + isTrans' = {a b c : A} → R a b → R b c → R a c + -- Sum types don't play nicely with props, so we truncate isCotrans : Type (ℓ-max ℓ ℓ') isCotrans = (a b c : A) → R a b → (R a c ⊔′ R b c) @@ -130,6 +162,9 @@ module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where symmetric : isSym transitive : isTrans + transitive' : isTrans' + transitive' = transitive _ _ _ + isUniversalRel→isEquivRel : HeterogenousRelation.isUniversalRel R → isEquivRel isUniversalRel→isEquivRel u .isEquivRel.reflexive a = u a a isUniversalRel→isEquivRel u .isEquivRel.symmetric a b _ = u b a @@ -149,6 +184,15 @@ module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where impliesIdentity : Type _ impliesIdentity = {a a' : A} → (R a a') → (a ≡ a') + impliedByIdentity : Type _ + impliedByIdentity = {a a' : A} → (a ≡ a') → (R a a') + + isRefl→impliedByIdentity : isRefl → impliedByIdentity + isRefl→impliedByIdentity is-refl p = subst (R _) p (is-refl _) + + impliedByIdentity→isRefl : impliedByIdentity → isRefl + impliedByIdentity→isRefl imp-by-id _ = imp-by-id refl + inequalityImplies : Type _ inequalityImplies = (a b : A) → ¬ a ≡ b → R a b @@ -163,6 +207,9 @@ module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where isUnivalent : Type (ℓ-max ℓ ℓ') isUnivalent = (a a' : A) → (R a a') ≃ (a ≡ a') + isFull : Type (ℓ-max ℓ ℓ') + isFull = (a a' : A) → (R a a') + contrRelSingl→isUnivalent : isRefl → contrRelSingl → isUnivalent contrRelSingl→isUnivalent ρ c a a' = isoToEquiv i where @@ -196,6 +243,13 @@ module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where q : isContr (relSinglAt a) q = isOfHLevelRespectEquiv 0 (t , totalEquiv _ _ f λ x → invEquiv (u a x) .snd) (isContrSingl a) + isPropIsEquivPropRel : isPropValued → isProp isEquivRel + isPropIsEquivPropRel ipv = + isOfHLevelRetract 1 _ (uncurry (uncurry equivRel)) + (λ _ → refl) + (isProp× (isProp× (isPropΠ λ _ → ipv _ _) + (isPropΠ2 λ _ _ → isProp→ (ipv _ _))) + (isPropΠ3 λ _ _ _ → isProp→ (isProp→ (ipv _ _)))) EquivRel : ∀ {ℓ} (A : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ')) EquivRel A ℓ' = Σ[ R ∈ Rel A A ℓ' ] BinaryRelation.isEquivRel R @@ -203,6 +257,39 @@ EquivRel A ℓ' = Σ[ R ∈ Rel A A ℓ' ] BinaryRelation.isEquivRel R EquivPropRel : ∀ {ℓ} (A : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ')) EquivPropRel A ℓ' = Σ[ R ∈ PropRel A A ℓ' ] BinaryRelation.isEquivRel (R .fst) +EquivPropRel→Rel : EquivPropRel A ℓA → Rel A A ℓA +EquivPropRel→Rel ((r , _) , _) = r + +isSetEquivPropRel : isSet (EquivPropRel A ℓ≅A) +isSetEquivPropRel = isSetΣ isSetPropRel + (isProp→isSet ∘ BinaryRelation.isPropIsEquivPropRel _ ∘ snd ) + +EquivPropRel≡ : {R R' : EquivPropRel A ℓ≅A} → + (∀ {x y} → (fst (fst R) x y → fst (fst R') x y) × + (fst (fst R') x y → fst (fst R) x y)) + → (R ≡ R') +EquivPropRel≡ {R = (_ , R) , _} {(_ , R') , _} x = + Σ≡Prop (BinaryRelation.isPropIsEquivPropRel _ ∘ snd ) (PropRel≡ x) + +isEquivEquivPropRel≡ : {R R' : EquivPropRel A ℓ≅A} + → isEquiv (EquivPropRel≡ {R = R} {R'}) +isEquivEquivPropRel≡ {R = (_ , R) , _} {(_ , R') , _} = + snd (propBiimpl→Equiv + ((isPropImplicitΠ2 λ _ _ → + isProp× (isProp→ (R' _ _)) (isProp→ (R _ _)))) + (isSetEquivPropRel _ _) _ + λ p {x y} → (subst (λ R → fst (fst R) x y) p) , + (subst (λ R → fst (fst R) x y) (sym p))) + +fullEquivPropRel : EquivPropRel A ℓ≅A +fst fullEquivPropRel = fullPropRel +snd fullEquivPropRel = _ + +isEquivRelIdRel : BinaryRelation.isEquivRel (idRel {A = A}) +BinaryRelation.isEquivRel.reflexive isEquivRelIdRel _ = refl +BinaryRelation.isEquivRel.symmetric isEquivRelIdRel _ _ = sym +BinaryRelation.isEquivRel.transitive isEquivRelIdRel _ _ _ = _∙_ + record RelIso {A : Type ℓA} (_≅_ : Rel A A ℓ≅A) {A' : Type ℓA'} (_≅'_ : Rel A' A' ℓ≅A') : Type (ℓ-max (ℓ-max ℓA ℓA') (ℓ-max ℓ≅A ℓ≅A')) where constructor reliso @@ -249,3 +336,17 @@ isSymSymClosure _ _ _ (inr Rba) = inl Rba isAsymAsymKernel : ∀ {ℓ ℓ'} {A : Type ℓ} (R : Rel A A ℓ') → isAsym (AsymKernel R) isAsymAsymKernel _ _ _ (Rab , _) (_ , ¬Rab) = ¬Rab Rab + +respects : (R : Rel A A ℓ≅A) (R' : Rel A' A' ℓ≅A') → + (A → A') → Type _ +respects _R_ _R'_ f = ∀ {x x'} → x R x' → f x R' f x' + +private + variable + R : Rel A A ℓ≅A + R' : Rel A' A' ℓ≅A' + +isPropRespects : isPropValued R' + → (f : A → A') → isProp (respects R R' f) +isPropRespects isPropRelR' f = + isPropImplicitΠ2 λ _ _ → isPropΠ λ _ → isPropRelR' _ _ diff --git a/Cubical/Relation/Binary/Properties.agda b/Cubical/Relation/Binary/Properties.agda index 545dac739a..8ade5697d7 100644 --- a/Cubical/Relation/Binary/Properties.agda +++ b/Cubical/Relation/Binary/Properties.agda @@ -3,39 +3,98 @@ module Cubical.Relation.Binary.Properties where open import Cubical.Foundations.Prelude open import Cubical.Relation.Binary.Base +open import Cubical.Foundations.Function +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.HLevels +open import Cubical.Functions.FunExtEquiv +open import Cubical.Data.Sigma private variable - ℓ : Level - A B : Type ℓ + ℓA ℓA' ℓB ℓB' : Level + A : Type ℓA + B : Type ℓB + f : A → B + rA : Rel A A ℓA' + rB : Rel B B ℓB' +open BinaryRelation --- Pulling back a relation along a function. --- This can for example be used when restricting an equivalence relation to a subset: --- _~'_ = on fst _~_ +module _ (R : Rel B B ℓB') where -module _ - (f : A → B) - (R : Rel B B ℓ) - where + -- Pulling back a relation along a function. + -- This can for example be used when restricting an equivalence relation to a subset: + -- _~'_ = on fst _~_ - open BinaryRelation + pulledbackRel : (A → B) → Rel A A ℓB' + pulledbackRel f x y = R (f x) (f y) - pulledbackRel : Rel A A ℓ - pulledbackRel x y = R (f x) (f y) + funRel : Rel (A → B) (A → B) _ + funRel f g = ∀ x → R (f x) (g x) - isReflPulledbackRel : isRefl R → isRefl pulledbackRel - isReflPulledbackRel isReflR a = isReflR (f a) +module _ (isEquivRelR : isEquivRel rB) where + open isEquivRel - isSymPulledbackRel : isSym R → isSym pulledbackRel - isSymPulledbackRel isSymR a a' = isSymR (f a) (f a') + isEquivRelPulledbackRel : (f : A → _) → isEquivRel (pulledbackRel rB f) + reflexive (isEquivRelPulledbackRel _) _ = reflexive isEquivRelR _ + symmetric (isEquivRelPulledbackRel _) _ _ = symmetric isEquivRelR _ _ + transitive (isEquivRelPulledbackRel _) _ _ _ = transitive isEquivRelR _ _ _ - isTransPulledbackRel : isTrans R → isTrans pulledbackRel - isTransPulledbackRel isTransR a a' a'' = isTransR (f a) (f a') (f a'') + isEquivRelFunRel : isEquivRel (funRel rB {A = A}) + reflexive isEquivRelFunRel _ _ = + reflexive isEquivRelR _ + symmetric isEquivRelFunRel _ _ = + symmetric isEquivRelR _ _ ∘_ + transitive isEquivRelFunRel _ _ _ u v _ = + transitive isEquivRelR _ _ _ (u _) (v _) - open isEquivRel +module _ (rA : Rel A A ℓA') (rB : Rel B B ℓB') where - isEquivRelPulledbackRel : isEquivRel R → isEquivRel pulledbackRel - reflexive (isEquivRelPulledbackRel isEquivRelR) = isReflPulledbackRel (reflexive isEquivRelR) - symmetric (isEquivRelPulledbackRel isEquivRelR) = isSymPulledbackRel (symmetric isEquivRelR) - transitive (isEquivRelPulledbackRel isEquivRelR) = isTransPulledbackRel (transitive isEquivRelR) + ×Rel : Rel (A × B) (A × B) (ℓ-max ℓA' ℓB') + ×Rel (a , b) (a' , b') = (rA a a') × (rB b b') + + +module _ (isEquivRelRA : isEquivRel rA) (isEquivRelRB : isEquivRel rB) where + open isEquivRel + + module eqrA = isEquivRel isEquivRelRA + module eqrB = isEquivRel isEquivRelRB + + isEquivRel×Rel : isEquivRel (×Rel rA rB) + reflexive isEquivRel×Rel _ = + eqrA.reflexive _ , eqrB.reflexive _ + symmetric isEquivRel×Rel _ _ = + map-× (eqrA.symmetric _ _) (eqrB.symmetric _ _) + transitive isEquivRel×Rel _ _ _ (ra , rb) = + map-× (eqrA.transitive _ _ _ ra) (eqrB.transitive _ _ _ rb) + + +module _ {A B : Type ℓA} (e : A ≃ B) {_∼_ : Rel A A ℓA'} {_∻_ : Rel B B ℓA'} + (_h_ : ∀ x y → (x ∼ y) ≃ ((fst e x) ∻ (fst e y))) where + + RelPathP : PathP (λ i → ua e i → ua e i → Type _) + _∼_ _∻_ + RelPathP i x y = Glue (ua-unglue e i x ∻ ua-unglue e i y) + λ { (i = i0) → _ , x h y + ; (i = i1) → _ , idEquiv _ } + + +module _ {ℓ''} {B : Type ℓB} {_∻_ : B → B → Type ℓB'} where + + JRelPathP-Goal : Type _ + JRelPathP-Goal = ∀ (A : Type ℓB) (e : A ≃ B) (_~_ : A → A → Type ℓB') + → (_h_ : ∀ x y → x ~ y ≃ (fst e x ∻ fst e y)) → Type ℓ'' + + + EquivJRel : (Goal : JRelPathP-Goal) + → (Goal _ (idEquiv _) _∻_ λ _ _ → idEquiv _ ) + → ∀ {A} e _~_ _h_ → Goal A e _~_ _h_ + EquivJRel Goal g {A} = EquivJ (λ A e → ∀ _~_ _h_ → Goal A e _~_ _h_) + λ _~_ _h_ → subst (uncurry (Goal B (idEquiv B))) + ((isPropRetract + (map-snd (λ r → funExt₂ λ x y → sym (ua (r x y)))) + (map-snd (λ r x y → pathToEquiv λ i → r (~ i) x y)) + (λ (o , r) → cong (o ,_) (funExt₂ λ x y → equivEq + (funExt λ _ → transportRefl _))) + (isPropSingl {a = _∻_})) _ _) g diff --git a/Cubical/Relation/Binary/Setoid.agda b/Cubical/Relation/Binary/Setoid.agda new file mode 100644 index 0000000000..ec3bbb9cef --- /dev/null +++ b/Cubical/Relation/Binary/Setoid.agda @@ -0,0 +1,79 @@ +{- + +This module defines a 'Setoid' as a pair consisting of an hSet and a propositional equivalence relation over it. + +In contrast to the standard Agda library where setoids act as carriers for different algebraic structures, this usage is not relevant in cubical-agda context due to the availability of set quotients. + +The Setoids from this module are given categorical structure in Cubical.Categories.Instances.Setoids. + +-} + + +{-# OPTIONS --safe #-} +module Cubical.Relation.Binary.Setoid where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Isomorphism +open import Cubical.Relation.Binary.Base +open import Cubical.Relation.Binary.Properties +open import Cubical.Data.Sigma + +private + variable + ℓX ℓX' ℓA ℓ≅A ℓA' ℓ≅A' : Level + A : Type ℓA + A' : Type ℓA' + +Setoid : ∀ ℓA ℓ≅A → Type (ℓ-suc (ℓ-max ℓA ℓ≅A)) +Setoid ℓA ℓ≅A = Σ (hSet ℓA) λ (X , _) → EquivPropRel X ℓ≅A + +SetoidMor : (Setoid ℓA ℓ≅A) → (Setoid ℓA' ℓ≅A') → Type _ +SetoidMor (_ , ((R , _) , _)) (_ , ((R' , _) , _)) = Σ _ (respects R R') + +isSetSetoidMor : + {A : Setoid ℓA ℓ≅A} + {A' : Setoid ℓA' ℓ≅A'} + → isSet (SetoidMor A A') +isSetSetoidMor {A' = (_ , isSetB) , ((_ , isPropR) , _)} = + isSetΣ (isSet→ isSetB) (isProp→isSet ∘ isPropRespects isPropR ) + +SetoidMor≡ : ∀ A A' → {f g : SetoidMor {ℓA = ℓA} {ℓ≅A} {ℓA'} {ℓ≅A'} A A'} + → fst f ≡ fst g → f ≡ g +SetoidMor≡ _ ((_ , (_ , pr) , _)) = Σ≡Prop (isPropRespects pr) + +substRel : ∀ {x y : A'} → {f g : A' → A} → (R : Rel A A ℓ≅A) + → (∀ x → f x ≡ g x) → + R (f x) (f y) → R (g x) (g y) +substRel R p = subst2 R (p _) (p _) + +_⊗_ : (Setoid ℓA ℓ≅A) → (Setoid ℓA' ℓ≅A') + → Setoid (ℓ-max ℓA ℓA') (ℓ-max ℓ≅A ℓ≅A') +((_ , isSetA) , ((_ , pr) , eqr)) ⊗ ((_ , isSetA') , ((_ , pr') , eqr')) = + (_ , isSet× isSetA isSetA') + , (_ , λ _ _ → isProp× (pr _ _) (pr' _ _)) , + isEquivRel×Rel eqr eqr' + +_⟶_ : (Setoid ℓA ℓ≅A) → (Setoid ℓA' ℓ≅A') → Setoid _ _ +A@((⟨A⟩ , _) , ((R , _) , _)) ⟶ A'@(_ , ((_ , pr) , eqr)) = + (_ , isSetSetoidMor {A = A} {A'}) , + (_ , λ _ _ → isPropΠ λ _ → pr _ _) , + isEquivRelPulledbackRel (isEquivRelFunRel eqr {A = ⟨A⟩}) fst + +open Iso + +setoidCurryIso : + (X : Setoid ℓX ℓX') (A : Setoid ℓA ℓ≅A) (B : Setoid ℓA' ℓ≅A') + → Iso (SetoidMor (A ⊗ X) B) + (SetoidMor A (X ⟶ B)) +fun (setoidCurryIso (_ , (_ , Rx)) (_ , (_ , Ra)) _ ) (f , p) = + (λ _ → curry f _ , p {_ , _} {_ , _} ∘ (reflexive Ra _ ,_)) , + flip λ _ → p {_ , _} {_ , _} ∘ (_, reflexive Rx _) + where open BinaryRelation.isEquivRel +inv (setoidCurryIso X _ (_ , (_ , Rb))) (f , p) = (uncurry (fst ∘ f)) + , λ (a~a' , b~b') → transitive' (p a~a' _) (snd (f _) b~b') + where open BinaryRelation.isEquivRel Rb using (transitive') +rightInv (setoidCurryIso X A B) _ = + SetoidMor≡ A (X ⟶ B) (funExt λ _ → SetoidMor≡ X B refl) +leftInv (setoidCurryIso X A B) _ = SetoidMor≡ (A ⊗ X) B refl From 8cd6eeb607af6f33568803249d14ff8762bc76e4 Mon Sep 17 00:00:00 2001 From: Marcin Grzybowski Date: Tue, 5 Dec 2023 02:48:24 +0100 Subject: [PATCH 02/17] simplified transport-filler-ua, as sugested by Tom Jack on Univalent Agda Discord --- Cubical/Foundations/Transport.agda | 58 ++++++------------------------ 1 file changed, 11 insertions(+), 47 deletions(-) diff --git a/Cubical/Foundations/Transport.agda b/Cubical/Foundations/Transport.agda index 06f2e9f3eb..d84f467813 100644 --- a/Cubical/Foundations/Transport.agda +++ b/Cubical/Foundations/Transport.agda @@ -63,14 +63,6 @@ transportTransport⁻ : ∀ {ℓ} {A B : Type ℓ} → (p : A ≡ B) → (b : B) transport p (transport⁻ p b) ≡ b transportTransport⁻ p b j = transport-fillerExt⁻ p j (transport⁻-fillerExt⁻ p j b) - -transportFillerExt[refl]∘TransportFillerExt⁻[refl] : ∀ {ℓ} {A : Type ℓ} → - (λ i → transp (λ j → A) (~ i) ∘ (transp (λ j → A) i)) ≡ refl -transportFillerExt[refl]∘TransportFillerExt⁻[refl] = - cong₂Funct (λ f g → f ∘ g) (transport-fillerExt refl) (transport-fillerExt⁻ refl) - ∙ cong funExt (funExt λ x → leftright _ _ ∙ - cong sym (sym (homotopyNatural transportRefl (sym (transportRefl x))) ∙ (rCancel _))) - subst⁻Subst : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} (B : A → Type ℓ') (p : x ≡ y) → (u : B x) → subst⁻ B p (subst B p u) ≡ u subst⁻Subst {x = x} {y = y} B p u = transport⁻Transport {A = B x} {B = B y} (cong B p) u @@ -215,44 +207,16 @@ module _ {ℓ : Level} {A : Type ℓ} {a x1 x2 : A} (p : x1 ≡ x2) where ≡⟨ sym (rUnit (sym p ∙ q))⟩ sym p ∙ q ∎ - -comp-const : ∀ {ℓ} {A : Type ℓ} {a b c d : A} (p : a ≡ b) (q : b ≡ c) (r : c ≡ d) - → (p ∙∙ q ∙∙ r) ≡ λ i → comp (λ _ → A) (doubleComp-faces p r i) (q i) -comp-const {A = A} p q r j i = - hcomp (doubleComp-faces - (λ i₁ → transp (λ _ → A) (~ j ∨ ~ i₁) (p i₁)) - (λ i₁ → transp (λ _ → A) (~ j ∨ i₁) (r i₁)) i) - (transp (λ _ → A) (~ j) (q i)) - - -cong-transport-uaIdEquiv : ∀ {ℓ} {A : Type ℓ} → refl ≡ cong transport (uaIdEquiv {A = A}) -cong-transport-uaIdEquiv = - cong funExt (funExt λ x → - cong (cong (transport refl)) (lUnit _) - ∙ cong-∙∙ (transport refl) refl refl refl - ∙∙ congS (refl ∙∙_∙∙ refl) - (lUnit _ ∙ cong (refl ∙_) - λ i j → transportFillerExt[refl]∘TransportFillerExt⁻[refl] (~ i) (~ j) x) - ∙∙ comp-const refl _ refl) - - -transport-filler-ua : ∀ {ℓ} {A B : Type ℓ} (e : A ≃ B) (x : A) → - SquareP (λ _ i → ua e i) - (transport-filler (ua e) x) +transport-filler-ua : ∀ {ℓ} {A B : Type ℓ} (e : A ≃ B) (a : A) + → SquareP (λ _ i → ua e i) + (transport-filler (ua e) a) (ua-gluePath e refl) refl - (transportRefl (fst e x)) -transport-filler-ua {B = B} e x = - EquivJ (λ A e → ∀ x → SquareP (λ _ i → ua e i) (transport-filler (ua e) x) - (ua-gluePath e refl) refl (transportRefl (fst e x))) - (λ x j i → comp - (λ k → uaIdEquiv {A = B} (~ k) (~ i)) - (λ k → λ where - (i = i1) → transp (λ _ → B) j x - (i = i0) → transp (λ _ → B) (k ∨ j) x - (j = i0) → let d = transp (λ k' → Glue B {φ = ~ k' ∨ ~ i ∨ ~ k ∨ (k' ∧ i)} - λ _ → B , idEquiv B) (k ∧ ~ i) x - in hcomp (λ k' → primPOr _ (~ i ∨ k ∨ ~ k) - (λ where (i = i1) → cong-transport-uaIdEquiv (~ k') (~ k) x) λ _ → d) d - (j = i1) → glue (λ where (i = i0) → x ; (i = i1) → x ;(k = i0) → x) x - ) (transp (λ _ → B) j x)) e x + (transportRefl (fst e a)) +transport-filler-ua {A = A} {B = B} (e , _) a j i = + let b = e a + tr = transportRefl b + z = tr (j ∧ ~ i) + in glue (λ { (i = i0) → a ; (i = i1) → tr j }) + (hcomp (λ k → λ { (i = i0) → b ; (i = i1) → tr (j ∧ k) ; (j = i1) → tr (~ i ∨ k) }) + (hcomp (λ k → λ { (i = i0) → tr (j ∨ k) ; (i = i1) → z ; (j = i1) → z }) z)) From d48cf4b4e2a831ab03fd9bbfbc242d6dd78f31ca Mon Sep 17 00:00:00 2001 From: Marcin Grzybowski Date: Tue, 5 Dec 2023 02:59:02 +0100 Subject: [PATCH 03/17] formatting fix --- .../Categories/Equivalence/WeakEquivalence.agda | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/Cubical/Categories/Equivalence/WeakEquivalence.agda b/Cubical/Categories/Equivalence/WeakEquivalence.agda index bad20dd855..45707f5b18 100644 --- a/Cubical/Categories/Equivalence/WeakEquivalence.agda +++ b/Cubical/Categories/Equivalence/WeakEquivalence.agda @@ -168,15 +168,14 @@ module _ (transport-fillerExt⁻ (ob≡ b)) j)) λ i j x y → Glue (𝑪'.Hom[ unglue _ x , unglue _ y ]) - λ { (j = i0) → _ , Hom≃ (isWeakEquivalenceTransportFunctor (mk≡ b)) _ _ - ;(j = i1) → _ , idEquiv _ - ;(i = i1) → _ , _ - , isProp→PathP (λ j → isPropΠ2 λ x y → - isPropIsEquiv (transp (λ i₂ → - let tr = transp (λ j' → ob≡ b (j ∨ (i₂ ∧ j'))) (~ i₂ ∨ j) - in Hom≡ b (i₂ ∨ j) (tr x) (tr y)) j)) - (λ _ _ → snd (Hom≃ (isWeakEquivalenceTransportFunctor (mk≡ b)) _ _)) - (λ _ _ → snd (idEquiv _)) j x y } + λ { (j = i0) → _ , Hom≃ (isWeakEquivalenceTransportFunctor (mk≡ b)) _ _ + ;(j = i1) → _ , idEquiv _ + ;(i = i1) → _ , _ + , isProp→PathP (λ j → isPropΠ2 λ x y → isPropIsEquiv (transp (λ i₂ → + let tr = transp (λ j' → ob≡ b (j ∨ (i₂ ∧ j'))) (~ i₂ ∨ j) + in Hom≡ b (i₂ ∨ j) (tr x) (tr y)) j)) + (λ _ _ → snd (Hom≃ (isWeakEquivalenceTransportFunctor (mk≡ b)) _ _)) + (λ _ _ → snd (idEquiv _)) j x y } leftInv IsoCategoryPath we = cong₂ weakEquivalence (Functor≡ (transportRefl ∘f (F-ob (func we))) From 7ebe15db4a8b571f41d9371e0384d05a696d2c40 Mon Sep 17 00:00:00 2001 From: Marcin Grzybowski Date: Mon, 15 Jan 2024 06:26:45 +0100 Subject: [PATCH 04/17] setoids are not LCCC, Sets are --- Cubical/Categories/Category/Path.agda | 7 +- .../Constructions/Slice/Functor.agda | 129 ++++ .../Constructions/Slice/Properties.agda | 4 +- .../Equivalence/WeakEquivalence.agda | 25 +- Cubical/Categories/Instances/Setoids.agda | 595 +++++++++++++++++- Cubical/Categories/Instances/Sets.agda | 29 + Cubical/Categories/Monoidal/Enriched.agda | 2 +- Cubical/Data/Bool/Properties.agda | 22 + Cubical/Data/Sigma/Properties.agda | 3 + Cubical/Foundations/HLevels.agda | 8 + Cubical/Relation/Binary/Base.agda | 1 + Cubical/Relation/Binary/Properties.agda | 24 +- Cubical/Relation/Binary/Setoid.agda | 113 ++++ 13 files changed, 952 insertions(+), 10 deletions(-) create mode 100644 Cubical/Categories/Constructions/Slice/Functor.agda diff --git a/Cubical/Categories/Category/Path.agda b/Cubical/Categories/Category/Path.agda index b87b0b54dd..e420487376 100644 --- a/Cubical/Categories/Category/Path.agda +++ b/Cubical/Categories/Category/Path.agda @@ -31,7 +31,7 @@ private ℓ ℓ' : Level record CategoryPath (C C' : Category ℓ ℓ') : Type (ℓ-suc (ℓ-max ℓ ℓ')) where - constructor categoryPath + no-eta-equality field ob≡ : C .ob ≡ C' .ob Hom≡ : PathP (λ i → ob≡ i → ob≡ i → Type ℓ') (C .Hom[_,_]) (C' .Hom[_,_]) @@ -114,7 +114,10 @@ module _ {C C' : Category ℓ ℓ'} where isSetHom c = isProp→SquareP (λ i j → isPropImplicitΠ2 λ x y → isPropIsSet {A = c'.Hom[_,_] j x y}) refl refl (λ j → b' j .isSetHom) (λ j → c'.isSetHom j) i j - Iso.leftInv CategoryPathIso a = refl + ob≡ (Iso.leftInv CategoryPathIso a i) = ob≡ a + Hom≡ (Iso.leftInv CategoryPathIso a i) = Hom≡ a + id≡ (Iso.leftInv CategoryPathIso a i) = id≡ a + ⋆≡ (Iso.leftInv CategoryPathIso a i) = ⋆≡ a CategoryPath≡ : {cp cp' : CategoryPath C C'} → (p≡ : ob≡ cp ≡ ob≡ cp') → diff --git a/Cubical/Categories/Constructions/Slice/Functor.agda b/Cubical/Categories/Constructions/Slice/Functor.agda new file mode 100644 index 0000000000..2ebaf36db4 --- /dev/null +++ b/Cubical/Categories/Constructions/Slice/Functor.agda @@ -0,0 +1,129 @@ +{-# OPTIONS --safe #-} + +module Cubical.Categories.Constructions.Slice.Functor where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Structure +open import Cubical.Foundations.Function +open import Cubical.Data.Sigma + +open import Cubical.HITs.PropositionalTruncation using (∣_∣₁) + +open import Cubical.Categories.Category +open import Cubical.Categories.Category.Properties +open import Cubical.Categories.Constructions.Slice.Base +open import Cubical.Categories.Constructions.Slice.Properties + +open import Cubical.Categories.Limits.Pullback +open import Cubical.Categories.Equivalence +open import Cubical.Categories.Functor +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Adjoint + +open Category hiding (_∘_) +open _≃ᶜ_ +open Functor +open NatTrans + +private + variable + ℓ ℓ' : Level + C D : Category ℓ ℓ' + +F/ : ∀ c (F : Functor C D) → Functor (SliceCat C c) (SliceCat D (F ⟅ c ⟆)) +F-ob (F/ c F) = sliceob ∘ F-hom F ∘ S-arr +F-hom (F/ c F) h = slicehom _ + (sym ( F-seq F _ _) ∙ cong (F-hom F) (S-comm h)) +F-id (F/ c F) = SliceHom-≡-intro' _ _ (F-id F) +F-seq (F/ c F) _ _ = SliceHom-≡-intro' _ _ (F-seq F _ _) + + +module _ (Pbs : Pullbacks C) (c : C .ob) where + + open Pullback + + module _ {Y} (f : C [ c , Y ]) where + + private module _ (x : SliceCat C Y .ob) where + pb = Pbs (cospan c Y _ f (x .S-arr)) + + module _ {y : SliceCat C Y .ob} (h : (SliceCat C Y) [ y , x ]) where + + pbU : _ + pbU = let pbx = Pbs (cospan c Y _ f (y .S-arr)) + in univProp pb + (pbPr₁ pbx) (h .S-hom ∘⟨ C ⟩ pbPr₂ pbx) + (pbCommutes pbx ∙∙ + cong (C ⋆ pbPr₂ (Pbs (cospan c Y (S-ob y) _ (y .S-arr)))) + (sym (h .S-comm)) ∙∙ sym (C .⋆Assoc _ _ _)) + + PbFunctor : Functor (SliceCat C Y) (SliceCat C c) + F-ob PbFunctor x = sliceob (pbPr₁ (pb x)) + F-hom PbFunctor {x} {y} f = + let ((f' , (u , _)) , _) = pbU y f + in slicehom f' (sym u) + + F-id PbFunctor = + SliceHom-≡-intro' _ _ (cong fst (pbU _ _ .snd + (_ , sym (C .⋆IdL _) , C .⋆IdR _ ∙ sym (C .⋆IdL _)))) + F-seq PbFunctor _ _ = + let (u₁ , v₁) = pbU _ _ .fst .snd + (u₂ , v₂) = pbU _ _ .fst .snd + in SliceHom-≡-intro' _ _ (cong fst (pbU _ _ .snd + (_ , u₂ ∙∙ cong (C ⋆ _) u₁ ∙∙ sym (C .⋆Assoc _ _ _) + , (sym (C .⋆Assoc _ _ _) ∙∙ cong (λ x → (C ⋆ x) _) v₂ ∙∙ + AssocCong₂⋆R {C = C} _ v₁)))) + + + open UnitCounit + + module SlicedAdjoint {L : Functor C D} {R} (L⊣R : L ⊣ R) where + +-- -- L/b : Functor (SliceCat C c) (SliceCat D (L ⟅ c ⟆)) +-- -- F-ob L/b (sliceob S-arr) = sliceob (F-hom L S-arr) +-- -- F-hom L/b (slicehom S-hom S-comm) = +-- -- slicehom _ (sym ( F-seq L _ _) ∙ cong (F-hom L) S-comm) +-- -- F-id L/b = SliceHom-≡-intro' _ _ (F-id L) +-- -- F-seq L/b _ _ = SliceHom-≡-intro' _ _ (F-seq L _ _) + + -- R' : Functor (SliceCat D (L ⟅ c ⟆)) (SliceCat C (funcComp R L .F-ob c)) + -- F-ob R' (sliceob S-arr) = sliceob (F-hom R S-arr) + -- F-hom R' (slicehom S-hom S-comm) = slicehom _ (sym ( F-seq R _ _) ∙ cong (F-hom R) S-comm) + -- F-id R' = SliceHom-≡-intro' _ _ (F-id R) + -- F-seq R' _ _ = SliceHom-≡-intro' _ _ (F-seq R _ _) + +-- -- -- R/b : Functor (SliceCat D (L ⟅ c ⟆)) (SliceCat C c) +-- -- -- R/b = BaseChangeFunctor.BaseChangeFunctor Pbs (N-ob (_⊣_.η L⊣R) c) +-- -- -- ∘F R' + module 𝑪 = Category C + module 𝑫 = Category D + + open _⊣_ L⊣R + + F/⊣ : Functor (SliceCat D (L ⟅ c ⟆)) (SliceCat C c) + F/⊣ = PbFunctor (N-ob η c) ∘F F/ (L ⟅ c ⟆) R + + L/b⊣R/b : F/ c L ⊣ F/⊣ + N-ob (_⊣_.η L/b⊣R/b) x = + slicehom {!(N-ob η $ S-ob x)!} {!!} + N-hom (_⊣_.η L/b⊣R/b) = {!!} + N-ob (_⊣_.ε L/b⊣R/b) x = + slicehom ({!F-hom L ?!} 𝑫.⋆ (N-ob ε $ S-ob x)) {!!} + N-hom (_⊣_.ε L/b⊣R/b) = {!!} + _⊣_.triangleIdentities L/b⊣R/b = {!!} + -- N-ob (_⊣_.η L/b⊣R/b) x = + -- slicehom ({!N-ob η $ S-ob x!}) {!!} + -- N-hom (_⊣_.η L/b⊣R/b) = {!!} + -- N-ob (_⊣_.ε L/b⊣R/b) x = + -- slicehom (F-hom L ((pbPr₁ ((Pbs + -- (cospan c (F-ob R (F-ob L c)) (F-ob R (S-ob x)) (N-ob η c) + -- (F-hom R (S-arr x))))))) 𝑫.⋆ + -- {!S-arr x !}) {!!} + -- N-hom (_⊣_.ε L/b⊣R/b) = {!!} + -- _⊣_.triangleIdentities L/b⊣R/b = {!!} + -- -- N-ob (_⊣_.η L/b⊣R/b) = {!!} + -- -- N-hom (_⊣_.η L/b⊣R/b) = {!!} + -- -- _⊣_.ε L/b⊣R/b = {!!} + -- -- _⊣_.triangleIdentities L/b⊣R/b = {!!} diff --git a/Cubical/Categories/Constructions/Slice/Properties.agda b/Cubical/Categories/Constructions/Slice/Properties.agda index 747bc1ec3c..9956afc770 100644 --- a/Cubical/Categories/Constructions/Slice/Properties.agda +++ b/Cubical/Categories/Constructions/Slice/Properties.agda @@ -2,14 +2,16 @@ open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels - +open import Cubical.Foundations.Structure open import Cubical.Data.Sigma open import Cubical.HITs.PropositionalTruncation using (∣_∣₁) open import Cubical.Categories.Category +open import Cubical.Categories.Category.Properties open import Cubical.Categories.Constructions.Slice.Base import Cubical.Categories.Constructions.Elements as Elements +open import Cubical.Categories.Limits.Pullback open import Cubical.Categories.Equivalence open import Cubical.Categories.Functor open import Cubical.Categories.Instances.Sets diff --git a/Cubical/Categories/Equivalence/WeakEquivalence.agda b/Cubical/Categories/Equivalence/WeakEquivalence.agda index 45707f5b18..9f4f297d6b 100644 --- a/Cubical/Categories/Equivalence/WeakEquivalence.agda +++ b/Cubical/Categories/Equivalence/WeakEquivalence.agda @@ -3,7 +3,7 @@ Weak Equivalence between Categories -} -{-# OPTIONS --safe --lossy-unification #-} +{-# OPTIONS --safe --lossy-unification #-} module Cubical.Categories.Equivalence.WeakEquivalence where @@ -161,6 +161,29 @@ module _ fun IsoCategoryPath = WeakEquivlance→CategoryPath ∘f isWeakEquiv inv IsoCategoryPath = ≡→WeakEquivlance ∘f mk≡ rightInv IsoCategoryPath b = CategoryPath≡ + {C = C} {C' = C'} {_} + -- {categoryPath {C = C} {C' = C'} + -- (λ i → + -- Glue (C' .Category.ob) {φ = i ∨ ~ i} + -- (λ ._ → ob≡ b i , equivPathP {e = ob≃ ((≡→WeakEquivlance (mk≡ b)) .isWeakEquiv)} + -- {f = idEquiv _} (transport-fillerExt⁻ (ob≡ b)) i)) + -- (λ j x y → + -- Glue 𝑪'.Hom[ unglue (~ j ∨ j) x , unglue (~ j ∨ j ∨ i0) y ] + -- (λ { (j = i0) + -- → 𝑪.Hom[ x , y ] , + -- Hom≃ (isWeakEquivalenceTransportFunctor (mk≡ b)) x y + -- ; (j = i1) + -- → 𝑪'.Hom[ unglue (~ i1 ∨ i1 ∨ i0) x , unglue (~ i1 ∨ i1 ∨ i0) y ] , + -- idEquiv + -- 𝑪'.Hom[ unglue (~ i1 ∨ i1 ∨ i0) x , unglue (~ i1 ∨ i1 ∨ i0) y ] + -- })) + -- (id≡ + -- (WeakEquivlance→CategoryPath + -- (isWeakEquiv (inv IsoCategoryPath b)))) + -- (⋆≡ + -- (WeakEquivlance→CategoryPath + -- (isWeakEquiv (inv IsoCategoryPath b))))} + {b} (λ i j → Glue _ {φ = ~ j ∨ j ∨ i} (λ _ → _ , equivPathP diff --git a/Cubical/Categories/Instances/Setoids.agda b/Cubical/Categories/Instances/Setoids.agda index 265608b3c8..4942e1897e 100644 --- a/Cubical/Categories/Instances/Setoids.agda +++ b/Cubical/Categories/Instances/Setoids.agda @@ -3,6 +3,7 @@ module Cubical.Categories.Instances.Setoids where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Structure open import Cubical.Foundations.HLevels open import Cubical.Foundations.Equiv open import Cubical.Foundations.Equiv.Properties @@ -10,11 +11,16 @@ open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Univalence open import Cubical.Foundations.Transport hiding (pathToIso) open import Cubical.Foundations.Function +open import Cubical.Foundations.Path open import Cubical.Functions.FunExtEquiv open import Cubical.Functions.Logic hiding (_⇒_) open import Cubical.Data.Unit +open import Cubical.Data.Maybe open import Cubical.Data.Sigma +open import Cubical.Data.Bool +open import Cubical.Data.Empty as ⊥ open import Cubical.Categories.Category +open import Cubical.Categories.Monoidal.Enriched open import Cubical.Categories.Morphism open import Cubical.Categories.Functor open import Cubical.Categories.NaturalTransformation @@ -23,11 +29,17 @@ open import Cubical.Categories.Adjoint open import Cubical.Categories.Functors.HomFunctor open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Constructions.BinProduct +open import Cubical.Categories.Constructions.Slice open import Cubical.Categories.Constructions.FullSubcategory open import Cubical.Categories.Instances.Functors open import Cubical.Relation.Binary +open import Cubical.Relation.Nullary open import Cubical.Relation.Binary.Setoid +open import Cubical.Categories.Monoidal + +open import Cubical.Categories.Limits.Pullback + open import Cubical.HITs.SetQuotients as / open import Cubical.HITs.PropositionalTruncation @@ -35,6 +47,86 @@ open Category hiding (_∘_) open Functor + +SETPullback : ∀ ℓ → Pullbacks (SET ℓ) +SETPullback ℓ (cospan l m r s₁ s₂) = w + where + open Pullback + w : Pullback (SET ℓ) (cospan l m r s₁ s₂) + pbOb w = _ , isSetΣ (isSet× (snd l) (snd r)) + (uncurry λ x y → isOfHLevelPath 2 (snd m) (s₁ x) (s₂ y)) + pbPr₁ w = fst ∘ fst + pbPr₂ w = snd ∘ fst + pbCommutes w = funExt snd + fst (fst (univProp w h k H')) d = _ , (H' ≡$ d) + snd (fst (univProp w h k H')) = refl , refl + snd (univProp w h k H') y = + Σ≡Prop + (λ _ → isProp× (isSet→ (snd l) _ _) (isSet→ (snd r) _ _)) + (funExt λ x → Σ≡Prop (λ _ → (snd m) _ _) + λ i → fst (snd y) i x , snd (snd y) i x) + +module SetLCCC ℓ {X@(_ , isSetX) Y@(_ , isSetY) : hSet ℓ} (f : ⟨ X ⟩ → ⟨ Y ⟩) where + open BaseChangeFunctor (SET ℓ) X (SETPullback ℓ) {Y} f + + open Cubical.Categories.Adjoint.NaturalBijection + open _⊣_ + + open import Cubical.Categories.Instances.Cospan + open import Cubical.Categories.Limits.Limits + + Π/ : Functor (SliceCat (SET ℓ) X) (SliceCat (SET ℓ) Y) + F-ob Π/ (sliceob {S-ob = _ , isSetA} h) = + sliceob {S-ob = _ , (isSetΣ isSetY $ + λ y → isSetΠ λ ((x , _) : fiber f y) → + isOfHLevelFiber 2 isSetA isSetX h x)} fst + F-hom Π/ {a} {b} (slicehom g p) = + slicehom (map-snd (map-sndDep (λ q → (p ≡$ _) ∙ q ) ∘_)) refl + F-id Π/ = SliceHom-≡-intro' _ _ $ + funExt λ x' → cong ((fst x') ,_) + (funExt λ y → Σ≡Prop (λ _ → isSetX _ _) refl) + F-seq Π/ _ _ = SliceHom-≡-intro' _ _ $ + funExt λ x' → cong ((fst x') ,_) + (funExt λ y → Σ≡Prop (λ _ → isSetX _ _) refl) + + f*⊣Π/ : BaseChangeFunctor ⊣ Π/ + Iso.fun (adjIso f*⊣Π/) (slicehom h p) = + slicehom (λ _ → _ , λ (_ , q) → h (_ , q) , (p ≡$ _)) refl + Iso.inv (adjIso f*⊣Π/) (slicehom h p) = + slicehom _ $ funExt λ (_ , q) → snd (snd (h _) (_ , q ∙ ((sym p) ≡$ _))) + Iso.rightInv (adjIso f*⊣Π/) b = SliceHom-≡-intro' _ _ $ + funExt λ _ → cong₂ _,_ (sym (S-comm b ≡$ _)) + $ toPathP $ funExt λ _ → + Σ≡Prop (λ _ → isSetX _ _) $ transportRefl _ ∙ + cong (fst ∘ snd (S-hom b _)) + (Σ≡Prop (λ _ → isSetY _ _) $ transportRefl _) + Iso.leftInv (adjIso f*⊣Π/) a = SliceHom-≡-intro' _ _ $ + funExt λ _ → cong (S-hom a) $ Σ≡Prop (λ _ → isSetY _ _) refl + adjNatInD f*⊣Π/ _ _ = SliceHom-≡-intro' _ _ $ + funExt λ _ → cong₂ _,_ refl $ + funExt λ _ → Σ≡Prop (λ _ → isSetX _ _) refl + adjNatInC f*⊣Π/ g h = SliceHom-≡-intro' _ _ $ + funExt λ _ → cong (fst ∘ (snd (S-hom g (S-hom h _)) ∘ (_ ,_))) $ isSetY _ _ _ _ + + Σ/ : Functor (SliceCat (SET ℓ) X) (SliceCat (SET ℓ) Y) + F-ob Σ/ (sliceob {S-ob = ob} arr) = sliceob {S-ob = ob} (f ∘ arr ) + F-hom Σ/ (slicehom g p) = slicehom _ (cong (f ∘_) p) + F-id Σ/ = refl + F-seq Σ/ _ _ = SliceHom-≡-intro' _ _ $ refl + + Σ/⊣f* : Σ/ ⊣ BaseChangeFunctor + Iso.fun (adjIso Σ/⊣f*) (slicehom g p) = slicehom (λ _ → _ , (sym p ≡$ _ )) refl + Iso.inv (adjIso Σ/⊣f*) (slicehom g p) = slicehom (snd ∘ fst ∘ g) $ + funExt (λ x → sym (snd (g x))) ∙ cong (f ∘_) p + Iso.rightInv (adjIso Σ/⊣f*) (slicehom g p) = + SliceHom-≡-intro' _ _ $ + funExt λ xx → Σ≡Prop (λ _ → isSetY _ _) + (ΣPathP (sym (p ≡$ _) , refl)) + Iso.leftInv (adjIso Σ/⊣f*) _ = SliceHom-≡-intro' _ _ $ refl + adjNatInD Σ/⊣f* _ _ = SliceHom-≡-intro' _ _ $ + funExt λ x → Σ≡Prop (λ _ → isSetY _ _) refl + adjNatInC Σ/⊣f* _ _ = SliceHom-≡-intro' _ _ $ refl + module _ ℓ where SETOID : Category (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ)) (ℓ-max ℓ ℓ) ob SETOID = Setoid ℓ ℓ @@ -194,16 +286,113 @@ module _ ℓ where F-seq InternalHomFunctor _ _ = refl -^_ : ∀ X → Functor SETOID SETOID - -^_ X = (λF SETOID _ (SETOID ^op) InternalHomFunctor ⟅ X ⟆) + -^_ X = λF SETOID _ (SETOID ^op) InternalHomFunctor ⟅ X ⟆ -⊗_ : ∀ X → Functor SETOID SETOID - -⊗_ X = (λF SETOID _ (SETOID) (-⊗- ∘F fst (Swap SETOID SETOID)) ⟅ X ⟆) + -⊗_ X = λF SETOID _ (SETOID) (-⊗- ∘F fst (Swap SETOID SETOID)) ⟅ X ⟆ ⊗⊣^ : ∀ X → (-⊗ X) ⊣ (-^ X) adjIso (⊗⊣^ X) {A} {B} = setoidCurryIso X A B adjNatInD (⊗⊣^ X) {A} {d' = C} _ _ = SetoidMor≡ A (X ⟶ C) refl adjNatInC (⊗⊣^ X) {A} {d = C} _ _ = SetoidMor≡ (A ⊗ X) C refl + -- SetoidsMonoidalStr : StrictMonStr SETOID + -- TensorStr.─⊗─ (StrictMonStr.tenstr SetoidsMonoidalStr) = -⊗- + -- TensorStr.unit (StrictMonStr.tenstr SetoidsMonoidalStr) = setoidUnit + -- StrictMonStr.assoc SetoidsMonoidalStr _ _ _ = + -- Setoid≡ _ _ (invEquiv Σ-assoc-≃) λ _ _ → invEquiv Σ-assoc-≃ + -- StrictMonStr.idl SetoidsMonoidalStr _ = + -- Setoid≡ _ _ (isoToEquiv lUnit*×Iso) λ _ _ → isoToEquiv lUnit*×Iso + -- StrictMonStr.idr SetoidsMonoidalStr _ = + -- Setoid≡ _ _ (isoToEquiv rUnit*×Iso) λ _ _ → isoToEquiv rUnit*×Iso + + SetoidsMonoidalStrα : + -⊗- ∘F (𝟙⟨ SETOID ⟩ ×F -⊗-) ≅ᶜ + -⊗- ∘F (-⊗- ×F 𝟙⟨ SETOID ⟩) ∘F ×C-assoc SETOID SETOID SETOID + NatTrans.N-ob (NatIso.trans SetoidsMonoidalStrα) _ = + invEq Σ-assoc-≃ , invEq Σ-assoc-≃ + NatTrans.N-hom (NatIso.trans SetoidsMonoidalStrα) {x} {y} _ = + SetoidMor≡ + (F-ob (-⊗- ∘F (𝟙⟨ SETOID ⟩ ×F -⊗-)) x) + ((-⊗- ∘F (-⊗- ×F 𝟙⟨ SETOID ⟩) ∘F ×C-assoc SETOID SETOID SETOID) + .F-ob y) + refl + isIso.inv (NatIso.nIso SetoidsMonoidalStrα _) = + fst Σ-assoc-≃ , fst Σ-assoc-≃ + isIso.sec (NatIso.nIso SetoidsMonoidalStrα x) = refl + isIso.ret (NatIso.nIso SetoidsMonoidalStrα x) = refl + + SetoidsMonoidalStrη : -⊗- ∘F rinj SETOID SETOID setoidUnit ≅ᶜ 𝟙⟨ SETOID ⟩ + NatIso.trans SetoidsMonoidalStrη = + natTrans (λ _ → Iso.fun lUnit*×Iso , Iso.fun lUnit*×Iso) + λ {x} {y} _ → + SetoidMor≡ (F-ob (-⊗- ∘F rinj SETOID SETOID setoidUnit) x) y refl + NatIso.nIso SetoidsMonoidalStrη x = + isiso (Iso.inv lUnit*×Iso , Iso.inv lUnit*×Iso) refl refl + + SetoidsMonoidalStrρ : -⊗- ∘F linj SETOID SETOID setoidUnit ≅ᶜ 𝟙⟨ SETOID ⟩ + NatIso.trans SetoidsMonoidalStrρ = + natTrans (λ _ → Iso.fun rUnit*×Iso , Iso.fun rUnit*×Iso) + λ {x} {y} _ → + SetoidMor≡ (F-ob (-⊗- ∘F linj SETOID SETOID setoidUnit) x) y refl + NatIso.nIso SetoidsMonoidalStrρ x = + isiso (Iso.inv rUnit*×Iso , Iso.inv rUnit*×Iso) refl refl + + + SetoidsMonoidalStr : MonoidalStr SETOID + TensorStr.─⊗─ (MonoidalStr.tenstr SetoidsMonoidalStr) = -⊗- + TensorStr.unit (MonoidalStr.tenstr SetoidsMonoidalStr) = setoidUnit + MonoidalStr.α SetoidsMonoidalStr = SetoidsMonoidalStrα + MonoidalStr.η SetoidsMonoidalStr = SetoidsMonoidalStrη + MonoidalStr.ρ SetoidsMonoidalStr = SetoidsMonoidalStrρ + MonoidalStr.pentagon SetoidsMonoidalStr w x y z = refl + MonoidalStr.triangle SetoidsMonoidalStr x y = refl + + E-Category = + EnrichedCategory (record { C = _ ; monstr = SetoidsMonoidalStr }) + + E-SETOIDS : E-Category (ℓ-suc ℓ) + EnrichedCategory.ob E-SETOIDS = Setoid ℓ ℓ + EnrichedCategory.Hom[_,_] E-SETOIDS = _⟶_ + EnrichedCategory.id E-SETOIDS {x} = + (λ _ → id SETOID {x}) , + λ _ _ → BinaryRelation.isEquivRel.reflexive (snd (snd x)) _ + EnrichedCategory.seq E-SETOIDS x y z = + uncurry (_⋆_ SETOID {x} {y} {z}) , + λ {(f , g)} {(f' , g')} (fr , gr) a → + transitive' (gr (fst f a)) (snd g' (fr a)) + where open BinaryRelation.isEquivRel (snd (snd z)) + EnrichedCategory.⋆IdL E-SETOIDS x y = + SetoidMor≡ (setoidUnit ⊗ (x ⟶ y)) (x ⟶ y) refl + EnrichedCategory.⋆IdR E-SETOIDS x y = + SetoidMor≡ ((x ⟶ y) ⊗ setoidUnit) (x ⟶ y) refl + EnrichedCategory.⋆Assoc E-SETOIDS x y z w = + SetoidMor≡ ((x ⟶ y) ⊗ ( (y ⟶ z) ⊗ (z ⟶ w))) (x ⟶ w) refl + + + + pullbacks : Pullbacks SETOID + pullbacks cspn = w + where + open Cospan cspn + open Pullback + w : Pullback (SETOID) cspn + pbOb w = PullbackSetoid l r m s₁ s₂ + pbPr₁ w = fst ∘ fst , fst + pbPr₂ w = snd ∘ fst , snd + pbCommutes w = SetoidMor≡ (PullbackSetoid l r m s₁ s₂) m (funExt snd) + fst (fst (univProp w h k H')) = (λ x → (fst h x , fst k x) , + (cong fst H' ≡$ x)) , + λ {a} {b} x → (snd h x) , (snd k x) + snd (fst (univProp w {d} h k H')) = SetoidMor≡ d l refl , SetoidMor≡ d r refl + snd (univProp w {d} h k H') y = Σ≡Prop + (λ _ → isProp× (isSetHom (SETOID) {d} {l} _ _) + (isSetHom (SETOID) {d} {r} _ _)) + (SetoidMor≡ d (PullbackSetoid l r m s₁ s₂) + (funExt λ x → Σ≡Prop (λ _ → snd (fst m) _ _) + (cong₂ _,_ (λ i → fst (fst (snd y) i) x) + (λ i → fst (snd (snd y) i) x)))) + open WeakEquivalence open isWeakEquivalence @@ -239,3 +428,405 @@ module _ ℓ where esssurj (isWeakEquiv IdRelationsSubcategory≅SET) d = ∣ (IdRel ⟅ d ⟆ , idfun _) , idCatIso ∣₁ + + +-- -- -- -- pullbacks : Pullbacks SETOID +-- -- -- -- pullbacks cspn = w +-- -- -- -- where +-- -- -- -- open Cospan cspn +-- -- -- -- open Pullback +-- -- -- -- w : Pullback (SETOID) cspn +-- -- -- -- pbOb w = PullbackSetoid l r m s₁ s₂ +-- -- -- -- pbPr₁ w = fst ∘ fst , fst ∘ fst +-- -- -- -- pbPr₂ w = snd ∘ fst , snd ∘ fst +-- -- -- -- pbCommutes w = SetoidMor≡ (PullbackSetoid l r m s₁ s₂) m (funExt snd) +-- -- -- -- fst (fst (univProp w h k H')) = (λ x → (fst h x , fst k x) , +-- -- -- -- (cong fst H' ≡$ x)) , +-- -- -- -- λ {a} {b} x → ((snd h x) , (snd k x)) , snd s₁ ((snd h x)) +-- -- -- -- snd (fst (univProp w {d} h k H')) = SetoidMor≡ d l refl , SetoidMor≡ d r refl +-- -- -- -- snd (univProp w {d} h k H') y = Σ≡Prop +-- -- -- -- (λ _ → isProp× (isSetHom (SETOID) {d} {l} _ _) +-- -- -- -- (isSetHom (SETOID) {d} {r} _ _)) +-- -- -- -- (SetoidMor≡ d (PullbackSetoid l r m s₁ s₂) +-- -- -- -- (funExt λ x → Σ≡Prop (λ _ → snd (fst m) _ _) +-- -- -- -- (cong₂ _,_ (λ i → fst (fst (snd y) i) x) +-- -- -- -- (λ i → fst (snd (snd y) i) x)))) + + + module _ {X Y : ob SETOID} (f : SetoidMor X Y) where + open BaseChangeFunctor SETOID X pullbacks {Y} f public + + SΣ : ∀ {X} → (x : SliceOb SETOID X) → _ + SΣ {X} = λ x → SetoidΣ (S-ob x) X (S-arr x) + + SΠ : ∀ {X} → (x : SliceOb SETOID X) → _ + SΠ {X} = λ x → setoidSection (S-ob x) X (S-arr x) + + SETOIDΣ : Functor (SliceCat SETOID X) (SliceCat SETOID Y) + S-ob (F-ob SETOIDΣ x) = SΣ x + S-arr (F-ob SETOIDΣ x) = SETOID ._⋆_ {SΣ x} {X} {Y} + (setoidΣ-pr₁ (S-ob x) X (S-arr x)) f + fst (S-hom (F-hom SETOIDΣ x)) = fst (S-hom x) + snd (S-hom (F-hom SETOIDΣ x)) x₁ = + snd (S-hom x) (fst x₁) , subst2 (fst (fst (snd X))) + (cong fst (sym (S-comm x)) ≡$ _) + (cong fst (sym (S-comm x)) ≡$ _) (snd x₁) + S-comm (F-hom SETOIDΣ {x} {y} g) = + SetoidMor≡ (SΣ x) Y + (funExt λ u → cong (fst f) (cong fst (S-comm g) ≡$ u)) + F-id SETOIDΣ {x = x} = SliceHom-≡-intro' _ _ + (SetoidMor≡ (SΣ x) (SΣ x) refl) + F-seq SETOIDΣ {x = x} {_} {z} _ _ = SliceHom-≡-intro' _ _ + (SetoidMor≡ (SΣ x) (SΣ z) refl) + + SetoidΣ⊣BaseChange : SETOIDΣ ⊣ BaseChangeFunctor + fst (S-hom (fun (adjIso SetoidΣ⊣BaseChange {c}) h)) x = + (fst (S-arr c) x , fst (S-hom h) x ) , sym (cong fst (S-comm h) ≡$ x) + snd (S-hom (fun (adjIso SetoidΣ⊣BaseChange {c}) h)) g = + ((snd (S-arr c) g) , snd (S-hom h) (g , snd (S-arr c) g)) + S-comm (fun (adjIso SetoidΣ⊣BaseChange {c} ) _) = SetoidMor≡ (S-ob c) X refl + fst (S-hom (inv (adjIso SetoidΣ⊣BaseChange) h)) x = + snd (fst (fst (S-hom h) x)) + snd (S-hom (inv (adjIso SetoidΣ⊣BaseChange) x)) {c} {d} (r , r') = + snd (snd (S-hom x) r) + S-comm (inv (adjIso SetoidΣ⊣BaseChange {c} {d}) (slicehom (x , _) y)) = + SetoidMor≡ (SΣ c) Y + (sym (funExt (snd ∘ x)) ∙ congS ((fst f ∘_) ∘ fst) y) + rightInv (adjIso SetoidΣ⊣BaseChange {c} {d}) b = SliceHom-≡-intro' _ _ + (SetoidMor≡ (S-ob c) (S-ob (BaseChangeFunctor ⟅ d ⟆)) + (funExt λ x → Σ≡Prop (λ _ → snd (fst Y) _ _) + (cong (_, _) (sym (cong fst (S-comm b) ≡$ x))))) + leftInv (adjIso SetoidΣ⊣BaseChange {c} {d}) a = SliceHom-≡-intro' _ _ + (SetoidMor≡ ((S-ob (SETOIDΣ ⟅ c ⟆))) (S-ob d) refl) + adjNatInD SetoidΣ⊣BaseChange {c} {_} {d'} _ _ = SliceHom-≡-intro' _ _ + (SetoidMor≡ (S-ob c) (S-ob (BaseChangeFunctor ⟅ d' ⟆)) + (funExt λ _ → Σ≡Prop (λ _ → snd (fst Y) _ _) refl)) + adjNatInC SetoidΣ⊣BaseChange _ _ = SliceHom-≡-intro' _ _ refl + + + ¬BaseChange⊣SetoidΠ : ({X Y : ob SETOID} (f : SetoidMor X Y) → + Σ _ (BaseChangeFunctor {X} {Y} f ⊣_)) → ⊥.⊥ + ¬BaseChange⊣SetoidΠ isLCCC = Πob-full-rel Πob-full + + where + + 𝕀 : Setoid ℓ ℓ + 𝕀 = (Lift Bool , isOfHLevelLift 2 isSetBool) , fullEquivPropRel + + 𝟚 : Setoid ℓ ℓ + 𝟚 = (Lift Bool , isOfHLevelLift 2 isSetBool) , + ((_ , isOfHLevelLift 2 isSetBool) , isEquivRelIdRel) + + 𝑨 : SetoidMor (setoidUnit {ℓ} {ℓ}) 𝕀 + 𝑨 = (λ _ → lift true) , λ _ → _ + + 𝟚/ = sliceob {S-ob = 𝟚} ((λ _ → tt*) , λ {x} {x'} _ → tt*) + + + open Σ (isLCCC {(setoidUnit {ℓ} {ℓ})} {𝕀} 𝑨) renaming (fst to ΠA ; snd to Π⊣A*) + open _⊣_ Π⊣A* renaming (adjIso to aIso) + + module lem2 where + G = sliceob {S-ob = setoidUnit} ((λ x → lift false) , _) + + bcf = BaseChangeFunctor {(setoidUnit {ℓ} {ℓ})} {𝕀} 𝑨 ⟅ G ⟆ + + isPropFiberFalse : isProp (fiber (fst (S-arr (ΠA ⟅ 𝟚/ ⟆))) (lift false)) + isPropFiberFalse (x , p) (y , q) = + Σ≡Prop (λ _ _ _ → cong (cong lift) (isSetBool _ _ _ _)) + ((cong (fst ∘ S-hom) (isoInvInjective (aIso {G} {𝟚/}) + (slicehom + ((λ _ → x) , λ _ → BinaryRelation.isEquivRel.reflexive (snd (snd + (S-ob (F-ob ΠA 𝟚/)))) _) + ( SetoidMor≡ (S-ob G) 𝕀 (funExt λ _ → p))) + ((slicehom + ((λ _ → y) , λ _ → BinaryRelation.isEquivRel.reflexive (snd (snd + (S-ob (F-ob ΠA 𝟚/)))) _) + ( SetoidMor≡ (S-ob G) 𝕀 (funExt λ _ → q)))) + (SliceHom-≡-intro' _ _ + (SetoidMor≡ (bcf .S-ob) (𝟚/ .S-ob) + (funExt λ z → ⊥.rec (true≢false (cong lower (snd z))) + ))))) ≡$ _ ) + + + module lem3 where + G = sliceob {S-ob = 𝕀} (SETOID .id {𝕀}) + + aL : Iso + (fst (fst (S-ob 𝟚/))) + (SliceHom SETOID setoidUnit (BaseChangeFunctor 𝑨 ⟅ G ⟆) 𝟚/) + + fun aL h = + slicehom ((λ _ → h) + , λ _ → BinaryRelation.isEquivRel.reflexive (snd (snd + (S-ob 𝟚/))) _) refl + inv aL (slicehom (f , _) _) = f (_ , refl) + rightInv aL b = + SliceHom-≡-intro' _ _ + (SetoidMor≡ + ((BaseChangeFunctor {X = (setoidUnit {ℓ} {ℓ})} {𝕀} 𝑨 ⟅ G ⟆) .S-ob) + (𝟚/ .S-ob) (funExt λ x' → + cong (λ (x , y) → fst (S-hom b) ((tt* , x) , y)) + (isPropSingl _ _))) + leftInv aL _ = refl + + lem3 : Iso (fst (fst (S-ob 𝟚/))) (SliceHom SETOID 𝕀 G (ΠA ⟅ 𝟚/ ⟆)) + lem3 = compIso aL (aIso {G} {𝟚/}) + + + + module zzz3 = Iso (compIso LiftIso (lem3.lem3)) + + + open BinaryRelation.isEquivRel (snd (snd (S-ob (ΠA ⟅ 𝟚/ ⟆)))) + + + piPt : Bool → fiber + (fst + (S-arr + (ΠA ⟅ 𝟚/ ⟆))) (lift true) + piPt b = (fst (S-hom (zzz3.fun b)) (lift true)) , + (cong fst (S-comm (zzz3.fun b)) ≡$ lift true) + + + + finLLem : fst (piPt true) ≡ fst (piPt false) + → ⊥.⊥ + finLLem p = + true≢false (isoFunInjective (compIso LiftIso (lem3.lem3)) _ _ + $ SliceHom-≡-intro' _ _ + $ SetoidMor≡ + ((lem3.G) .S-ob) + ((ΠA ⟅ 𝟚/ ⟆) .S-ob) + (funExt ( + λ where (lift false) → (congS fst (lem2.isPropFiberFalse + (_ , ((cong fst (S-comm (fun (lem3.lem3) (lift true))) ≡$ lift false))) + (_ , (cong fst (S-comm (fun (lem3.lem3) (lift false))) ≡$ lift false)))) + (lift true) → p))) + + + Πob-full : fst (fst (snd (S-ob (ΠA ⟅ 𝟚/ ⟆)))) + (fst (piPt false)) + (fst (piPt true)) + + Πob-full = + ((transitive' ((snd (S-hom (zzz3.fun false)) {lift true} {lift false} _)) + (transitive' + ((BinaryRelation.isRefl→impliedByIdentity + (fst (fst (snd (S-ob (ΠA ⟅ 𝟚/ ⟆))))) reflexive + (congS fst (lem2.isPropFiberFalse + (_ , ((cong fst (S-comm (fun (lem3.lem3) (lift false))) ≡$ lift false))) + (_ , (cong fst (S-comm (fun (lem3.lem3) (lift true))) ≡$ lift false)))) + )) + (snd (S-hom (zzz3.fun true)) {lift false} {lift true} _)))) + + Πob-full-rel : fst (fst (snd (S-ob (ΠA ⟅ 𝟚/ ⟆)))) + (fst (piPt false)) + (fst (piPt true)) + → ⊥.⊥ + Πob-full-rel rr = elim𝟚 Date: Sun, 21 Jan 2024 01:12:26 +0100 Subject: [PATCH 05/17] sliced adjoints --- Cubical/Categories/Adjoint.agda | 6 +- Cubical/Categories/Category/Properties.agda | 12 +- .../Categories/Constructions/Slice/Base.agda | 2 + .../Constructions/Slice/Functor.agda | 231 ++++++++++++------ Cubical/Categories/Instances/Functors.agda | 2 +- Cubical/Categories/Limits/Pullback.agda | 3 + 6 files changed, 178 insertions(+), 78 deletions(-) diff --git a/Cubical/Categories/Adjoint.agda b/Cubical/Categories/Adjoint.agda index fb0e4e4191..2f3ac8b99a 100644 --- a/Cubical/Categories/Adjoint.agda +++ b/Cubical/Categories/Adjoint.agda @@ -126,8 +126,8 @@ module AdjointUniqeUpToNatIso where open _⊣_ H⊣G using (η ; Δ₂) open _⊣_ H'⊣G using (ε ; Δ₁) by-N-homs = - AssocCong₂⋆R {C = D} _ - (AssocCong₂⋆L {C = D} (sym (N-hom ε _)) _) + AssocCong₂⋆R D + (AssocCong₂⋆L D (sym (N-hom ε _))) ∙ cong₂ _D⋆_ (sym (F-seq H' _ _) ∙∙ cong (H' ⟪_⟫) ((sym (N-hom η _))) @@ -156,7 +156,7 @@ module AdjointUniqeUpToNatIso where (sym (F-seq F _ _) ∙∙ cong (F ⟪_⟫) (N-hom (F'⊣G .η) _) ∙∙ (F-seq F _ _)) - ∙∙ AssocCong₂⋆R {C = D} _ (N-hom (F⊣G .ε) _) + ∙∙ AssocCong₂⋆R D (N-hom (F⊣G .ε) _) where open _⊣_ inv (nIso F≅ᶜF' _) = _ sec (nIso F≅ᶜF' _) = s F⊣G F'⊣G diff --git a/Cubical/Categories/Category/Properties.agda b/Cubical/Categories/Category/Properties.agda index 0040358578..e65d16e7f6 100644 --- a/Cubical/Categories/Category/Properties.agda +++ b/Cubical/Categories/Category/Properties.agda @@ -93,25 +93,27 @@ module _ {C : Category ℓ ℓ'} where rCatWhiskerP f' f g r = cong (λ v → v ⋆⟨ C ⟩ g) (sym (fromPathP r)) +module _ (C : Category ℓ ℓ') where + AssocCong₂⋆L : {x y' y z w : C .ob} → {f' : C [ x , y' ]} {f : C [ x , y ]} {g' : C [ y' , z ]} {g : C [ y , z ]} - → f ⋆⟨ C ⟩ g ≡ f' ⋆⟨ C ⟩ g' → (h : C [ z , w ]) + → f ⋆⟨ C ⟩ g ≡ f' ⋆⟨ C ⟩ g' → {h : C [ z , w ]} → f ⋆⟨ C ⟩ (g ⋆⟨ C ⟩ h) ≡ f' ⋆⟨ C ⟩ (g' ⋆⟨ C ⟩ h) - AssocCong₂⋆L p h = - sym (⋆Assoc C _ _ h) + AssocCong₂⋆L p {h} = + sym (⋆Assoc C _ _ _) ∙∙ (λ i → p i ⋆⟨ C ⟩ h) ∙∙ ⋆Assoc C _ _ h AssocCong₂⋆R : {x y z z' w : C .ob} → - (f : C [ x , y ]) + {f : C [ x , y ]} {g' : C [ y , z' ]} {g : C [ y , z ]} {h' : C [ z' , w ]} {h : C [ z , w ]} → g ⋆⟨ C ⟩ h ≡ g' ⋆⟨ C ⟩ h' → (f ⋆⟨ C ⟩ g) ⋆⟨ C ⟩ h ≡ (f ⋆⟨ C ⟩ g') ⋆⟨ C ⟩ h' - AssocCong₂⋆R f p = + AssocCong₂⋆R {f = f} p = ⋆Assoc C f _ _ ∙∙ (λ i → f ⋆⟨ C ⟩ p i) ∙∙ sym (⋆Assoc C _ _ _) diff --git a/Cubical/Categories/Constructions/Slice/Base.agda b/Cubical/Categories/Constructions/Slice/Base.agda index e2cfc8d81e..39c34d26cb 100644 --- a/Cubical/Categories/Constructions/Slice/Base.agda +++ b/Cubical/Categories/Constructions/Slice/Base.agda @@ -30,6 +30,8 @@ record SliceOb : TypeC where {S-ob} : C .ob S-arr : C [ S-ob , c ] +pattern sliceob' x y = sliceob {S-ob = x} y + open SliceOb public record SliceHom (a b : SliceOb) : Type ℓ' where diff --git a/Cubical/Categories/Constructions/Slice/Functor.agda b/Cubical/Categories/Constructions/Slice/Functor.agda index 2ebaf36db4..32051b384d 100644 --- a/Cubical/Categories/Constructions/Slice/Functor.agda +++ b/Cubical/Categories/Constructions/Slice/Functor.agda @@ -6,6 +6,7 @@ open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels open import Cubical.Foundations.Structure open import Cubical.Foundations.Function +open import Cubical.Foundations.Isomorphism open import Cubical.Data.Sigma open import Cubical.HITs.PropositionalTruncation using (∣_∣₁) @@ -31,99 +32,191 @@ private variable ℓ ℓ' : Level C D : Category ℓ ℓ' + c d : C .ob -F/ : ∀ c (F : Functor C D) → Functor (SliceCat C c) (SliceCat D (F ⟅ c ⟆)) -F-ob (F/ c F) = sliceob ∘ F-hom F ∘ S-arr -F-hom (F/ c F) h = slicehom _ - (sym ( F-seq F _ _) ∙ cong (F-hom F) (S-comm h)) -F-id (F/ c F) = SliceHom-≡-intro' _ _ (F-id F) -F-seq (F/ c F) _ _ = SliceHom-≡-intro' _ _ (F-seq F _ _) +infix 39 _F/_ +infix 40 _﹗ +_F/_ : ∀ (F : Functor C D) c → Functor (SliceCat C c) (SliceCat D (F ⟅ c ⟆)) +F-ob (F F/ c) = sliceob ∘ F-hom F ∘ S-arr +F-hom (F F/ c) h = slicehom _ + $ sym ( F-seq F _ _) ∙ cong (F-hom F) (S-comm h) +F-id (F F/ c) = SliceHom-≡-intro' _ _ $ F-id F +F-seq (F F/ c) _ _ = SliceHom-≡-intro' _ _ $ F-seq F _ _ -module _ (Pbs : Pullbacks C) (c : C .ob) where +_﹗ : ∀ {c d} f → Functor (SliceCat C c) (SliceCat C d) +F-ob (_﹗ {C = C} f) (sliceob x) = sliceob (_⋆_ C x f) +F-hom (_﹗ {C = C} f) (slicehom h p) = slicehom _ $ + sym (C .⋆Assoc _ _ _) ∙ cong (λ x → (_⋆_ C x f)) p +F-id (f ﹗) = SliceHom-≡-intro' _ _ refl +F-seq (f ﹗) _ _ = SliceHom-≡-intro' _ _ refl + +module Pullbacks (Pbs : Pullbacks C) where open Pullback - module _ {Y} (f : C [ c , Y ]) where + _⋆ᶜ_ = C ._⋆_ + + module BaseChange {c d} (𝑓 : C [ c , d ]) where - private module _ (x : SliceCat C Y .ob) where - pb = Pbs (cospan c Y _ f (x .S-arr)) + module _ {x : SliceCat C d .ob} where + pb = Pbs (cospan c d _ 𝑓 (x .S-arr)) - module _ {y : SliceCat C Y .ob} (h : (SliceCat C Y) [ y , x ]) where + module _ {y : SliceCat C d .ob} (h : (SliceCat C d) [ y , x ]) where pbU : _ - pbU = let pbx = Pbs (cospan c Y _ f (y .S-arr)) + pbU = let pbx = Pbs (cospan c d _ 𝑓 (y .S-arr)) in univProp pb (pbPr₁ pbx) (h .S-hom ∘⟨ C ⟩ pbPr₂ pbx) (pbCommutes pbx ∙∙ - cong (C ⋆ pbPr₂ (Pbs (cospan c Y (S-ob y) _ (y .S-arr)))) + cong (C ⋆ pbPr₂ (Pbs (cospan c d (S-ob y) _ (y .S-arr)))) (sym (h .S-comm)) ∙∙ sym (C .⋆Assoc _ _ _)) + infix 40 _＊ - PbFunctor : Functor (SliceCat C Y) (SliceCat C c) - F-ob PbFunctor x = sliceob (pbPr₁ (pb x)) - F-hom PbFunctor {x} {y} f = - let ((f' , (u , _)) , _) = pbU y f + _＊ : Functor (SliceCat C d) (SliceCat C c) + F-ob _＊ x = sliceob (pbPr₁ pb) + F-hom _＊ f = + let ((f' , (u , _)) , _) = pbU f in slicehom f' (sym u) + F-id _＊ = SliceHom-≡-intro' _ _ $ + univProp' pb (sym (C .⋆IdL _)) (C .⋆IdR _ ∙ sym (C .⋆IdL _)) - F-id PbFunctor = - SliceHom-≡-intro' _ _ (cong fst (pbU _ _ .snd - (_ , sym (C .⋆IdL _) , C .⋆IdR _ ∙ sym (C .⋆IdL _)))) - F-seq PbFunctor _ _ = - let (u₁ , v₁) = pbU _ _ .fst .snd - (u₂ , v₂) = pbU _ _ .fst .snd - in SliceHom-≡-intro' _ _ (cong fst (pbU _ _ .snd - (_ , u₂ ∙∙ cong (C ⋆ _) u₁ ∙∙ sym (C .⋆Assoc _ _ _) - , (sym (C .⋆Assoc _ _ _) ∙∙ cong (λ x → (C ⋆ x) _) v₂ ∙∙ - AssocCong₂⋆R {C = C} _ v₁)))) + F-seq _＊ _ _ = + let (u₁ , v₁) = pbU _ .fst .snd + (u₂ , v₂) = pbU _ .fst .snd + in SliceHom-≡-intro' _ _ $ univProp' pb + (u₂ ∙∙ cong (C ⋆ _) u₁ ∙∙ sym (C .⋆Assoc _ _ _)) + (sym (C .⋆Assoc _ _ _) ∙∙ cong (λ x → (C ⋆ x) _) v₂ ∙∙ + AssocCong₂⋆R C v₁) + open BaseChange using (_＊) + open NaturalBijection renaming (_⊣_ to _⊣₂_) + open Iso + open _⊣₂_ - open UnitCounit + + module _ (𝑓 : C [ c , d ]) where + + open BaseChange 𝑓 using (pb ; pbU) + 𝑓﹗⊣𝑓＊ : 𝑓 ﹗ ⊣₂ 𝑓 ＊ + fun (adjIso 𝑓﹗⊣𝑓＊) (slicehom h o) = + let ((_ , (p , _)) , _) = univProp pb _ _ (sym o) + in slicehom _ (sym p) + inv (adjIso 𝑓﹗⊣𝑓＊) (slicehom h o) = slicehom _ $ + AssocCong₂⋆R C (sym (pbCommutes pb)) ∙ cong (_⋆ᶜ 𝑓) o + rightInv (adjIso 𝑓﹗⊣𝑓＊) (slicehom h o) = + SliceHom-≡-intro' _ _ (univProp' pb (sym o) refl) + leftInv (adjIso 𝑓﹗⊣𝑓＊) (slicehom h o) = + let ((_ , (_ , q)) , _) = univProp pb _ _ _ + in SliceHom-≡-intro' _ _ (sym q) + adjNatInD 𝑓﹗⊣𝑓＊ f k = SliceHom-≡-intro' _ _ $ + let ((h' , (v' , u')) , _) = univProp pb _ _ _ + ((_ , (v'' , u'')) , _) = univProp pb _ _ _ + in univProp' pb (v' ∙∙ cong (h' ⋆ᶜ_) v'' ∙∙ sym (C .⋆Assoc _ _ _)) + (cong (_⋆ᶜ _) u' ∙ AssocCong₂⋆R C u'') + + adjNatInC 𝑓﹗⊣𝑓＊ g h = SliceHom-≡-intro' _ _ $ C .⋆Assoc _ _ _ + + + open UnitCounit + + module SlicedAdjoint {L : Functor C D} {R} (L⊣R : L ⊣ R) where --- -- L/b : Functor (SliceCat C c) (SliceCat D (L ⟅ c ⟆)) --- -- F-ob L/b (sliceob S-arr) = sliceob (F-hom L S-arr) --- -- F-hom L/b (slicehom S-hom S-comm) = --- -- slicehom _ (sym ( F-seq L _ _) ∙ cong (F-hom L) S-comm) --- -- F-id L/b = SliceHom-≡-intro' _ _ (F-id L) --- -- F-seq L/b _ _ = SliceHom-≡-intro' _ _ (F-seq L _ _) - - -- R' : Functor (SliceCat D (L ⟅ c ⟆)) (SliceCat C (funcComp R L .F-ob c)) - -- F-ob R' (sliceob S-arr) = sliceob (F-hom R S-arr) - -- F-hom R' (slicehom S-hom S-comm) = slicehom _ (sym ( F-seq R _ _) ∙ cong (F-hom R) S-comm) - -- F-id R' = SliceHom-≡-intro' _ _ (F-id R) - -- F-seq R' _ _ = SliceHom-≡-intro' _ _ (F-seq R _ _) - --- -- -- R/b : Functor (SliceCat D (L ⟅ c ⟆)) (SliceCat C c) --- -- -- R/b = BaseChangeFunctor.BaseChangeFunctor Pbs (N-ob (_⊣_.η L⊣R) c) --- -- -- ∘F R' module 𝑪 = Category C module 𝑫 = Category D + open _⊣_ L⊣R - F/⊣ : Functor (SliceCat D (L ⟅ c ⟆)) (SliceCat C c) - F/⊣ = PbFunctor (N-ob η c) ∘F F/ (L ⟅ c ⟆) R - - L/b⊣R/b : F/ c L ⊣ F/⊣ - N-ob (_⊣_.η L/b⊣R/b) x = - slicehom {!(N-ob η $ S-ob x)!} {!!} - N-hom (_⊣_.η L/b⊣R/b) = {!!} - N-ob (_⊣_.ε L/b⊣R/b) x = - slicehom ({!F-hom L ?!} 𝑫.⋆ (N-ob ε $ S-ob x)) {!!} - N-hom (_⊣_.ε L/b⊣R/b) = {!!} - _⊣_.triangleIdentities L/b⊣R/b = {!!} - -- N-ob (_⊣_.η L/b⊣R/b) x = - -- slicehom ({!N-ob η $ S-ob x!}) {!!} - -- N-hom (_⊣_.η L/b⊣R/b) = {!!} - -- N-ob (_⊣_.ε L/b⊣R/b) x = - -- slicehom (F-hom L ((pbPr₁ ((Pbs - -- (cospan c (F-ob R (F-ob L c)) (F-ob R (S-ob x)) (N-ob η c) - -- (F-hom R (S-arr x))))))) 𝑫.⋆ - -- {!S-arr x !}) {!!} - -- N-hom (_⊣_.ε L/b⊣R/b) = {!!} - -- _⊣_.triangleIdentities L/b⊣R/b = {!!} - -- -- N-ob (_⊣_.η L/b⊣R/b) = {!!} - -- -- N-hom (_⊣_.η L/b⊣R/b) = {!!} - -- -- _⊣_.ε L/b⊣R/b = {!!} - -- -- _⊣_.triangleIdentities L/b⊣R/b = {!!} + module _ {c} {d} where + module aI = Iso (adjIso (adj→adj' _ _ L⊣R) {c} {d}) + + module Left (b : D .ob) where + + ⊣F/ : Functor (SliceCat C (R ⟅ b ⟆)) (SliceCat D b) + ⊣F/ = N-ob ε b ﹗ ∘F L F/ (R ⟅ b ⟆) + + L/b⊣R/b : ⊣F/ ⊣₂ (R F/ b) + fun (adjIso L/b⊣R/b) (slicehom _ p) = + slicehom _ $ 𝑪.⋆Assoc _ _ _ + ∙∙ cong (_ 𝑪.⋆_) (sym (F-seq R _ _) ∙∙ cong (F-hom R) p ∙∙ F-seq R _ _) + ∙∙ (AssocCong₂⋆L C (sym (N-hom η _)) + ∙∙ cong (_ 𝑪.⋆_) (Δ₂ _) ∙∙ C .⋆IdR _) + + inv (adjIso L/b⊣R/b) (slicehom _ p) = + slicehom _ $ AssocCong₂⋆R D (sym (N-hom ε _)) + ∙ cong (𝑫._⋆ _) (sym (F-seq L _ _) ∙ cong (F-hom L) p) + rightInv (adjIso L/b⊣R/b) _ = SliceHom-≡-intro' _ _ $ aI.rightInv _ + leftInv (adjIso L/b⊣R/b) _ = SliceHom-≡-intro' _ _ $ aI.leftInv _ + adjNatInD L/b⊣R/b _ _ = SliceHom-≡-intro' _ _ $ + cong (_ 𝑪.⋆_) (F-seq R _ _) ∙ sym (C .⋆Assoc _ _ _) + adjNatInC L/b⊣R/b _ _ = SliceHom-≡-intro' _ _ $ + cong (𝑫._⋆ _) (F-seq L _ _) ∙ (D .⋆Assoc _ _ _) + + + module Right (b : C .ob) where + + F/⊣ : Functor (SliceCat D (L ⟅ b ⟆)) (SliceCat C b) + F/⊣ = (N-ob η b) ＊ ∘F R F/ (L ⟅ b ⟆) + + + + module _ {d} {p : 𝑫.Hom[ d , L ⟅ b ⟆ ]} where + module PB = Pullback (Pbs (cospan _ _ _ (N-ob η b) (F-hom R p))) + + L/b⊣R/b : L F/ b ⊣₂ F/⊣ + fun (adjIso L/b⊣R/b) (slicehom f s) = slicehom _ (sym (fst (snd (fst pbu')))) + where + + pbu' = PB.univProp _ _ + (N-hom η _ ∙∙ + cong (_ 𝑪.⋆_) (cong (F-hom R) (sym s) ∙ F-seq R _ _) + ∙∙ sym (𝑪.⋆Assoc _ _ _)) + inv (adjIso L/b⊣R/b) (slicehom f s) = slicehom _ + (𝑫.⋆Assoc _ _ _ + ∙∙ congS (𝑫._⋆ (N-ob ε _ 𝑫.⋆ _)) (F-seq L _ _) + ∙∙ 𝑫.⋆Assoc _ _ _ ∙ cong (F-hom L f 𝑫.⋆_) + (cong ((F-hom L (PB.pbPr₂)) 𝑫.⋆_) (sym (N-hom ε _)) + ∙∙ sym (𝑫.⋆Assoc _ _ _) + ∙∙ cong (𝑫._⋆ N-ob ε (F-ob L b)) + (sym (F-seq L _ _) + ∙∙ cong (F-hom L) (sym (PB.pbCommutes)) + ∙∙ F-seq L _ _) + ∙∙ 𝑫.⋆Assoc _ _ _ + ∙∙ cong (F-hom L (PB.pbPr₁) 𝑫.⋆_) (Δ₁ b) + ∙ 𝑫.⋆IdR _) + ∙∙ sym (F-seq L _ _) + ∙∙ cong (F-hom L) s) + + rightInv (adjIso L/b⊣R/b) h = SliceHom-≡-intro' _ _ $ + let p₂ : ∀ {x} → N-ob η _ 𝑪.⋆ F-hom R (F-hom L x 𝑫.⋆ N-ob ε _) ≡ x + p₂ = cong (_ 𝑪.⋆_) (F-seq R _ _) ∙ + AssocCong₂⋆L C (sym (N-hom η _)) + ∙∙ cong (_ 𝑪.⋆_) (Δ₂ _) ∙∙ 𝑪.⋆IdR _ + + + in PB.univProp' (sym (S-comm h)) p₂ + + leftInv (adjIso L/b⊣R/b) _ = SliceHom-≡-intro' _ _ $ + cong ((𝑫._⋆ _) ∘ F-hom L) + (sym (snd (snd (fst (PB.univProp _ _ _))))) + ∙ aI.leftInv _ + adjNatInD L/b⊣R/b _ _ = SliceHom-≡-intro' _ _ $ + let ee = _ + ((_ , (u , v)) , _) = PB.univProp _ _ _ + ((_ , (u' , v')) , _) = PB.univProp _ _ _ + + in PB.univProp' + (u ∙∙ cong (ee 𝑪.⋆_) u' ∙∙ sym (𝑪.⋆Assoc ee _ _)) + (cong (N-ob η _ 𝑪.⋆_) (F-seq R _ _) + ∙∙ sym (𝑪.⋆Assoc _ _ _) ∙∙ + (cong (𝑪._⋆ _) v ∙ AssocCong₂⋆R C v')) + + adjNatInC L/b⊣R/b _ _ = let w = _ in SliceHom-≡-intro' _ _ $ + cong (𝑫._⋆ _) (F-seq L _ w ∙∙ cong (𝑫._⋆ (F-hom L w)) (F-seq L _ _) ∙∙ + (𝑫.⋆Assoc _ _ _)) ∙∙ (𝑫.⋆Assoc _ _ _) + ∙∙ cong (_ 𝑫.⋆_) (cong (𝑫._⋆ _) (sym (F-seq L _ _))) + + diff --git a/Cubical/Categories/Instances/Functors.agda b/Cubical/Categories/Instances/Functors.agda index 0a220f92a0..0c4dea14ba 100644 --- a/Cubical/Categories/Instances/Functors.agda +++ b/Cubical/Categories/Instances/Functors.agda @@ -178,7 +178,7 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where F-seq (λF⁻ a) _ (eG , cG) = cong₂ (seq' D) (F-seq (F-ob a _) _ _) (cong (flip N-ob _) (F-seq a _ _)) - ∙ AssocCong₂⋆R {C = D} _ + ∙ AssocCong₂⋆R D (N-hom ((F-hom a _) ●ᵛ (F-hom a _)) _ ∙ (⋆Assoc D _ _ _) ∙ cong (seq' D _) (sym (N-hom (F-hom a eG) cG))) diff --git a/Cubical/Categories/Limits/Pullback.agda b/Cubical/Categories/Limits/Pullback.agda index a872212b80..287bce68c2 100644 --- a/Cubical/Categories/Limits/Pullback.agda +++ b/Cubical/Categories/Limits/Pullback.agda @@ -53,6 +53,9 @@ module _ (C : Category ℓ ℓ') where pbCommutes : pbPr₁ ⋆ cspn .s₁ ≡ pbPr₂ ⋆ cspn .s₂ univProp : isPullback cspn pbPr₁ pbPr₂ pbCommutes + univProp' : ∀ {c p₁ p₂ H g} p q → fst (fst (univProp {c} p₁ p₂ H)) ≡ g + univProp' p q = cong fst (snd (univProp _ _ _) (_ , (p , q))) + open Pullback pullbackArrow : From b79c4318a9b938792e8fb055003c34e00f6c5e58 Mon Sep 17 00:00:00 2001 From: Marcin Grzybowski Date: Tue, 23 Jan 2024 00:15:25 +0100 Subject: [PATCH 06/17] wip --- Cubical/Categories/Category/Base.agda | 29 +- .../Constructions/Slice/Functor.agda | 34 +- Cubical/Categories/Instances/Cat.agda | 80 ++ Cubical/Categories/Instances/Setoids.agda | 681 +++++++----------- Cubical/Foundations/Equiv/Properties.agda | 30 +- 5 files changed, 403 insertions(+), 451 deletions(-) create mode 100644 Cubical/Categories/Instances/Cat.agda diff --git a/Cubical/Categories/Category/Base.agda b/Cubical/Categories/Category/Base.agda index 7656b21a73..f3ca1d6850 100644 --- a/Cubical/Categories/Category/Base.agda +++ b/Cubical/Categories/Category/Base.agda @@ -9,7 +9,7 @@ open import Cubical.Data.Sigma private variable - ℓ ℓ' : Level + ℓ ℓ' ℓ'' : Level -- Categories with hom-sets record Category ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where @@ -140,8 +140,10 @@ _⋆_ (C ^op) f g = g ⋆⟨ C ⟩ f ⋆Assoc (C ^op) f g h = sym (C .⋆Assoc _ _ _) isSetHom (C ^op) = C .isSetHom -ΣPropCat : (C : Category ℓ ℓ') (P : ℙ (ob C)) → Category ℓ ℓ' -ob (ΣPropCat C P) = Σ[ x ∈ ob C ] x ∈ P + + +ΣPropCat : (C : Category ℓ ℓ') (P : ob C → hProp ℓ'') → Category (ℓ-max ℓ ℓ'') ℓ' +ob (ΣPropCat C P) = Σ[ x ∈ ob C ] (fst (P x)) Hom[_,_] (ΣPropCat C P) x y = C [ fst x , fst y ] id (ΣPropCat C P) = id C _⋆_ (ΣPropCat C P) = _⋆_ C @@ -150,10 +152,29 @@ _⋆_ (ΣPropCat C P) = _⋆_ C ⋆Assoc (ΣPropCat C P) = ⋆Assoc C isSetHom (ΣPropCat C P) = isSetHom C -isIsoΣPropCat : {C : Category ℓ ℓ'} {P : ℙ (ob C)} +isIsoΣPropCat : ∀ {C : Category ℓ ℓ'} {P} {x y : ob C} (p : x ∈ P) (q : y ∈ P) (f : C [ x , y ]) → isIso C f → isIso (ΣPropCat C P) {x , p} {y , q} f inv (isIsoΣPropCat p q f isIsoF) = isIsoF .inv sec (isIsoΣPropCat p q f isIsoF) = isIsoF .sec ret (isIsoΣPropCat p q f isIsoF) = isIsoF .ret + +ΣℙCat : (C : Category ℓ ℓ') (P : ℙ (ob C)) → Category ℓ ℓ' +ΣℙCat = ΣPropCat + +isSmall : (C : Category ℓ ℓ') → Type ℓ +isSmall C = isSet (C .ob) + +isThin : (C : Category ℓ ℓ') → Type (ℓ-max ℓ ℓ') +isThin C = ∀ x y → isProp (C [ x , y ]) + +isPropIsThin : (C : Category ℓ ℓ') → isProp (isThin C) +isPropIsThin C = isPropΠ2 λ _ _ → isPropIsProp + +isGroupoidCat : (C : Category ℓ ℓ') → Type (ℓ-max ℓ ℓ') +isGroupoidCat C = ∀ {x} {y} (f : C [ x , y ]) → isIso C f + +isPropIsGroupoidCat : (C : Category ℓ ℓ') → isProp (isGroupoidCat C) +isPropIsGroupoidCat C = + isPropImplicitΠ2 λ _ _ → isPropΠ isPropIsIso diff --git a/Cubical/Categories/Constructions/Slice/Functor.agda b/Cubical/Categories/Constructions/Slice/Functor.agda index 32051b384d..a28828d6fe 100644 --- a/Cubical/Categories/Constructions/Slice/Functor.agda +++ b/Cubical/Categories/Constructions/Slice/Functor.agda @@ -35,7 +35,7 @@ private c d : C .ob infix 39 _F/_ -infix 40 _﹗ +infix 40 Σ𝑓_ _F/_ : ∀ (F : Functor C D) c → Functor (SliceCat C c) (SliceCat D (F ⟅ c ⟆)) F-ob (F F/ c) = sliceob ∘ F-hom F ∘ S-arr @@ -44,20 +44,21 @@ F-hom (F F/ c) h = slicehom _ F-id (F F/ c) = SliceHom-≡-intro' _ _ $ F-id F F-seq (F F/ c) _ _ = SliceHom-≡-intro' _ _ $ F-seq F _ _ -_﹗ : ∀ {c d} f → Functor (SliceCat C c) (SliceCat C d) -F-ob (_﹗ {C = C} f) (sliceob x) = sliceob (_⋆_ C x f) -F-hom (_﹗ {C = C} f) (slicehom h p) = slicehom _ $ +Σ𝑓_ : ∀ {c d} f → Functor (SliceCat C c) (SliceCat C d) +F-ob (Σ𝑓_ {C = C} f) (sliceob x) = sliceob (_⋆_ C x f) +F-hom (Σ𝑓_ {C = C} f) (slicehom h p) = slicehom _ $ sym (C .⋆Assoc _ _ _) ∙ cong (λ x → (_⋆_ C x f)) p -F-id (f ﹗) = SliceHom-≡-intro' _ _ refl -F-seq (f ﹗) _ _ = SliceHom-≡-intro' _ _ refl +F-id (Σ𝑓 f) = SliceHom-≡-intro' _ _ refl +F-seq (Σ𝑓 f) _ _ = SliceHom-≡-intro' _ _ refl -module Pullbacks (Pbs : Pullbacks C) where +module _ (Pbs : Pullbacks C) where open Pullback _⋆ᶜ_ = C ._⋆_ module BaseChange {c d} (𝑓 : C [ c , d ]) where + infix 40 _＊ module _ {x : SliceCat C d .ob} where pb = Pbs (cospan c d _ 𝑓 (x .S-arr)) @@ -71,7 +72,6 @@ module Pullbacks (Pbs : Pullbacks C) where (pbCommutes pbx ∙∙ cong (C ⋆ pbPr₂ (Pbs (cospan c d (S-ob y) _ (y .S-arr)))) (sym (h .S-comm)) ∙∙ sym (C .⋆Assoc _ _ _)) - infix 40 _＊ _＊ : Functor (SliceCat C d) (SliceCat C c) F-ob _＊ x = sliceob (pbPr₁ pb) @@ -98,25 +98,25 @@ module Pullbacks (Pbs : Pullbacks C) where module _ (𝑓 : C [ c , d ]) where open BaseChange 𝑓 using (pb ; pbU) - - 𝑓﹗⊣𝑓＊ : 𝑓 ﹗ ⊣₂ 𝑓 ＊ - fun (adjIso 𝑓﹗⊣𝑓＊) (slicehom h o) = + + Σ𝑓⊣𝑓＊ : Σ𝑓 𝑓 ⊣₂ 𝑓 ＊ + fun (adjIso Σ𝑓⊣𝑓＊) (slicehom h o) = let ((_ , (p , _)) , _) = univProp pb _ _ (sym o) in slicehom _ (sym p) - inv (adjIso 𝑓﹗⊣𝑓＊) (slicehom h o) = slicehom _ $ + inv (adjIso Σ𝑓⊣𝑓＊) (slicehom h o) = slicehom _ $ AssocCong₂⋆R C (sym (pbCommutes pb)) ∙ cong (_⋆ᶜ 𝑓) o - rightInv (adjIso 𝑓﹗⊣𝑓＊) (slicehom h o) = + rightInv (adjIso Σ𝑓⊣𝑓＊) (slicehom h o) = SliceHom-≡-intro' _ _ (univProp' pb (sym o) refl) - leftInv (adjIso 𝑓﹗⊣𝑓＊) (slicehom h o) = + leftInv (adjIso Σ𝑓⊣𝑓＊) (slicehom h o) = let ((_ , (_ , q)) , _) = univProp pb _ _ _ in SliceHom-≡-intro' _ _ (sym q) - adjNatInD 𝑓﹗⊣𝑓＊ f k = SliceHom-≡-intro' _ _ $ + adjNatInD Σ𝑓⊣𝑓＊ f k = SliceHom-≡-intro' _ _ $ let ((h' , (v' , u')) , _) = univProp pb _ _ _ ((_ , (v'' , u'')) , _) = univProp pb _ _ _ in univProp' pb (v' ∙∙ cong (h' ⋆ᶜ_) v'' ∙∙ sym (C .⋆Assoc _ _ _)) (cong (_⋆ᶜ _) u' ∙ AssocCong₂⋆R C u'') - adjNatInC 𝑓﹗⊣𝑓＊ g h = SliceHom-≡-intro' _ _ $ C .⋆Assoc _ _ _ + adjNatInC Σ𝑓⊣𝑓＊ g h = SliceHom-≡-intro' _ _ $ C .⋆Assoc _ _ _ open UnitCounit @@ -136,7 +136,7 @@ module Pullbacks (Pbs : Pullbacks C) where module Left (b : D .ob) where ⊣F/ : Functor (SliceCat C (R ⟅ b ⟆)) (SliceCat D b) - ⊣F/ = N-ob ε b ﹗ ∘F L F/ (R ⟅ b ⟆) + ⊣F/ = Σ𝑓 N-ob ε b ∘F L F/ (R ⟅ b ⟆) L/b⊣R/b : ⊣F/ ⊣₂ (R F/ b) fun (adjIso L/b⊣R/b) (slicehom _ p) = diff --git a/Cubical/Categories/Instances/Cat.agda b/Cubical/Categories/Instances/Cat.agda new file mode 100644 index 0000000000..616f3f4129 --- /dev/null +++ b/Cubical/Categories/Instances/Cat.agda @@ -0,0 +1,80 @@ +-- The category of small categories +{-# OPTIONS --safe #-} + +module Cubical.Categories.Instances.Cat where + + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Equiv.Properties +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function +open import Cubical.Foundations.Univalence +open import Cubical.Data.Unit +open import Cubical.Data.Sigma +open import Cubical.Categories.Category +open import Cubical.Categories.Functor +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Equivalence.WeakEquivalence +open import Cubical.Categories.Category.Path +open import Cubical.Relation.Binary.Properties + +open import Cubical.Categories.Limits + +open Category hiding (_∘_) +open Functor + +module _ (ℓ ℓ' : Level) where + Cat : Category (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-max ℓ ℓ') + ob Cat = Σ (Category ℓ ℓ') isSmall + Hom[_,_] Cat X Y = Functor (fst X) (fst Y) + id Cat = 𝟙⟨ _ ⟩ + _⋆_ Cat G H = H ∘F G + ⋆IdL Cat _ = F-lUnit + ⋆IdR Cat _ = F-rUnit + ⋆Assoc Cat _ _ _ = F-assoc + isSetHom Cat {y = _ , isSetObY} = isSetFunctor isSetObY + + + -- isUnivalentCat : isUnivalent Cat + -- isUnivalent.univ isUnivalentCat (C , isSmallC) (C' , isSmallC') = + -- {!!} + + -- where + -- w : Iso (CategoryPath C C') (CatIso Cat (C , isSmallC) (C' , isSmallC')) + -- Iso.fun w = pathToIso ∘ Σ≡Prop (λ _ → isPropIsSet) ∘ CategoryPath.mk≡ + -- Iso.inv w (m , isiso inv sec ret) = ww + -- where + -- obIsom : Iso (C .ob) (C' .ob) + -- Iso.fun obIsom = F-ob m + -- Iso.inv obIsom = F-ob inv + -- Iso.rightInv obIsom = cong F-ob sec ≡$_ + -- Iso.leftInv obIsom = cong F-ob ret ≡$_ + + -- homIsom : (x y : C .ob) → + -- Iso (C .Hom[_,_] x y) + -- (C' .Hom[_,_] (fst (isoToEquiv obIsom) x) + -- (fst (isoToEquiv obIsom) y)) + -- Iso.fun (homIsom x y) = F-hom m + -- Iso.inv (homIsom x y) f = + -- subst2 (C [_,_]) (cong F-ob ret ≡$ x) ((cong F-ob ret ≡$ y)) + -- (F-hom inv f) + + -- Iso.rightInv (homIsom x y) b = + -- -- cong (F-hom m) + -- -- (fromPathP {A = (λ i → Hom[ C , F-ob (ret i) x ] (F-ob (ret i) y))} + -- -- {!!}) ∙ + -- {!!} ∙ + -- λ i → (fromPathP (cong F-hom sec)) i b + -- -- {!!} ∙ λ i → {!sec i .F-hom b!} + -- Iso.leftInv (homIsom x y) a = {!!} + + -- open CategoryPath + -- ww : CategoryPath C C' + -- ob≡ ww = ua (isoToEquiv obIsom) + -- Hom≡ ww = RelPathP _ λ x y → isoToEquiv $ homIsom x y + -- id≡ ww = {!!} + -- ⋆≡ ww = {!!} + -- Iso.rightInv w = {!!} + -- Iso.leftInv w = {!!} diff --git a/Cubical/Categories/Instances/Setoids.agda b/Cubical/Categories/Instances/Setoids.agda index 4942e1897e..595affba66 100644 --- a/Cubical/Categories/Instances/Setoids.agda +++ b/Cubical/Categories/Instances/Setoids.agda @@ -25,6 +25,7 @@ open import Cubical.Categories.Morphism open import Cubical.Categories.Functor open import Cubical.Categories.NaturalTransformation open import Cubical.Categories.Equivalence.WeakEquivalence +open import Cubical.Categories.Equivalence.AdjointEquivalence open import Cubical.Categories.Adjoint open import Cubical.Categories.Functors.HomFunctor open import Cubical.Categories.Instances.Sets @@ -36,9 +37,14 @@ open import Cubical.Relation.Binary open import Cubical.Relation.Nullary open import Cubical.Relation.Binary.Setoid +open import Cubical.Categories.Category.Path + +open import Cubical.Categories.Instances.Cat + open import Cubical.Categories.Monoidal open import Cubical.Categories.Limits.Pullback +open import Cubical.Categories.Constructions.Slice.Functor open import Cubical.HITs.SetQuotients as / open import Cubical.HITs.PropositionalTruncation @@ -48,85 +54,86 @@ open Functor -SETPullback : ∀ ℓ → Pullbacks (SET ℓ) -SETPullback ℓ (cospan l m r s₁ s₂) = w - where - open Pullback - w : Pullback (SET ℓ) (cospan l m r s₁ s₂) - pbOb w = _ , isSetΣ (isSet× (snd l) (snd r)) - (uncurry λ x y → isOfHLevelPath 2 (snd m) (s₁ x) (s₂ y)) - pbPr₁ w = fst ∘ fst - pbPr₂ w = snd ∘ fst - pbCommutes w = funExt snd - fst (fst (univProp w h k H')) d = _ , (H' ≡$ d) - snd (fst (univProp w h k H')) = refl , refl - snd (univProp w h k H') y = - Σ≡Prop - (λ _ → isProp× (isSet→ (snd l) _ _) (isSet→ (snd r) _ _)) - (funExt λ x → Σ≡Prop (λ _ → (snd m) _ _) - λ i → fst (snd y) i x , snd (snd y) i x) +-- SETPullback : ∀ ℓ → Pullbacks (SET ℓ) +-- SETPullback ℓ (cospan l m r s₁ s₂) = w +-- where +-- open Pullback +-- w : Pullback (SET ℓ) (cospan l m r s₁ s₂) +-- pbOb w = _ , isSetΣ (isSet× (snd l) (snd r)) +-- (uncurry λ x y → isOfHLevelPath 2 (snd m) (s₁ x) (s₂ y)) +-- pbPr₁ w = fst ∘ fst +-- pbPr₂ w = snd ∘ fst +-- pbCommutes w = funExt snd +-- fst (fst (univProp w h k H')) d = _ , (H' ≡$ d) +-- snd (fst (univProp w h k H')) = refl , refl +-- snd (univProp w h k H') y = +-- Σ≡Prop +-- (λ _ → isProp× (isSet→ (snd l) _ _) (isSet→ (snd r) _ _)) +-- (funExt λ x → Σ≡Prop (λ _ → (snd m) _ _) +-- λ i → fst (snd y) i x , snd (snd y) i x) -module SetLCCC ℓ {X@(_ , isSetX) Y@(_ , isSetY) : hSet ℓ} (f : ⟨ X ⟩ → ⟨ Y ⟩) where - open BaseChangeFunctor (SET ℓ) X (SETPullback ℓ) {Y} f - - open Cubical.Categories.Adjoint.NaturalBijection - open _⊣_ - - open import Cubical.Categories.Instances.Cospan - open import Cubical.Categories.Limits.Limits - - Π/ : Functor (SliceCat (SET ℓ) X) (SliceCat (SET ℓ) Y) - F-ob Π/ (sliceob {S-ob = _ , isSetA} h) = - sliceob {S-ob = _ , (isSetΣ isSetY $ - λ y → isSetΠ λ ((x , _) : fiber f y) → - isOfHLevelFiber 2 isSetA isSetX h x)} fst - F-hom Π/ {a} {b} (slicehom g p) = - slicehom (map-snd (map-sndDep (λ q → (p ≡$ _) ∙ q ) ∘_)) refl - F-id Π/ = SliceHom-≡-intro' _ _ $ - funExt λ x' → cong ((fst x') ,_) - (funExt λ y → Σ≡Prop (λ _ → isSetX _ _) refl) - F-seq Π/ _ _ = SliceHom-≡-intro' _ _ $ - funExt λ x' → cong ((fst x') ,_) - (funExt λ y → Σ≡Prop (λ _ → isSetX _ _) refl) - - f*⊣Π/ : BaseChangeFunctor ⊣ Π/ - Iso.fun (adjIso f*⊣Π/) (slicehom h p) = - slicehom (λ _ → _ , λ (_ , q) → h (_ , q) , (p ≡$ _)) refl - Iso.inv (adjIso f*⊣Π/) (slicehom h p) = - slicehom _ $ funExt λ (_ , q) → snd (snd (h _) (_ , q ∙ ((sym p) ≡$ _))) - Iso.rightInv (adjIso f*⊣Π/) b = SliceHom-≡-intro' _ _ $ - funExt λ _ → cong₂ _,_ (sym (S-comm b ≡$ _)) - $ toPathP $ funExt λ _ → - Σ≡Prop (λ _ → isSetX _ _) $ transportRefl _ ∙ - cong (fst ∘ snd (S-hom b _)) - (Σ≡Prop (λ _ → isSetY _ _) $ transportRefl _) - Iso.leftInv (adjIso f*⊣Π/) a = SliceHom-≡-intro' _ _ $ - funExt λ _ → cong (S-hom a) $ Σ≡Prop (λ _ → isSetY _ _) refl - adjNatInD f*⊣Π/ _ _ = SliceHom-≡-intro' _ _ $ - funExt λ _ → cong₂ _,_ refl $ - funExt λ _ → Σ≡Prop (λ _ → isSetX _ _) refl - adjNatInC f*⊣Π/ g h = SliceHom-≡-intro' _ _ $ - funExt λ _ → cong (fst ∘ (snd (S-hom g (S-hom h _)) ∘ (_ ,_))) $ isSetY _ _ _ _ - - Σ/ : Functor (SliceCat (SET ℓ) X) (SliceCat (SET ℓ) Y) - F-ob Σ/ (sliceob {S-ob = ob} arr) = sliceob {S-ob = ob} (f ∘ arr ) - F-hom Σ/ (slicehom g p) = slicehom _ (cong (f ∘_) p) - F-id Σ/ = refl - F-seq Σ/ _ _ = SliceHom-≡-intro' _ _ $ refl - - Σ/⊣f* : Σ/ ⊣ BaseChangeFunctor - Iso.fun (adjIso Σ/⊣f*) (slicehom g p) = slicehom (λ _ → _ , (sym p ≡$ _ )) refl - Iso.inv (adjIso Σ/⊣f*) (slicehom g p) = slicehom (snd ∘ fst ∘ g) $ - funExt (λ x → sym (snd (g x))) ∙ cong (f ∘_) p - Iso.rightInv (adjIso Σ/⊣f*) (slicehom g p) = - SliceHom-≡-intro' _ _ $ - funExt λ xx → Σ≡Prop (λ _ → isSetY _ _) - (ΣPathP (sym (p ≡$ _) , refl)) - Iso.leftInv (adjIso Σ/⊣f*) _ = SliceHom-≡-intro' _ _ $ refl - adjNatInD Σ/⊣f* _ _ = SliceHom-≡-intro' _ _ $ - funExt λ x → Σ≡Prop (λ _ → isSetY _ _) refl - adjNatInC Σ/⊣f* _ _ = SliceHom-≡-intro' _ _ $ refl - +-- module SetLCCC ℓ {X@(_ , isSetX) Y@(_ , isSetY) : hSet ℓ} (f : ⟨ X ⟩ → ⟨ Y ⟩) where +-- open BaseChange (SETPullback ℓ) + +-- open Cubical.Categories.Adjoint.NaturalBijection +-- open _⊣_ + +-- open import Cubical.Categories.Instances.Cospan +-- open import Cubical.Categories.Limits.Limits + +-- Π/ : Functor (SliceCat (SET ℓ) X) (SliceCat (SET ℓ) Y) +-- F-ob Π/ (sliceob {S-ob = _ , isSetA} h) = +-- sliceob {S-ob = _ , (isSetΣ isSetY $ +-- λ y → isSetΠ λ ((x , _) : fiber f y) → +-- isOfHLevelFiber 2 isSetA isSetX h x)} fst +-- F-hom Π/ {a} {b} (slicehom g p) = +-- slicehom (map-snd (map-sndDep (λ q → (p ≡$ _) ∙ q ) ∘_)) refl +-- F-id Π/ = SliceHom-≡-intro' _ _ $ +-- funExt λ x' → cong ((fst x') ,_) +-- (funExt λ y → Σ≡Prop (λ _ → isSetX _ _) refl) +-- F-seq Π/ _ _ = SliceHom-≡-intro' _ _ $ +-- funExt λ x' → cong ((fst x') ,_) +-- (funExt λ y → Σ≡Prop (λ _ → isSetX _ _) refl) + +-- f*⊣Π/ : f ＊ ⊣ Π/ +-- Iso.fun (adjIso f*⊣Π/) (slicehom h p) = +-- slicehom (λ _ → _ , λ (_ , q) → h (_ , q) , (p ≡$ _)) refl +-- Iso.inv (adjIso f*⊣Π/) (slicehom h p) = +-- slicehom _ $ funExt λ (_ , q) → snd (snd (h _) (_ , q ∙ ((sym p) ≡$ _))) +-- Iso.rightInv (adjIso f*⊣Π/) b = SliceHom-≡-intro' _ _ $ +-- funExt λ _ → cong₂ _,_ (sym (S-comm b ≡$ _)) +-- $ toPathP $ funExt λ _ → +-- Σ≡Prop (λ _ → isSetX _ _) $ transportRefl _ ∙ +-- cong (fst ∘ snd (S-hom b _)) +-- (Σ≡Prop (λ _ → isSetY _ _) $ transportRefl _) +-- Iso.leftInv (adjIso f*⊣Π/) a = SliceHom-≡-intro' _ _ $ +-- funExt λ _ → cong (S-hom a) $ Σ≡Prop (λ _ → isSetY _ _) refl +-- adjNatInD f*⊣Π/ _ _ = SliceHom-≡-intro' _ _ $ +-- funExt λ _ → cong₂ _,_ refl $ +-- funExt λ _ → Σ≡Prop (λ _ → isSetX _ _) refl +-- adjNatInC f*⊣Π/ g h = SliceHom-≡-intro' _ _ $ +-- funExt λ _ → cong (fst ∘ (snd (S-hom g (S-hom h _)) ∘ (_ ,_))) $ isSetY _ _ _ _ + +-- -- Σ/ : Functor (SliceCat (SET ℓ) X) (SliceCat (SET ℓ) Y) +-- -- F-ob Σ/ (sliceob {S-ob = ob} arr) = sliceob {S-ob = ob} (f ∘ arr ) +-- -- F-hom Σ/ (slicehom g p) = slicehom _ (cong (f ∘_) p) +-- -- F-id Σ/ = refl +-- -- F-seq Σ/ _ _ = SliceHom-≡-intro' _ _ $ refl + +-- -- Σ/⊣f* : Σ/ ⊣ BaseChangeFunctor +-- -- Iso.fun (adjIso Σ/⊣f*) (slicehom g p) = slicehom (λ _ → _ , (sym p ≡$ _ )) refl +-- -- Iso.inv (adjIso Σ/⊣f*) (slicehom g p) = slicehom (snd ∘ fst ∘ g) $ +-- -- funExt (λ x → sym (snd (g x))) ∙ cong (f ∘_) p +-- -- Iso.rightInv (adjIso Σ/⊣f*) (slicehom g p) = +-- -- SliceHom-≡-intro' _ _ $ +-- -- funExt λ xx → Σ≡Prop (λ _ → isSetY _ _) +-- -- (ΣPathP (sym (p ≡$ _) , refl)) +-- -- Iso.leftInv (adjIso Σ/⊣f*) _ = SliceHom-≡-intro' _ _ $ refl +-- -- adjNatInD Σ/⊣f* _ _ = SliceHom-≡-intro' _ _ $ +-- -- funExt λ x → Σ≡Prop (λ _ → isSetY _ _) refl +-- -- adjNatInC Σ/⊣f* _ _ = SliceHom-≡-intro' _ _ $ refl + + module _ ℓ where SETOID : Category (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ)) (ℓ-max ℓ ℓ) ob SETOID = Setoid ℓ ℓ @@ -141,6 +148,65 @@ module _ ℓ where isSetHom SETOID {y = (_ , isSetB) , ((_ , isPropR) , _)} = isSetΣ (isSet→ isSetB) (isProp→isSet ∘ isPropRespects isPropR ) + SETOID' : Category (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ)) (ℓ-max ℓ ℓ) + SETOID' = ΣPropCat (Cat ℓ ℓ) ((λ C → _ , isProp× (isPropIsThin C) (isPropIsGroupoidCat C)) ∘ fst) + + + SETOID→SETOID' : Functor SETOID SETOID' + F-ob SETOID→SETOID' ((X , isSetX) , ((_∼_ , isProp∼) , isEquivRel∼)) = (w , isSetX) + , isProp∼ , λ f → isiso (symmetric _ _ f) (isProp∼ _ _ _ _) (isProp∼ _ _ _ _) + where + open BinaryRelation.isEquivRel isEquivRel∼ + w : (Category ℓ ℓ) + ob w = X + Hom[_,_] w = _∼_ + id w = reflexive _ + _⋆_ w = transitive' + ⋆IdL w _ = isProp∼ _ _ _ _ + ⋆IdR w _ = isProp∼ _ _ _ _ + ⋆Assoc w _ _ _ = isProp∼ _ _ _ _ + isSetHom w = isProp→isSet (isProp∼ _ _) + + F-hom SETOID→SETOID' {y = (_ , ((_ , isProp∼') , _))} (f , f-resp) = w + where + w : Functor _ _ + F-ob w = f + F-hom w = f-resp + F-id w = isProp∼' _ _ _ _ + F-seq w _ _ = isProp∼' _ _ _ _ + F-id SETOID→SETOID' = Functor≡ (λ _ → refl) λ _ → refl + F-seq SETOID→SETOID' _ _ = Functor≡ (λ _ → refl) λ _ → refl + + SETOID'→SETOID : Functor SETOID' SETOID + F-ob SETOID'→SETOID ((C , isSetCob) , thin , isGrpCat) = + (_ , isSetCob) , (C [_,_] , thin) , + BinaryRelation.equivRel (λ _ → C .id) (λ _ _ → isIso.inv ∘ isGrpCat) + λ _ _ _ → C ._⋆_ + + F-hom SETOID'→SETOID F = _ , F-hom F + F-id SETOID'→SETOID = refl + F-seq SETOID'→SETOID _ _ = refl + + -- open AdjointEquivalence + -- WE : AdjointEquivalence SETOID SETOID' + -- fun WE = SETOID→SETOID' + -- inv WE = SETOID'→SETOID + -- NatTrans.N-ob (NatIso.trans (η WE)) _ = _ + -- NatTrans.N-hom (NatIso.trans (η WE)) _ = refl + -- NatIso.nIso (η WE) _ = snd (idCatIso) + -- F-ob (NatTrans.N-ob (NatIso.trans (ε WE)) _) = idfun _ + -- F-hom (NatTrans.N-ob (NatIso.trans (ε WE)) _) = idfun _ + -- F-id (NatTrans.N-ob (NatIso.trans (ε WE)) _) = refl + -- F-seq (NatTrans.N-ob (NatIso.trans (ε WE)) _) _ _ = refl + -- NatTrans.N-hom (NatIso.trans (ε WE)) _ = Functor≡ (λ _ → refl) (λ _ → refl) + -- F-ob (isIso.inv (NatIso.nIso (ε WE) (_ , _ , isGrpCat))) = idfun _ + -- F-hom (isIso.inv (NatIso.nIso (ε WE) (_ , _ , isGrpCat))) = idfun _ + -- F-id (isIso.inv (NatIso.nIso (ε WE) (_ , _ , isGrpCat))) = refl + -- F-seq (isIso.inv (NatIso.nIso (ε WE) (_ , _ , isGrpCat))) _ _ = refl + -- isIso.sec (NatIso.nIso (ε WE) (_ , _ , isGrpCat)) = {!SetoidMor !} + -- isIso.ret (NatIso.nIso (ε WE) (_ , _ , isGrpCat)) = {!!} + -- triangleIdentities WE = {!!} + open Iso IsoPathCatIsoSETOID : ∀ {x y} → Iso (x ≡ y) (CatIso SETOID x y) @@ -296,78 +362,70 @@ module _ ℓ where adjNatInD (⊗⊣^ X) {A} {d' = C} _ _ = SetoidMor≡ A (X ⟶ C) refl adjNatInC (⊗⊣^ X) {A} {d = C} _ _ = SetoidMor≡ (A ⊗ X) C refl - -- SetoidsMonoidalStr : StrictMonStr SETOID - -- TensorStr.─⊗─ (StrictMonStr.tenstr SetoidsMonoidalStr) = -⊗- - -- TensorStr.unit (StrictMonStr.tenstr SetoidsMonoidalStr) = setoidUnit - -- StrictMonStr.assoc SetoidsMonoidalStr _ _ _ = - -- Setoid≡ _ _ (invEquiv Σ-assoc-≃) λ _ _ → invEquiv Σ-assoc-≃ - -- StrictMonStr.idl SetoidsMonoidalStr _ = - -- Setoid≡ _ _ (isoToEquiv lUnit*×Iso) λ _ _ → isoToEquiv lUnit*×Iso - -- StrictMonStr.idr SetoidsMonoidalStr _ = - -- Setoid≡ _ _ (isoToEquiv rUnit*×Iso) λ _ _ → isoToEquiv rUnit*×Iso + + -- -- works but slow! + -- SetoidsMonoidalStrα : + -- -⊗- ∘F (𝟙⟨ SETOID ⟩ ×F -⊗-) ≅ᶜ + -- -⊗- ∘F (-⊗- ×F 𝟙⟨ SETOID ⟩) ∘F ×C-assoc SETOID SETOID SETOID + -- NatTrans.N-ob (NatIso.trans SetoidsMonoidalStrα) _ = + -- invEq Σ-assoc-≃ , invEq Σ-assoc-≃ + -- NatTrans.N-hom (NatIso.trans SetoidsMonoidalStrα) {x} {y} _ = + -- SetoidMor≡ + -- (F-ob (-⊗- ∘F (𝟙⟨ SETOID ⟩ ×F -⊗-)) x) + -- ((-⊗- ∘F (-⊗- ×F 𝟙⟨ SETOID ⟩) ∘F ×C-assoc SETOID SETOID SETOID) + -- .F-ob y) + -- refl + -- isIso.inv (NatIso.nIso SetoidsMonoidalStrα _) = + -- fst Σ-assoc-≃ , fst Σ-assoc-≃ + -- isIso.sec (NatIso.nIso SetoidsMonoidalStrα x) = refl + -- isIso.ret (NatIso.nIso SetoidsMonoidalStrα x) = refl + + -- SetoidsMonoidalStrη : -⊗- ∘F rinj SETOID SETOID setoidUnit ≅ᶜ 𝟙⟨ SETOID ⟩ + -- NatIso.trans SetoidsMonoidalStrη = + -- natTrans (λ _ → Iso.fun lUnit*×Iso , Iso.fun lUnit*×Iso) + -- λ {x} {y} _ → + -- SetoidMor≡ (F-ob (-⊗- ∘F rinj SETOID SETOID setoidUnit) x) y refl + -- NatIso.nIso SetoidsMonoidalStrη x = + -- isiso (Iso.inv lUnit*×Iso , Iso.inv lUnit*×Iso) refl refl + + -- SetoidsMonoidalStrρ : -⊗- ∘F linj SETOID SETOID setoidUnit ≅ᶜ 𝟙⟨ SETOID ⟩ + -- NatIso.trans SetoidsMonoidalStrρ = + -- natTrans (λ _ → Iso.fun rUnit*×Iso , Iso.fun rUnit*×Iso) + -- λ {x} {y} _ → + -- SetoidMor≡ (F-ob (-⊗- ∘F linj SETOID SETOID setoidUnit) x) y refl + -- NatIso.nIso SetoidsMonoidalStrρ x = + -- isiso (Iso.inv rUnit*×Iso , Iso.inv rUnit*×Iso) refl refl + - SetoidsMonoidalStrα : - -⊗- ∘F (𝟙⟨ SETOID ⟩ ×F -⊗-) ≅ᶜ - -⊗- ∘F (-⊗- ×F 𝟙⟨ SETOID ⟩) ∘F ×C-assoc SETOID SETOID SETOID - NatTrans.N-ob (NatIso.trans SetoidsMonoidalStrα) _ = - invEq Σ-assoc-≃ , invEq Σ-assoc-≃ - NatTrans.N-hom (NatIso.trans SetoidsMonoidalStrα) {x} {y} _ = - SetoidMor≡ - (F-ob (-⊗- ∘F (𝟙⟨ SETOID ⟩ ×F -⊗-)) x) - ((-⊗- ∘F (-⊗- ×F 𝟙⟨ SETOID ⟩) ∘F ×C-assoc SETOID SETOID SETOID) - .F-ob y) - refl - isIso.inv (NatIso.nIso SetoidsMonoidalStrα _) = - fst Σ-assoc-≃ , fst Σ-assoc-≃ - isIso.sec (NatIso.nIso SetoidsMonoidalStrα x) = refl - isIso.ret (NatIso.nIso SetoidsMonoidalStrα x) = refl - - SetoidsMonoidalStrη : -⊗- ∘F rinj SETOID SETOID setoidUnit ≅ᶜ 𝟙⟨ SETOID ⟩ - NatIso.trans SetoidsMonoidalStrη = - natTrans (λ _ → Iso.fun lUnit*×Iso , Iso.fun lUnit*×Iso) - λ {x} {y} _ → - SetoidMor≡ (F-ob (-⊗- ∘F rinj SETOID SETOID setoidUnit) x) y refl - NatIso.nIso SetoidsMonoidalStrη x = - isiso (Iso.inv lUnit*×Iso , Iso.inv lUnit*×Iso) refl refl - - SetoidsMonoidalStrρ : -⊗- ∘F linj SETOID SETOID setoidUnit ≅ᶜ 𝟙⟨ SETOID ⟩ - NatIso.trans SetoidsMonoidalStrρ = - natTrans (λ _ → Iso.fun rUnit*×Iso , Iso.fun rUnit*×Iso) - λ {x} {y} _ → - SetoidMor≡ (F-ob (-⊗- ∘F linj SETOID SETOID setoidUnit) x) y refl - NatIso.nIso SetoidsMonoidalStrρ x = - isiso (Iso.inv rUnit*×Iso , Iso.inv rUnit*×Iso) refl refl - - - SetoidsMonoidalStr : MonoidalStr SETOID - TensorStr.─⊗─ (MonoidalStr.tenstr SetoidsMonoidalStr) = -⊗- - TensorStr.unit (MonoidalStr.tenstr SetoidsMonoidalStr) = setoidUnit - MonoidalStr.α SetoidsMonoidalStr = SetoidsMonoidalStrα - MonoidalStr.η SetoidsMonoidalStr = SetoidsMonoidalStrη - MonoidalStr.ρ SetoidsMonoidalStr = SetoidsMonoidalStrρ - MonoidalStr.pentagon SetoidsMonoidalStr w x y z = refl - MonoidalStr.triangle SetoidsMonoidalStr x y = refl - - E-Category = - EnrichedCategory (record { C = _ ; monstr = SetoidsMonoidalStr }) - - E-SETOIDS : E-Category (ℓ-suc ℓ) - EnrichedCategory.ob E-SETOIDS = Setoid ℓ ℓ - EnrichedCategory.Hom[_,_] E-SETOIDS = _⟶_ - EnrichedCategory.id E-SETOIDS {x} = - (λ _ → id SETOID {x}) , - λ _ _ → BinaryRelation.isEquivRel.reflexive (snd (snd x)) _ - EnrichedCategory.seq E-SETOIDS x y z = - uncurry (_⋆_ SETOID {x} {y} {z}) , - λ {(f , g)} {(f' , g')} (fr , gr) a → - transitive' (gr (fst f a)) (snd g' (fr a)) - where open BinaryRelation.isEquivRel (snd (snd z)) - EnrichedCategory.⋆IdL E-SETOIDS x y = - SetoidMor≡ (setoidUnit ⊗ (x ⟶ y)) (x ⟶ y) refl - EnrichedCategory.⋆IdR E-SETOIDS x y = - SetoidMor≡ ((x ⟶ y) ⊗ setoidUnit) (x ⟶ y) refl - EnrichedCategory.⋆Assoc E-SETOIDS x y z w = - SetoidMor≡ ((x ⟶ y) ⊗ ( (y ⟶ z) ⊗ (z ⟶ w))) (x ⟶ w) refl + -- SetoidsMonoidalStr : MonoidalStr SETOID + -- TensorStr.─⊗─ (MonoidalStr.tenstr SetoidsMonoidalStr) = -⊗- + -- TensorStr.unit (MonoidalStr.tenstr SetoidsMonoidalStr) = setoidUnit + -- MonoidalStr.α SetoidsMonoidalStr = SetoidsMonoidalStrα + -- MonoidalStr.η SetoidsMonoidalStr = SetoidsMonoidalStrη + -- MonoidalStr.ρ SetoidsMonoidalStr = SetoidsMonoidalStrρ + -- MonoidalStr.pentagon SetoidsMonoidalStr w x y z = refl + -- MonoidalStr.triangle SetoidsMonoidalStr x y = refl + + -- E-Category = + -- EnrichedCategory (record { C = _ ; monstr = SetoidsMonoidalStr }) + + -- E-SETOIDS : E-Category (ℓ-suc ℓ) + -- EnrichedCategory.ob E-SETOIDS = Setoid ℓ ℓ + -- EnrichedCategory.Hom[_,_] E-SETOIDS = _⟶_ + -- EnrichedCategory.id E-SETOIDS {x} = + -- (λ _ → id SETOID {x}) , + -- λ _ _ → BinaryRelation.isEquivRel.reflexive (snd (snd x)) _ + -- EnrichedCategory.seq E-SETOIDS x y z = + -- uncurry (_⋆_ SETOID {x} {y} {z}) , + -- λ {(f , g)} {(f' , g')} (fr , gr) a → + -- transitive' (gr (fst f a)) (snd g' (fr a)) + -- where open BinaryRelation.isEquivRel (snd (snd z)) + -- EnrichedCategory.⋆IdL E-SETOIDS x y = + -- SetoidMor≡ (setoidUnit ⊗ (x ⟶ y)) (x ⟶ y) refl + -- EnrichedCategory.⋆IdR E-SETOIDS x y = + -- SetoidMor≡ ((x ⟶ y) ⊗ setoidUnit) (x ⟶ y) refl + -- EnrichedCategory.⋆Assoc E-SETOIDS x y z w = + -- SetoidMor≡ ((x ⟶ y) ⊗ ( (y ⟶ z) ⊗ (z ⟶ w))) (x ⟶ w) refl @@ -430,240 +488,14 @@ module _ ℓ where ∣ (IdRel ⟅ d ⟆ , idfun _) , idCatIso ∣₁ --- -- -- -- pullbacks : Pullbacks SETOID --- -- -- -- pullbacks cspn = w --- -- -- -- where --- -- -- -- open Cospan cspn --- -- -- -- open Pullback --- -- -- -- w : Pullback (SETOID) cspn --- -- -- -- pbOb w = PullbackSetoid l r m s₁ s₂ --- -- -- -- pbPr₁ w = fst ∘ fst , fst ∘ fst --- -- -- -- pbPr₂ w = snd ∘ fst , snd ∘ fst --- -- -- -- pbCommutes w = SetoidMor≡ (PullbackSetoid l r m s₁ s₂) m (funExt snd) --- -- -- -- fst (fst (univProp w h k H')) = (λ x → (fst h x , fst k x) , --- -- -- -- (cong fst H' ≡$ x)) , --- -- -- -- λ {a} {b} x → ((snd h x) , (snd k x)) , snd s₁ ((snd h x)) --- -- -- -- snd (fst (univProp w {d} h k H')) = SetoidMor≡ d l refl , SetoidMor≡ d r refl --- -- -- -- snd (univProp w {d} h k H') y = Σ≡Prop --- -- -- -- (λ _ → isProp× (isSetHom (SETOID) {d} {l} _ _) --- -- -- -- (isSetHom (SETOID) {d} {r} _ _)) --- -- -- -- (SetoidMor≡ d (PullbackSetoid l r m s₁ s₂) --- -- -- -- (funExt λ x → Σ≡Prop (λ _ → snd (fst m) _ _) --- -- -- -- (cong₂ _,_ (λ i → fst (fst (snd y) i) x) --- -- -- -- (λ i → fst (snd (snd y) i) x)))) - - - module _ {X Y : ob SETOID} (f : SetoidMor X Y) where - open BaseChangeFunctor SETOID X pullbacks {Y} f public - - SΣ : ∀ {X} → (x : SliceOb SETOID X) → _ - SΣ {X} = λ x → SetoidΣ (S-ob x) X (S-arr x) - - SΠ : ∀ {X} → (x : SliceOb SETOID X) → _ - SΠ {X} = λ x → setoidSection (S-ob x) X (S-arr x) - - SETOIDΣ : Functor (SliceCat SETOID X) (SliceCat SETOID Y) - S-ob (F-ob SETOIDΣ x) = SΣ x - S-arr (F-ob SETOIDΣ x) = SETOID ._⋆_ {SΣ x} {X} {Y} - (setoidΣ-pr₁ (S-ob x) X (S-arr x)) f - fst (S-hom (F-hom SETOIDΣ x)) = fst (S-hom x) - snd (S-hom (F-hom SETOIDΣ x)) x₁ = - snd (S-hom x) (fst x₁) , subst2 (fst (fst (snd X))) - (cong fst (sym (S-comm x)) ≡$ _) - (cong fst (sym (S-comm x)) ≡$ _) (snd x₁) - S-comm (F-hom SETOIDΣ {x} {y} g) = - SetoidMor≡ (SΣ x) Y - (funExt λ u → cong (fst f) (cong fst (S-comm g) ≡$ u)) - F-id SETOIDΣ {x = x} = SliceHom-≡-intro' _ _ - (SetoidMor≡ (SΣ x) (SΣ x) refl) - F-seq SETOIDΣ {x = x} {_} {z} _ _ = SliceHom-≡-intro' _ _ - (SetoidMor≡ (SΣ x) (SΣ z) refl) - - SetoidΣ⊣BaseChange : SETOIDΣ ⊣ BaseChangeFunctor - fst (S-hom (fun (adjIso SetoidΣ⊣BaseChange {c}) h)) x = - (fst (S-arr c) x , fst (S-hom h) x ) , sym (cong fst (S-comm h) ≡$ x) - snd (S-hom (fun (adjIso SetoidΣ⊣BaseChange {c}) h)) g = - ((snd (S-arr c) g) , snd (S-hom h) (g , snd (S-arr c) g)) - S-comm (fun (adjIso SetoidΣ⊣BaseChange {c} ) _) = SetoidMor≡ (S-ob c) X refl - fst (S-hom (inv (adjIso SetoidΣ⊣BaseChange) h)) x = - snd (fst (fst (S-hom h) x)) - snd (S-hom (inv (adjIso SetoidΣ⊣BaseChange) x)) {c} {d} (r , r') = - snd (snd (S-hom x) r) - S-comm (inv (adjIso SetoidΣ⊣BaseChange {c} {d}) (slicehom (x , _) y)) = - SetoidMor≡ (SΣ c) Y - (sym (funExt (snd ∘ x)) ∙ congS ((fst f ∘_) ∘ fst) y) - rightInv (adjIso SetoidΣ⊣BaseChange {c} {d}) b = SliceHom-≡-intro' _ _ - (SetoidMor≡ (S-ob c) (S-ob (BaseChangeFunctor ⟅ d ⟆)) - (funExt λ x → Σ≡Prop (λ _ → snd (fst Y) _ _) - (cong (_, _) (sym (cong fst (S-comm b) ≡$ x))))) - leftInv (adjIso SetoidΣ⊣BaseChange {c} {d}) a = SliceHom-≡-intro' _ _ - (SetoidMor≡ ((S-ob (SETOIDΣ ⟅ c ⟆))) (S-ob d) refl) - adjNatInD SetoidΣ⊣BaseChange {c} {_} {d'} _ _ = SliceHom-≡-intro' _ _ - (SetoidMor≡ (S-ob c) (S-ob (BaseChangeFunctor ⟅ d' ⟆)) - (funExt λ _ → Σ≡Prop (λ _ → snd (fst Y) _ _) refl)) - adjNatInC SetoidΣ⊣BaseChange _ _ = SliceHom-≡-intro' _ _ refl - - - ¬BaseChange⊣SetoidΠ : ({X Y : ob SETOID} (f : SetoidMor X Y) → - Σ _ (BaseChangeFunctor {X} {Y} f ⊣_)) → ⊥.⊥ - ¬BaseChange⊣SetoidΠ isLCCC = Πob-full-rel Πob-full - - where - - 𝕀 : Setoid ℓ ℓ - 𝕀 = (Lift Bool , isOfHLevelLift 2 isSetBool) , fullEquivPropRel - - 𝟚 : Setoid ℓ ℓ - 𝟚 = (Lift Bool , isOfHLevelLift 2 isSetBool) , - ((_ , isOfHLevelLift 2 isSetBool) , isEquivRelIdRel) - - 𝑨 : SetoidMor (setoidUnit {ℓ} {ℓ}) 𝕀 - 𝑨 = (λ _ → lift true) , λ _ → _ - - 𝟚/ = sliceob {S-ob = 𝟚} ((λ _ → tt*) , λ {x} {x'} _ → tt*) - - - open Σ (isLCCC {(setoidUnit {ℓ} {ℓ})} {𝕀} 𝑨) renaming (fst to ΠA ; snd to Π⊣A*) - open _⊣_ Π⊣A* renaming (adjIso to aIso) - - module lem2 where - G = sliceob {S-ob = setoidUnit} ((λ x → lift false) , _) - - bcf = BaseChangeFunctor {(setoidUnit {ℓ} {ℓ})} {𝕀} 𝑨 ⟅ G ⟆ - - isPropFiberFalse : isProp (fiber (fst (S-arr (ΠA ⟅ 𝟚/ ⟆))) (lift false)) - isPropFiberFalse (x , p) (y , q) = - Σ≡Prop (λ _ _ _ → cong (cong lift) (isSetBool _ _ _ _)) - ((cong (fst ∘ S-hom) (isoInvInjective (aIso {G} {𝟚/}) - (slicehom - ((λ _ → x) , λ _ → BinaryRelation.isEquivRel.reflexive (snd (snd - (S-ob (F-ob ΠA 𝟚/)))) _) - ( SetoidMor≡ (S-ob G) 𝕀 (funExt λ _ → p))) - ((slicehom - ((λ _ → y) , λ _ → BinaryRelation.isEquivRel.reflexive (snd (snd - (S-ob (F-ob ΠA 𝟚/)))) _) - ( SetoidMor≡ (S-ob G) 𝕀 (funExt λ _ → q)))) - (SliceHom-≡-intro' _ _ - (SetoidMor≡ (bcf .S-ob) (𝟚/ .S-ob) - (funExt λ z → ⊥.rec (true≢false (cong lower (snd z))) - ))))) ≡$ _ ) - - - module lem3 where - G = sliceob {S-ob = 𝕀} (SETOID .id {𝕀}) - - aL : Iso - (fst (fst (S-ob 𝟚/))) - (SliceHom SETOID setoidUnit (BaseChangeFunctor 𝑨 ⟅ G ⟆) 𝟚/) - - fun aL h = - slicehom ((λ _ → h) - , λ _ → BinaryRelation.isEquivRel.reflexive (snd (snd - (S-ob 𝟚/))) _) refl - inv aL (slicehom (f , _) _) = f (_ , refl) - rightInv aL b = - SliceHom-≡-intro' _ _ - (SetoidMor≡ - ((BaseChangeFunctor {X = (setoidUnit {ℓ} {ℓ})} {𝕀} 𝑨 ⟅ G ⟆) .S-ob) - (𝟚/ .S-ob) (funExt λ x' → - cong (λ (x , y) → fst (S-hom b) ((tt* , x) , y)) - (isPropSingl _ _))) - leftInv aL _ = refl - - lem3 : Iso (fst (fst (S-ob 𝟚/))) (SliceHom SETOID 𝕀 G (ΠA ⟅ 𝟚/ ⟆)) - lem3 = compIso aL (aIso {G} {𝟚/}) - - - - module zzz3 = Iso (compIso LiftIso (lem3.lem3)) - - open BinaryRelation.isEquivRel (snd (snd (S-ob (ΠA ⟅ 𝟚/ ⟆)))) - piPt : Bool → fiber - (fst - (S-arr - (ΠA ⟅ 𝟚/ ⟆))) (lift true) - piPt b = (fst (S-hom (zzz3.fun b)) (lift true)) , - (cong fst (S-comm (zzz3.fun b)) ≡$ lift true) - - + -- open BaseChange pullbacks public - finLLem : fst (piPt true) ≡ fst (piPt false) - → ⊥.⊥ - finLLem p = - true≢false (isoFunInjective (compIso LiftIso (lem3.lem3)) _ _ - $ SliceHom-≡-intro' _ _ - $ SetoidMor≡ - ((lem3.G) .S-ob) - ((ΠA ⟅ 𝟚/ ⟆) .S-ob) - (funExt ( - λ where (lift false) → (congS fst (lem2.isPropFiberFalse - (_ , ((cong fst (S-comm (fun (lem3.lem3) (lift true))) ≡$ lift false))) - (_ , (cong fst (S-comm (fun (lem3.lem3) (lift false))) ≡$ lift false)))) - (lift true) → p))) - - - Πob-full : fst (fst (snd (S-ob (ΠA ⟅ 𝟚/ ⟆)))) - (fst (piPt false)) - (fst (piPt true)) - - Πob-full = - ((transitive' ((snd (S-hom (zzz3.fun false)) {lift true} {lift false} _)) - (transitive' - ((BinaryRelation.isRefl→impliedByIdentity - (fst (fst (snd (S-ob (ΠA ⟅ 𝟚/ ⟆))))) reflexive - (congS fst (lem2.isPropFiberFalse - (_ , ((cong fst (S-comm (fun (lem3.lem3) (lift false))) ≡$ lift false))) - (_ , (cong fst (S-comm (fun (lem3.lem3) (lift true))) ≡$ lift false)))) - )) - (snd (S-hom (zzz3.fun true)) {lift false} {lift true} _)))) - - Πob-full-rel : fst (fst (snd (S-ob (ΠA ⟅ 𝟚/ ⟆)))) - (fst (piPt false)) - (fst (piPt true)) - → ⊥.⊥ - Πob-full-rel rr = elim𝟚 Date: Sun, 28 Jan 2024 12:41:13 +0100 Subject: [PATCH 07/17] sliced adjoints --- Cubical/Categories/Adjoint.agda | 24 ++- Cubical/Categories/Category/Properties.agda | 11 +- .../Constructions/Slice/Functor.agda | 193 ++++++++++++++++++ Cubical/Categories/Functor/Properties.agda | 30 +-- Cubical/Categories/Limits/Pullback.agda | 3 + .../NaturalTransformation/Base.agda | 2 +- 6 files changed, 238 insertions(+), 25 deletions(-) create mode 100644 Cubical/Categories/Constructions/Slice/Functor.agda diff --git a/Cubical/Categories/Adjoint.agda b/Cubical/Categories/Adjoint.agda index 5d6c102ac3..957e0d1df6 100644 --- a/Cubical/Categories/Adjoint.agda +++ b/Cubical/Categories/Adjoint.agda @@ -31,7 +31,7 @@ equivalence. private variable - ℓC ℓC' ℓD ℓD' : Level + ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level {- ============================================== @@ -69,7 +69,7 @@ private variable C : Category ℓC ℓC' D : Category ℓC ℓC' - + E : Category ℓE ℓE' module _ {F : Functor C D} {G : Functor D C} where open UnitCounit @@ -125,8 +125,8 @@ module AdjointUniqeUpToNatIso where open _⊣_ H⊣G using (η ; Δ₂) open _⊣_ H'⊣G using (ε ; Δ₁) by-N-homs = - AssocCong₂⋆R {C = D} _ - (AssocCong₂⋆L {C = D} (sym (N-hom ε _)) _) + AssocCong₂⋆R D + (AssocCong₂⋆L D (sym (N-hom ε _))) ∙ cong₂ _D⋆_ (sym (F-seq H' _ _) ∙∙ cong (H' ⟪_⟫) ((sym (N-hom η _))) @@ -155,7 +155,7 @@ module AdjointUniqeUpToNatIso where (sym (F-seq F _ _) ∙∙ cong (F ⟪_⟫) (N-hom (F'⊣G .η) _) ∙∙ (F-seq F _ _)) - ∙∙ AssocCong₂⋆R {C = D} _ (N-hom (F⊣G .ε) _) + ∙∙ AssocCong₂⋆R D (N-hom (F⊣G .ε) _) where open _⊣_ inv (nIso F≅ᶜF' _) = _ sec (nIso F≅ᶜF' _) = s F⊣G F'⊣G @@ -232,6 +232,20 @@ module NaturalBijection where isRightAdjoint : {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (G : Functor D C) → Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) isRightAdjoint {C = C}{D} G = Σ[ F ∈ Functor C D ] F ⊣ G +module Compose {F : Functor C D} {G : Functor D C} + {L : Functor D E} {R : Functor E D} + where + open NaturalBijection + module _ (F⊣G : F ⊣ G) (L⊣R : L ⊣ R) where + open _⊣_ + + LF⊣GR : (L ∘F F) ⊣ (G ∘F R) + adjIso LF⊣GR = compIso (adjIso L⊣R) (adjIso F⊣G) + adjNatInD LF⊣GR f k = + cong (adjIso F⊣G .fun) (adjNatInD L⊣R _ _) ∙ adjNatInD F⊣G _ _ + adjNatInC LF⊣GR f k = + cong (adjIso L⊣R .inv) (adjNatInC F⊣G _ _) ∙ adjNatInC L⊣R _ _ + {- ============================================== Proofs of equivalence diff --git a/Cubical/Categories/Category/Properties.agda b/Cubical/Categories/Category/Properties.agda index 0040358578..eca5e14ed5 100644 --- a/Cubical/Categories/Category/Properties.agda +++ b/Cubical/Categories/Category/Properties.agda @@ -92,26 +92,27 @@ module _ {C : Category ℓ ℓ'} where → f ⋆⟨ C ⟩ g ≡ seqP' {p = p} f' g rCatWhiskerP f' f g r = cong (λ v → v ⋆⟨ C ⟩ g) (sym (fromPathP r)) +module _ (C : Category ℓ ℓ') where AssocCong₂⋆L : {x y' y z w : C .ob} → {f' : C [ x , y' ]} {f : C [ x , y ]} {g' : C [ y' , z ]} {g : C [ y , z ]} - → f ⋆⟨ C ⟩ g ≡ f' ⋆⟨ C ⟩ g' → (h : C [ z , w ]) + → f ⋆⟨ C ⟩ g ≡ f' ⋆⟨ C ⟩ g' → {h : C [ z , w ]} → f ⋆⟨ C ⟩ (g ⋆⟨ C ⟩ h) ≡ f' ⋆⟨ C ⟩ (g' ⋆⟨ C ⟩ h) - AssocCong₂⋆L p h = - sym (⋆Assoc C _ _ h) + AssocCong₂⋆L p {h} = + sym (⋆Assoc C _ _ _) ∙∙ (λ i → p i ⋆⟨ C ⟩ h) ∙∙ ⋆Assoc C _ _ h AssocCong₂⋆R : {x y z z' w : C .ob} → - (f : C [ x , y ]) + {f : C [ x , y ]} {g' : C [ y , z' ]} {g : C [ y , z ]} {h' : C [ z' , w ]} {h : C [ z , w ]} → g ⋆⟨ C ⟩ h ≡ g' ⋆⟨ C ⟩ h' → (f ⋆⟨ C ⟩ g) ⋆⟨ C ⟩ h ≡ (f ⋆⟨ C ⟩ g') ⋆⟨ C ⟩ h' - AssocCong₂⋆R f p = + AssocCong₂⋆R {f = f} p = ⋆Assoc C f _ _ ∙∙ (λ i → f ⋆⟨ C ⟩ p i) ∙∙ sym (⋆Assoc C _ _ _) diff --git a/Cubical/Categories/Constructions/Slice/Functor.agda b/Cubical/Categories/Constructions/Slice/Functor.agda new file mode 100644 index 0000000000..1ab6901ff9 --- /dev/null +++ b/Cubical/Categories/Constructions/Slice/Functor.agda @@ -0,0 +1,193 @@ +{-# OPTIONS --safe #-} + +module Cubical.Categories.Constructions.Slice.Functor where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.Isomorphism + +open import Cubical.Categories.Category +open import Cubical.Categories.Category.Properties + +open import Cubical.Categories.Constructions.Slice.Base + +open import Cubical.Categories.Limits.Pullback +open import Cubical.Categories.Functor +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Adjoint + +open import Cubical.Tactics.FunctorSolver.Reflection + + +open Category hiding (_∘_) +open Functor +open NatTrans + +private + variable + ℓ ℓ' : Level + C D : Category ℓ ℓ' + c d : C .ob + +infix 39 _F/_ +infix 40 ∑_ + +_F/_ : ∀ (F : Functor C D) c → Functor (SliceCat C c) (SliceCat D (F ⟅ c ⟆)) +F-ob (F F/ c) = sliceob ∘ F ⟪_⟫ ∘ S-arr +F-hom (F F/ c) h = slicehom _ + $ sym ( F-seq F _ _) ∙ cong (F ⟪_⟫) (S-comm h) +F-id (F F/ c) = SliceHom-≡-intro' _ _ $ F-id F +F-seq (F F/ c) _ _ = SliceHom-≡-intro' _ _ $ F-seq F _ _ + + +∑_ : ∀ {c d} f → Functor (SliceCat C c) (SliceCat C d) +F-ob (∑_ {C = C} f) (sliceob x) = sliceob (_⋆_ C x f) +F-hom (∑_ {C = C} f) (slicehom h p) = slicehom _ $ + sym (C .⋆Assoc _ _ _) ∙ cong (comp' C f) p +F-id (∑ f) = SliceHom-≡-intro' _ _ refl +F-seq (∑ f) _ _ = SliceHom-≡-intro' _ _ refl + +module _ (Pbs : Pullbacks C) where + + open Category C using () renaming (_⋆_ to _⋆ᶜ_) + + module BaseChange {c d} (𝑓 : C [ c , d ]) where + infix 40 _＊ + + module _ {x@(sliceob arr) : SliceOb C d} where + open Pullback (Pbs (cospan _ _ _ 𝑓 arr)) public + + module _ {x} {y} ((slicehom h h-comm) : SliceCat C d [ y , x ]) where + + pbU = univProp (pbPr₁ {x = y}) (pbPr₂ ⋆ᶜ h) + (pbCommutes {x = y} ∙∙ cong (pbPr₂ ⋆ᶜ_) (sym (h-comm)) ∙∙ sym (C .⋆Assoc _ _ _)) + .fst .snd + + _＊ : Functor (SliceCat C d) (SliceCat C c) + F-ob _＊ x = sliceob (pbPr₁ {x = x}) + F-hom _＊ f = slicehom _ (sym (fst (pbU f))) + F-id _＊ = SliceHom-≡-intro' _ _ $ univPropEq (sym (C .⋆IdL _)) (C .⋆IdR _ ∙ sym (C .⋆IdL _)) + + F-seq _＊ _ _ = + let (u₁ , v₁) = pbU _ ; (u₂ , v₂) = pbU _ + in SliceHom-≡-intro' _ _ $ univPropEq + (u₂ ∙∙ cong (C ⋆ _) u₁ ∙∙ sym (C .⋆Assoc _ _ _)) + (sym (C .⋆Assoc _ _ _) ∙∙ cong (comp' C _) v₂ ∙∙ AssocCong₂⋆R C v₁) + + open BaseChange using (_＊) + open NaturalBijection renaming (_⊣_ to _⊣₂_) + open Iso + open _⊣₂_ + + + module _ (𝑓 : C [ c , d ]) where + + open BaseChange 𝑓 hiding (_＊) + + ∑𝑓⊣𝑓＊ : ∑ 𝑓 ⊣₂ 𝑓 ＊ + fun (adjIso ∑𝑓⊣𝑓＊) (slicehom h o) = + let ((_ , (p , _)) , _) = univProp _ _ (sym o) + in slicehom _ (sym p) + inv (adjIso ∑𝑓⊣𝑓＊) (slicehom h o) = slicehom _ $ + AssocCong₂⋆R C (sym (pbCommutes)) ∙ cong (_⋆ᶜ 𝑓) o + rightInv (adjIso ∑𝑓⊣𝑓＊) (slicehom h o) = + SliceHom-≡-intro' _ _ (univPropEq (sym o) refl) + leftInv (adjIso ∑𝑓⊣𝑓＊) (slicehom h o) = + let ((_ , (_ , q)) , _) = univProp _ _ _ + in SliceHom-≡-intro' _ _ (sym q) + adjNatInD ∑𝑓⊣𝑓＊ f k = SliceHom-≡-intro' _ _ $ + let ((h' , (v' , u')) , _) = univProp _ _ _ + ((_ , (v'' , u'')) , _) = univProp _ _ _ + in univPropEq (v' ∙∙ cong (h' ⋆ᶜ_) v'' ∙∙ sym (C .⋆Assoc _ _ _)) + (cong (_⋆ᶜ _) u' ∙ AssocCong₂⋆R C u'') + + adjNatInC ∑𝑓⊣𝑓＊ g h = SliceHom-≡-intro' _ _ $ C .⋆Assoc _ _ _ + + + open UnitCounit + + module SlicedAdjoint {L : Functor C D} {R} (L⊣R : L ⊣ R) where + + open Category D using () renaming (_⋆_ to _⋆ᵈ_) + + open _⊣_ L⊣R + + module _ {c} {d} where + module aI = Iso (adjIso (adj→adj' _ _ L⊣R) {c} {d}) + + module Left (b : D .ob) where + + ⊣F/ : Functor (SliceCat C (R ⟅ b ⟆)) (SliceCat D b) + ⊣F/ = ∑ (ε ⟦ b ⟧) ∘F L F/ (R ⟅ b ⟆) + + L/b⊣R/b : ⊣F/ ⊣₂ (R F/ b) + fun (adjIso L/b⊣R/b) (slicehom _ p) = slicehom _ $ + C .⋆Assoc _ _ _ + ∙∙ cong (_ ⋆ᶜ_) (sym (F-seq R _ _) ∙∙ cong (R ⟪_⟫) p ∙∙ F-seq R _ _) + ∙∙ AssocCong₂⋆L C (sym (N-hom η _)) + ∙∙ cong (_ ⋆ᶜ_) (Δ₂ _) + ∙∙ C .⋆IdR _ + + inv (adjIso L/b⊣R/b) (slicehom _ p) = + slicehom _ $ AssocCong₂⋆R D (sym (N-hom ε _)) + ∙ cong (_⋆ᵈ _) (sym (F-seq L _ _) ∙ cong (L ⟪_⟫) p) + rightInv (adjIso L/b⊣R/b) _ = SliceHom-≡-intro' _ _ $ aI.rightInv _ + leftInv (adjIso L/b⊣R/b) _ = SliceHom-≡-intro' _ _ $ aI.leftInv _ + adjNatInD L/b⊣R/b _ _ = SliceHom-≡-intro' _ _ $ + cong (_ ⋆ᶜ_) (F-seq R _ _) ∙ sym (C .⋆Assoc _ _ _) + adjNatInC L/b⊣R/b _ _ = SliceHom-≡-intro' _ _ $ + cong (_⋆ᵈ _) (F-seq L _ _) ∙ (D .⋆Assoc _ _ _) + + + module Right (b : C .ob) where + + F/⊣ : Functor (SliceCat D (L ⟅ b ⟆)) (SliceCat C b) + F/⊣ = (η ⟦ b ⟧) ＊ ∘F R F/ (L ⟅ b ⟆) + + open BaseChange (η ⟦ b ⟧) hiding (_＊) + + L/b⊣R/b : L F/ b ⊣₂ F/⊣ + fun (adjIso L/b⊣R/b) (slicehom f s) = slicehom _ $ + sym $ univProp _ _ (N-hom η _ ∙∙ + cong (_ ⋆ᶜ_) (cong (R ⟪_⟫) (sym s) ∙ F-seq R _ _) + ∙∙ sym (C .⋆Assoc _ _ _)) .fst .snd .fst + inv (adjIso L/b⊣R/b) (slicehom f s) = slicehom _ + (D .⋆Assoc _ _ _ + ∙∙ congS (_⋆ᵈ (ε ⟦ _ ⟧ ⋆ᵈ _)) (F-seq L _ _) + ∙∙ D .⋆Assoc _ _ _ ∙ cong (L ⟪ f ⟫ ⋆ᵈ_) + (cong (L ⟪ pbPr₂ ⟫ ⋆ᵈ_) (sym (N-hom ε _)) + ∙∙ sym (D .⋆Assoc _ _ _) + ∙∙ cong (_⋆ᵈ ε ⟦ F-ob L b ⟧) + (preserveCommF L $ sym pbCommutes) + ∙∙ D .⋆Assoc _ _ _ + ∙∙ cong (L ⟪ pbPr₁ ⟫ ⋆ᵈ_) (Δ₁ b) + ∙ D .⋆IdR _) + ∙∙ sym (F-seq L _ _) + ∙∙ cong (L ⟪_⟫) s) + + rightInv (adjIso L/b⊣R/b) h = SliceHom-≡-intro' _ _ $ + let p₂ : ∀ {x} → η ⟦ _ ⟧ ⋆ᶜ R ⟪ L ⟪ x ⟫ ⋆ᵈ ε ⟦ _ ⟧ ⟫ ≡ x + p₂ = cong (_ ⋆ᶜ_) (F-seq R _ _) ∙ + AssocCong₂⋆L C (sym (N-hom η _)) + ∙∙ cong (_ ⋆ᶜ_) (Δ₂ _) ∙∙ C .⋆IdR _ + + + in univPropEq (sym (S-comm h)) p₂ + + leftInv (adjIso L/b⊣R/b) _ = SliceHom-≡-intro' _ _ $ + cong ((_⋆ᵈ _) ∘ L ⟪_⟫) (sym (snd (snd (fst (univProp _ _ _))))) + ∙ aI.leftInv _ + adjNatInD L/b⊣R/b _ _ = SliceHom-≡-intro' _ _ $ + let (h , (u , v)) = univProp _ _ _ .fst + (u' , v') = pbU _ + + in univPropEq + (u ∙∙ cong (h ⋆ᶜ_) u' ∙∙ sym (C .⋆Assoc h _ _)) + (cong (_ ⋆ᶜ_) (F-seq R _ _) + ∙∙ sym (C .⋆Assoc _ _ _) ∙∙ + (cong (_⋆ᶜ _) v ∙ AssocCong₂⋆R C v')) + + adjNatInC L/b⊣R/b g h = let w = _ in SliceHom-≡-intro' _ _ $ + cong (_⋆ᵈ _) (cong (L ⟪_⟫) (C .⋆Assoc _ _ w) ∙ F-seq L _ (_ ⋆ᶜ w)) + ∙ D .⋆Assoc _ _ _ + diff --git a/Cubical/Categories/Functor/Properties.agda b/Cubical/Categories/Functor/Properties.agda index a6d378dea1..525498cba9 100644 --- a/Cubical/Categories/Functor/Properties.agda +++ b/Cubical/Categories/Functor/Properties.agda @@ -48,20 +48,6 @@ module _ {F : Functor C D} where F-rUnit i .F-id {x} = rUnit (F .F-id) (~ i) F-rUnit i .F-seq f g = rUnit (F .F-seq f g) (~ i) - -- functors preserve commutative diagrams (specificallysqures here) - preserveCommF : ∀ {x y z w} {f : C [ x , y ]} {g : C [ y , w ]} {h : C [ x , z ]} {k : C [ z , w ]} - → f ⋆⟨ C ⟩ g ≡ h ⋆⟨ C ⟩ k - → (F ⟪ f ⟫) ⋆⟨ D ⟩ (F ⟪ g ⟫) ≡ (F ⟪ h ⟫) ⋆⟨ D ⟩ (F ⟪ k ⟫) - preserveCommF {f = f} {g = g} {h = h} {k = k} eq - = (F ⟪ f ⟫) ⋆⟨ D ⟩ (F ⟪ g ⟫) - ≡⟨ sym (F .F-seq _ _) ⟩ - F ⟪ f ⋆⟨ C ⟩ g ⟫ - ≡⟨ cong (F ⟪_⟫) eq ⟩ - F ⟪ h ⋆⟨ C ⟩ k ⟫ - ≡⟨ F .F-seq _ _ ⟩ - (F ⟪ h ⟫) ⋆⟨ D ⟩ (F ⟪ k ⟫) - ∎ - -- functors preserve isomorphisms preserveIsosF : ∀ {x y} → CatIso C x y → CatIso D (F ⟅ x ⟆) (F ⟅ y ⟆) preserveIsosF {x} {y} (f , isiso f⁻¹ sec' ret') = @@ -123,6 +109,22 @@ 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₁ +module _ (F : Functor C D) where + + -- functors preserve commutative diagrams (specificallysqures here) + preserveCommF : ∀ {x y z w} {f : C [ x , y ]} {g : C [ y , w ]} {h : C [ x , z ]} {k : C [ z , w ]} + → f ⋆⟨ C ⟩ g ≡ h ⋆⟨ C ⟩ k + → (F ⟪ f ⟫) ⋆⟨ D ⟩ (F ⟪ g ⟫) ≡ (F ⟪ h ⟫) ⋆⟨ D ⟩ (F ⟪ k ⟫) + preserveCommF {f = f} {g = g} {h = h} {k = k} eq + = (F ⟪ f ⟫) ⋆⟨ D ⟩ (F ⟪ g ⟫) + ≡⟨ sym (F .F-seq _ _) ⟩ + F ⟪ f ⋆⟨ C ⟩ g ⟫ + ≡⟨ cong (F ⟪_⟫) eq ⟩ + F ⟪ h ⋆⟨ C ⟩ k ⟫ + ≡⟨ F .F-seq _ _ ⟩ + (F ⟪ h ⟫) ⋆⟨ D ⟩ (F ⟪ k ⟫) + ∎ + -- Conservative Functor, -- namely if a morphism f is mapped to an isomorphism, diff --git a/Cubical/Categories/Limits/Pullback.agda b/Cubical/Categories/Limits/Pullback.agda index a872212b80..2236cbcad0 100644 --- a/Cubical/Categories/Limits/Pullback.agda +++ b/Cubical/Categories/Limits/Pullback.agda @@ -53,6 +53,9 @@ module _ (C : Category ℓ ℓ') where pbCommutes : pbPr₁ ⋆ cspn .s₁ ≡ pbPr₂ ⋆ cspn .s₂ univProp : isPullback cspn pbPr₁ pbPr₂ pbCommutes + univPropEq : ∀ {c p₁ p₂ H g} p q → fst (fst (univProp {c} p₁ p₂ H)) ≡ g + univPropEq p q = cong fst (snd (univProp _ _ _) (_ , (p , q))) + open Pullback pullbackArrow : diff --git a/Cubical/Categories/NaturalTransformation/Base.agda b/Cubical/Categories/NaturalTransformation/Base.agda index 93b9fb2bd8..119b342dd0 100644 --- a/Cubical/Categories/NaturalTransformation/Base.agda +++ b/Cubical/Categories/NaturalTransformation/Base.agda @@ -242,7 +242,7 @@ module _ {B : Category ℓB ℓB'} {C : Category ℓC ℓC'} {D : Category ℓD _∘ʳ_ : ∀ (K : Functor C D) → {G H : Functor B C} (β : NatTrans G H) → NatTrans (K ∘F G) (K ∘F H) (_∘ʳ_ K {G} {H} β) .N-ob x = K ⟪ β ⟦ x ⟧ ⟫ - (_∘ʳ_ K {G} {H} β) .N-hom f = preserveCommF {C = C} {D = D} {K} (β .N-hom f) + (_∘ʳ_ K {G} {H} β) .N-hom f = preserveCommF K (β .N-hom f) whiskerTrans : {F F' : Functor B C} {G G' : Functor C D} (β : NatTrans G G') (α : NatTrans F F') → NatTrans (G ∘F F) (G' ∘F F') From 6d319cb7978a88d9be98625358114949bc1c2366 Mon Sep 17 00:00:00 2001 From: Marcin Grzybowski Date: Tue, 30 Jan 2024 23:50:35 +0100 Subject: [PATCH 08/17] wip --- Cubical/Categories/Instances/Sets.agda | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/Cubical/Categories/Instances/Sets.agda b/Cubical/Categories/Instances/Sets.agda index fd0589da27..68bcbcf102 100644 --- a/Cubical/Categories/Instances/Sets.agda +++ b/Cubical/Categories/Instances/Sets.agda @@ -7,6 +7,7 @@ open import Cubical.Foundations.HLevels open import Cubical.Foundations.Equiv open import Cubical.Foundations.Equiv.Properties open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function open import Cubical.Data.Unit open import Cubical.Data.Sigma open import Cubical.Categories.Category @@ -15,7 +16,7 @@ open import Cubical.Categories.NaturalTransformation open import Cubical.Categories.Limits -open Category +open Category hiding (_∘_) module _ ℓ where SET : Category (ℓ-suc ℓ) ℓ @@ -135,3 +136,25 @@ univProp (completeSET J D) c cc = (λ _ → funExt (λ _ → refl)) (λ x → isPropIsConeMor cc (limCone (completeSET J D)) x) (λ x hx → funExt (λ d → cone≡ λ u → funExt (λ _ → sym (funExt⁻ (hx u) d)))) + + +module _ {ℓ} where + + open Pullback + + PullbacksSET : Pullbacks (SET ℓ) + PullbacksSET (cospan l m r s₁ s₂) = pb + where + pb : Pullback (SET ℓ) (cospan l m r s₁ s₂) + pbOb pb = _ , isSetΣ (isSet× (snd l) (snd r)) + (uncurry λ x y → isOfHLevelPath 2 (snd m) (s₁ x) (s₂ y)) + pbPr₁ pb = fst ∘ fst + pbPr₂ pb = snd ∘ fst + pbCommutes pb = funExt snd + fst (fst (univProp pb h k H')) d = _ , (H' ≡$ d) + snd (fst (univProp pb h k H')) = refl , refl + snd (univProp pb h k H') y = + Σ≡Prop + (λ _ → isProp× (isSet→ (snd l) _ _) (isSet→ (snd r) _ _)) + (funExt λ x → Σ≡Prop (λ _ → (snd m) _ _) + λ i → fst (snd y) i x , snd (snd y) i x) From c42e23060295d863278f59af19176c155f0ff3f4 Mon Sep 17 00:00:00 2001 From: Marcin Grzybowski Date: Tue, 2 Apr 2024 04:20:42 +0200 Subject: [PATCH 09/17] cleanup --- Cubical/Categories/Instances/Sets.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Cubical/Categories/Instances/Sets.agda b/Cubical/Categories/Instances/Sets.agda index 68bcbcf102..a211ceef3c 100644 --- a/Cubical/Categories/Instances/Sets.agda +++ b/Cubical/Categories/Instances/Sets.agda @@ -139,9 +139,9 @@ univProp (completeSET J D) c cc = module _ {ℓ} where - + open Pullback - + PullbacksSET : Pullbacks (SET ℓ) PullbacksSET (cospan l m r s₁ s₂) = pb where From 46a83f8f9b721c75c08fc12748a31d068aff9193 Mon Sep 17 00:00:00 2001 From: Marcin Grzybowski Date: Tue, 2 Apr 2024 05:02:31 +0200 Subject: [PATCH 10/17] wip --- Cubical/Categories/Adjoint.agda | 3 + .../Instances/Functors/Currying.agda | 4 +- Cubical/Categories/Instances/Setoids.agda | 430 ++++++++---------- Cubical/Categories/Monoidal/Enriched.agda | 2 +- 4 files changed, 200 insertions(+), 239 deletions(-) diff --git a/Cubical/Categories/Adjoint.agda b/Cubical/Categories/Adjoint.agda index 957e0d1df6..9e69468f60 100644 --- a/Cubical/Categories/Adjoint.agda +++ b/Cubical/Categories/Adjoint.agda @@ -188,6 +188,9 @@ module NaturalBijection where record _⊣_ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) (G : Functor D C) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where field adjIso : ∀ {c d} → Iso (D [ F ⟅ c ⟆ , d ]) (C [ c , G ⟅ d ⟆ ]) + + adjEquiv : ∀ {c d} → (D [ F ⟅ c ⟆ , d ]) ≃ (C [ c , G ⟅ d ⟆ ]) + adjEquiv = isoToEquiv adjIso infix 40 _♭ infix 40 _♯ diff --git a/Cubical/Categories/Instances/Functors/Currying.agda b/Cubical/Categories/Instances/Functors/Currying.agda index 4a80b28976..9a34731e10 100644 --- a/Cubical/Categories/Instances/Functors/Currying.agda +++ b/Cubical/Categories/Instances/Functors/Currying.agda @@ -75,7 +75,7 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where F-seq (λF⁻ a) _ (eG , cG) = cong₂ (seq' D) (F-seq (F-ob a _) _ _) (cong (flip N-ob _) (F-seq a _ _)) - ∙ AssocCong₂⋆R {C = D} _ + ∙ AssocCong₂⋆R D (N-hom ((F-hom a _) ●ᵛ (F-hom a _)) _ ∙ (⋆Assoc D _ _ _) ∙ cong (seq' D _) (sym (N-hom (F-hom a eG) cG))) @@ -85,7 +85,7 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where N-ob (F-hom λF⁻Functor x) = uncurry (N-ob ∘→ N-ob x) N-hom ((F-hom λF⁻Functor) {F} {F'} x) {xx} {yy} = uncurry λ hh gg → - AssocCong₂⋆R {C = D} _ (cong N-ob (N-hom x hh) ≡$ _) + AssocCong₂⋆R D (cong N-ob (N-hom x hh) ≡$ _) ∙∙ cong (comp' D _) ((N-ob x (fst xx) .N-hom) gg) ∙∙ D .⋆Assoc _ _ _ diff --git a/Cubical/Categories/Instances/Setoids.agda b/Cubical/Categories/Instances/Setoids.agda index aa2ee62c35..50097e9280 100644 --- a/Cubical/Categories/Instances/Setoids.agda +++ b/Cubical/Categories/Instances/Setoids.agda @@ -33,6 +33,7 @@ open import Cubical.Categories.Constructions.BinProduct open import Cubical.Categories.Constructions.Slice open import Cubical.Categories.Constructions.FullSubcategory open import Cubical.Categories.Instances.Functors +open import Cubical.Categories.Instances.Functors.Currying open import Cubical.Relation.Binary open import Cubical.Relation.Nullary open import Cubical.Relation.Binary.Setoid @@ -187,26 +188,6 @@ module _ ℓ where F-id SETOID'→SETOID = refl F-seq SETOID'→SETOID _ _ = refl - -- open AdjointEquivalence - -- WE : AdjointEquivalence SETOID SETOID' - -- fun WE = SETOID→SETOID' - -- inv WE = SETOID'→SETOID - -- NatTrans.N-ob (NatIso.trans (η WE)) _ = _ - -- NatTrans.N-hom (NatIso.trans (η WE)) _ = refl - -- NatIso.nIso (η WE) _ = snd (idCatIso) - -- F-ob (NatTrans.N-ob (NatIso.trans (ε WE)) _) = idfun _ - -- F-hom (NatTrans.N-ob (NatIso.trans (ε WE)) _) = idfun _ - -- F-id (NatTrans.N-ob (NatIso.trans (ε WE)) _) = refl - -- F-seq (NatTrans.N-ob (NatIso.trans (ε WE)) _) _ _ = refl - -- NatTrans.N-hom (NatIso.trans (ε WE)) _ = Functor≡ (λ _ → refl) (λ _ → refl) - -- F-ob (isIso.inv (NatIso.nIso (ε WE) (_ , _ , isGrpCat))) = idfun _ - -- F-hom (isIso.inv (NatIso.nIso (ε WE) (_ , _ , isGrpCat))) = idfun _ - -- F-id (isIso.inv (NatIso.nIso (ε WE) (_ , _ , isGrpCat))) = refl - -- F-seq (isIso.inv (NatIso.nIso (ε WE) (_ , _ , isGrpCat))) _ _ = refl - -- isIso.sec (NatIso.nIso (ε WE) (_ , _ , isGrpCat)) = {!SetoidMor !} - -- isIso.ret (NatIso.nIso (ε WE) (_ , _ , isGrpCat)) = {!!} - -- triangleIdentities WE = {!!} - open Iso IsoPathCatIsoSETOID : ∀ {x y} → Iso (x ≡ y) (CatIso SETOID x y) @@ -363,71 +344,48 @@ module _ ℓ where adjNatInC (⊗⊣^ X) {A} {d = C} _ _ = SetoidMor≡ (A ⊗ X) C refl - -- -- works but slow! - -- SetoidsMonoidalStrα : - -- -⊗- ∘F (𝟙⟨ SETOID ⟩ ×F -⊗-) ≅ᶜ - -- -⊗- ∘F (-⊗- ×F 𝟙⟨ SETOID ⟩) ∘F ×C-assoc SETOID SETOID SETOID - -- NatTrans.N-ob (NatIso.trans SetoidsMonoidalStrα) _ = - -- invEq Σ-assoc-≃ , invEq Σ-assoc-≃ - -- NatTrans.N-hom (NatIso.trans SetoidsMonoidalStrα) {x} {y} _ = - -- SetoidMor≡ - -- (F-ob (-⊗- ∘F (𝟙⟨ SETOID ⟩ ×F -⊗-)) x) - -- ((-⊗- ∘F (-⊗- ×F 𝟙⟨ SETOID ⟩) ∘F ×C-assoc SETOID SETOID SETOID) - -- .F-ob y) - -- refl - -- isIso.inv (NatIso.nIso SetoidsMonoidalStrα _) = - -- fst Σ-assoc-≃ , fst Σ-assoc-≃ - -- isIso.sec (NatIso.nIso SetoidsMonoidalStrα x) = refl - -- isIso.ret (NatIso.nIso SetoidsMonoidalStrα x) = refl - - -- SetoidsMonoidalStrη : -⊗- ∘F rinj SETOID SETOID setoidUnit ≅ᶜ 𝟙⟨ SETOID ⟩ - -- NatIso.trans SetoidsMonoidalStrη = - -- natTrans (λ _ → Iso.fun lUnit*×Iso , Iso.fun lUnit*×Iso) - -- λ {x} {y} _ → - -- SetoidMor≡ (F-ob (-⊗- ∘F rinj SETOID SETOID setoidUnit) x) y refl - -- NatIso.nIso SetoidsMonoidalStrη x = - -- isiso (Iso.inv lUnit*×Iso , Iso.inv lUnit*×Iso) refl refl - - -- SetoidsMonoidalStrρ : -⊗- ∘F linj SETOID SETOID setoidUnit ≅ᶜ 𝟙⟨ SETOID ⟩ - -- NatIso.trans SetoidsMonoidalStrρ = - -- natTrans (λ _ → Iso.fun rUnit*×Iso , Iso.fun rUnit*×Iso) - -- λ {x} {y} _ → - -- SetoidMor≡ (F-ob (-⊗- ∘F linj SETOID SETOID setoidUnit) x) y refl - -- NatIso.nIso SetoidsMonoidalStrρ x = - -- isiso (Iso.inv rUnit*×Iso , Iso.inv rUnit*×Iso) refl refl - - - -- SetoidsMonoidalStr : MonoidalStr SETOID - -- TensorStr.─⊗─ (MonoidalStr.tenstr SetoidsMonoidalStr) = -⊗- - -- TensorStr.unit (MonoidalStr.tenstr SetoidsMonoidalStr) = setoidUnit - -- MonoidalStr.α SetoidsMonoidalStr = SetoidsMonoidalStrα - -- MonoidalStr.η SetoidsMonoidalStr = SetoidsMonoidalStrη - -- MonoidalStr.ρ SetoidsMonoidalStr = SetoidsMonoidalStrρ - -- MonoidalStr.pentagon SetoidsMonoidalStr w x y z = refl - -- MonoidalStr.triangle SetoidsMonoidalStr x y = refl - - -- E-Category = - -- EnrichedCategory (record { C = _ ; monstr = SetoidsMonoidalStr }) - - -- E-SETOIDS : E-Category (ℓ-suc ℓ) - -- EnrichedCategory.ob E-SETOIDS = Setoid ℓ ℓ - -- EnrichedCategory.Hom[_,_] E-SETOIDS = _⟶_ - -- EnrichedCategory.id E-SETOIDS {x} = - -- (λ _ → id SETOID {x}) , - -- λ _ _ → BinaryRelation.isEquivRel.reflexive (snd (snd x)) _ - -- EnrichedCategory.seq E-SETOIDS x y z = - -- uncurry (_⋆_ SETOID {x} {y} {z}) , - -- λ {(f , g)} {(f' , g')} (fr , gr) a → - -- transitive' (gr (fst f a)) (snd g' (fr a)) - -- where open BinaryRelation.isEquivRel (snd (snd z)) - -- EnrichedCategory.⋆IdL E-SETOIDS x y = - -- SetoidMor≡ (setoidUnit ⊗ (x ⟶ y)) (x ⟶ y) refl - -- EnrichedCategory.⋆IdR E-SETOIDS x y = - -- SetoidMor≡ ((x ⟶ y) ⊗ setoidUnit) (x ⟶ y) refl - -- EnrichedCategory.⋆Assoc E-SETOIDS x y z w = - -- SetoidMor≡ ((x ⟶ y) ⊗ ( (y ⟶ z) ⊗ (z ⟶ w))) (x ⟶ w) refl - - + -- works but slow! + SetoidsMonoidalStrα : + -⊗- ∘F (𝟙⟨ SETOID ⟩ ×F -⊗-) ≅ᶜ + -⊗- ∘F (-⊗- ×F 𝟙⟨ SETOID ⟩) ∘F ×C-assoc SETOID SETOID SETOID + NatTrans.N-ob (NatIso.trans SetoidsMonoidalStrα) _ = + invEq Σ-assoc-≃ , invEq Σ-assoc-≃ + NatTrans.N-hom (NatIso.trans SetoidsMonoidalStrα) {x} {y} _ = + SetoidMor≡ + (F-ob (-⊗- ∘F (𝟙⟨ SETOID ⟩ ×F -⊗-)) x) + ((-⊗- ∘F (-⊗- ×F 𝟙⟨ SETOID ⟩) ∘F ×C-assoc SETOID SETOID SETOID) + .F-ob y) + refl + isIso.inv (NatIso.nIso SetoidsMonoidalStrα _) = + fst Σ-assoc-≃ , fst Σ-assoc-≃ + isIso.sec (NatIso.nIso SetoidsMonoidalStrα x) = refl + isIso.ret (NatIso.nIso SetoidsMonoidalStrα x) = refl + + SetoidsMonoidalStrη : -⊗- ∘F rinj SETOID SETOID setoidUnit ≅ᶜ 𝟙⟨ SETOID ⟩ + NatIso.trans SetoidsMonoidalStrη = + natTrans (λ _ → Iso.fun lUnit*×Iso , Iso.fun lUnit*×Iso) + λ {x} {y} _ → + SetoidMor≡ (F-ob (-⊗- ∘F rinj SETOID SETOID setoidUnit) x) y refl + NatIso.nIso SetoidsMonoidalStrη x = + isiso (Iso.inv lUnit*×Iso , Iso.inv lUnit*×Iso) refl refl + + SetoidsMonoidalStrρ : -⊗- ∘F linj SETOID SETOID setoidUnit ≅ᶜ 𝟙⟨ SETOID ⟩ + NatIso.trans SetoidsMonoidalStrρ = + natTrans (λ _ → Iso.fun rUnit*×Iso , Iso.fun rUnit*×Iso) + λ {x} {y} _ → + SetoidMor≡ (F-ob (-⊗- ∘F linj SETOID SETOID setoidUnit) x) y refl + NatIso.nIso SetoidsMonoidalStrρ x = + isiso (Iso.inv rUnit*×Iso , Iso.inv rUnit*×Iso) refl refl + + + SetoidsMonoidalStr : MonoidalStr SETOID + TensorStr.─⊗─ (MonoidalStr.tenstr SetoidsMonoidalStr) = -⊗- + TensorStr.unit (MonoidalStr.tenstr SetoidsMonoidalStr) = setoidUnit + MonoidalStr.α SetoidsMonoidalStr = SetoidsMonoidalStrα + MonoidalStr.η SetoidsMonoidalStr = SetoidsMonoidalStrη + MonoidalStr.ρ SetoidsMonoidalStr = SetoidsMonoidalStrρ + MonoidalStr.pentagon SetoidsMonoidalStr w x y z = refl + MonoidalStr.triangle SetoidsMonoidalStr x y = refl pullbacks : Pullbacks SETOID pullbacks cspn = w @@ -491,165 +449,165 @@ module _ ℓ where - -- open BaseChange pullbacks public - - -- ¬BaseChange⊣SetoidΠ : ({X Y : ob SETOID} (f : SETOID .Hom[_,_] X Y) → - -- Σ (Functor (SliceCat SETOID X) (SliceCat SETOID Y)) - -- (λ Πf → (_＊ {c = X} {d = Y} f) ⊣ Πf)) → ⊥.⊥ - -- ¬BaseChange⊣SetoidΠ isLCCC = Πob-full-rel Πob-full - - -- where - - -- 𝕀 : Setoid ℓ ℓ - -- 𝕀 = (Lift Bool , isOfHLevelLift 2 isSetBool) , fullEquivPropRel - - -- 𝟚 : Setoid ℓ ℓ - -- 𝟚 = (Lift Bool , isOfHLevelLift 2 isSetBool) , - -- ((_ , isOfHLevelLift 2 isSetBool) , isEquivRelIdRel) - - -- 𝑨 : SetoidMor (setoidUnit {ℓ} {ℓ}) 𝕀 - -- 𝑨 = (λ _ → lift true) , λ _ → _ - - -- 𝑨＊ = _＊ {c = (setoidUnit {ℓ} {ℓ})} {𝕀} 𝑨 - - -- 𝟚/ = sliceob {S-ob = 𝟚} ((λ _ → tt*) , λ {x} {x'} _ → tt*) - - - -- open Σ (isLCCC {(setoidUnit {ℓ} {ℓ})} {𝕀} 𝑨) renaming (fst to ΠA ; snd to Π⊣A*) - -- open _⊣_ Π⊣A* renaming (adjIso to aIso) - - -- module lem2 where - -- G = sliceob {S-ob = setoidUnit} ((λ x → lift false) , _) - - -- bcf = 𝑨＊ ⟅ G ⟆ - - -- isPropFiberFalse : isProp (fiber (fst (S-arr (ΠA ⟅ 𝟚/ ⟆))) (lift false)) - -- isPropFiberFalse (x , p) (y , q) = - -- Σ≡Prop (λ _ _ _ → cong (cong lift) (isSetBool _ _ _ _)) - -- ((cong (fst ∘ S-hom) (isoInvInjective (aIso {G} {𝟚/}) - -- (slicehom - -- ((λ _ → x) , λ _ → BinaryRelation.isEquivRel.reflexive (snd (snd - -- (S-ob (F-ob ΠA 𝟚/)))) _) - -- ( SetoidMor≡ (S-ob G) 𝕀 (funExt λ _ → p))) - -- ((slicehom - -- ((λ _ → y) , λ _ → BinaryRelation.isEquivRel.reflexive (snd (snd - -- (S-ob (F-ob ΠA 𝟚/)))) _) - -- ( SetoidMor≡ (S-ob G) 𝕀 (funExt λ _ → q)))) - -- (SliceHom-≡-intro' _ _ - -- (SetoidMor≡ (bcf .S-ob) (𝟚/ .S-ob) - -- (funExt λ z → ⊥.rec (true≢false (cong lower (snd z))) - -- ))))) ≡$ _ ) - - - -- module lem3 where - -- G = sliceob {S-ob = 𝕀} (SETOID .id {𝕀}) - - -- aL : Iso - -- (fst (fst (S-ob 𝟚/))) - -- (SliceHom SETOID setoidUnit ( 𝑨 ＊ ⟅ G ⟆) 𝟚/) - - -- fun aL h = - -- slicehom ((λ _ → h) - -- , λ _ → BinaryRelation.isEquivRel.reflexive (snd (snd - -- (S-ob 𝟚/))) _) refl - -- inv aL (slicehom (f , _) _) = f (_ , refl) - -- rightInv aL b = - -- SliceHom-≡-intro' _ _ - -- (SetoidMor≡ - -- ((𝑨＊ ⟅ G ⟆) .S-ob) - -- (𝟚/ .S-ob) (funExt λ x' → - -- cong (λ (x , y) → fst (S-hom b) ((tt* , x) , y)) - -- (isPropSingl _ _))) - -- leftInv aL _ = refl - - -- lem3 : Iso (fst (fst (S-ob 𝟚/))) (SliceHom SETOID 𝕀 G (ΠA ⟅ 𝟚/ ⟆)) - -- lem3 = compIso aL (aIso {G} {𝟚/}) + open BaseChange pullbacks public + ¬BaseChange⊣SetoidΠ : ({X Y : ob SETOID} (f : SETOID .Hom[_,_] X Y) → + Σ (Functor (SliceCat SETOID X) (SliceCat SETOID Y)) + (λ Πf → (_＊ {c = X} {d = Y} f) ⊣ Πf)) → ⊥.⊥ + ¬BaseChange⊣SetoidΠ isLCCC = Πob-full-rel Πob-full + where - -- module zzz3 = Iso (compIso LiftIso (lem3.lem3)) + 𝕀 : Setoid ℓ ℓ + 𝕀 = (Lift Bool , isOfHLevelLift 2 isSetBool) , fullEquivPropRel + 𝟚 : Setoid ℓ ℓ + 𝟚 = (Lift Bool , isOfHLevelLift 2 isSetBool) , + ((_ , isOfHLevelLift 2 isSetBool) , isEquivRelIdRel) - -- open BinaryRelation.isEquivRel (snd (snd (S-ob (ΠA ⟅ 𝟚/ ⟆)))) + 𝑨 : SetoidMor (setoidUnit {ℓ} {ℓ}) 𝕀 + 𝑨 = (λ _ → lift true) , λ _ → _ + 𝑨＊ = _＊ {c = (setoidUnit {ℓ} {ℓ})} {𝕀} 𝑨 - -- piPt : Bool → fiber - -- (fst - -- (S-arr - -- (ΠA ⟅ 𝟚/ ⟆))) (lift true) - -- piPt b = (fst (S-hom (zzz3.fun b)) (lift true)) , - -- (cong fst (S-comm (zzz3.fun b)) ≡$ lift true) + 𝟚/ = sliceob {S-ob = 𝟚} ((λ _ → tt*) , λ {x} {x'} _ → tt*) + open Σ (isLCCC {(setoidUnit {ℓ} {ℓ})} {𝕀} 𝑨) renaming (fst to ΠA ; snd to Π⊣A*) + open _⊣_ Π⊣A* renaming (adjIso to aIso) - -- finLLem : fst (piPt true) ≡ fst (piPt false) - -- → ⊥.⊥ - -- finLLem p = - -- true≢false (isoFunInjective (compIso LiftIso (lem3.lem3)) _ _ - -- $ SliceHom-≡-intro' _ _ - -- $ SetoidMor≡ - -- ((lem3.G) .S-ob) - -- ((ΠA ⟅ 𝟚/ ⟆) .S-ob) - -- (funExt ( - -- λ where (lift false) → (congS fst (lem2.isPropFiberFalse - -- (_ , ((cong fst (S-comm (fun (lem3.lem3) (lift true))) ≡$ lift false))) - -- (_ , (cong fst (S-comm (fun (lem3.lem3) (lift false))) ≡$ lift false)))) - -- (lift true) → p))) - - - -- Πob-full : fst (fst (snd (S-ob (ΠA ⟅ 𝟚/ ⟆)))) - -- (fst (piPt false)) - -- (fst (piPt true)) - - -- Πob-full = - -- ((transitive' ((snd (S-hom (zzz3.fun false)) {lift true} {lift false} _)) - -- (transitive' - -- ((BinaryRelation.isRefl→impliedByIdentity - -- (fst (fst (snd (S-ob (ΠA ⟅ 𝟚/ ⟆))))) reflexive - -- (congS fst (lem2.isPropFiberFalse - -- (_ , ((cong fst (S-comm (fun (lem3.lem3) (lift false))) ≡$ lift false))) - -- (_ , (cong fst (S-comm (fun (lem3.lem3) (lift true))) ≡$ lift false)))) - -- )) - -- (snd (S-hom (zzz3.fun true)) {lift false} {lift true} _)))) - - -- Πob-full-rel : fst (fst (snd (S-ob (ΠA ⟅ 𝟚/ ⟆)))) - -- (fst (piPt false)) - -- (fst (piPt true)) - -- → ⊥.⊥ - -- Πob-full-rel rr = elim𝟚 Date: Tue, 2 Apr 2024 05:55:35 +0200 Subject: [PATCH 11/17] small fix --- Cubical/Categories/Instances/Functors/Currying.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Cubical/Categories/Instances/Functors/Currying.agda b/Cubical/Categories/Instances/Functors/Currying.agda index 4a80b28976..9a34731e10 100644 --- a/Cubical/Categories/Instances/Functors/Currying.agda +++ b/Cubical/Categories/Instances/Functors/Currying.agda @@ -75,7 +75,7 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where F-seq (λF⁻ a) _ (eG , cG) = cong₂ (seq' D) (F-seq (F-ob a _) _ _) (cong (flip N-ob _) (F-seq a _ _)) - ∙ AssocCong₂⋆R {C = D} _ + ∙ AssocCong₂⋆R D (N-hom ((F-hom a _) ●ᵛ (F-hom a _)) _ ∙ (⋆Assoc D _ _ _) ∙ cong (seq' D _) (sym (N-hom (F-hom a eG) cG))) @@ -85,7 +85,7 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where N-ob (F-hom λF⁻Functor x) = uncurry (N-ob ∘→ N-ob x) N-hom ((F-hom λF⁻Functor) {F} {F'} x) {xx} {yy} = uncurry λ hh gg → - AssocCong₂⋆R {C = D} _ (cong N-ob (N-hom x hh) ≡$ _) + AssocCong₂⋆R D (cong N-ob (N-hom x hh) ≡$ _) ∙∙ cong (comp' D _) ((N-ob x (fst xx) .N-hom) gg) ∙∙ D .⋆Assoc _ _ _ From b9e93947345f73cae97ad6d75385973d3e4c5307 Mon Sep 17 00:00:00 2001 From: Marcin Grzybowski Date: Thu, 4 Apr 2024 01:42:38 +0200 Subject: [PATCH 12/17] cleanup --- Cubical/Categories/Adjoint.agda | 4 +- Cubical/Categories/Instances/Setoids.agda | 99 +++---------------- Cubical/Categories/Instances/Sets.agda | 11 --- .../Categories/Instances/Sets/Properties.agda | 64 ++++++++++++ Cubical/Relation/Binary/Setoid.agda | 16 ++- 5 files changed, 91 insertions(+), 103 deletions(-) create mode 100644 Cubical/Categories/Instances/Sets/Properties.agda diff --git a/Cubical/Categories/Adjoint.agda b/Cubical/Categories/Adjoint.agda index 9e69468f60..6695102064 100644 --- a/Cubical/Categories/Adjoint.agda +++ b/Cubical/Categories/Adjoint.agda @@ -188,9 +188,9 @@ module NaturalBijection where record _⊣_ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) (G : Functor D C) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where field adjIso : ∀ {c d} → Iso (D [ F ⟅ c ⟆ , d ]) (C [ c , G ⟅ d ⟆ ]) - + adjEquiv : ∀ {c d} → (D [ F ⟅ c ⟆ , d ]) ≃ (C [ c , G ⟅ d ⟆ ]) - adjEquiv = isoToEquiv adjIso + adjEquiv = isoToEquiv adjIso infix 40 _♭ infix 40 _♯ diff --git a/Cubical/Categories/Instances/Setoids.agda b/Cubical/Categories/Instances/Setoids.agda index 50097e9280..2dc17f63e3 100644 --- a/Cubical/Categories/Instances/Setoids.agda +++ b/Cubical/Categories/Instances/Setoids.agda @@ -38,8 +38,6 @@ open import Cubical.Relation.Binary open import Cubical.Relation.Nullary open import Cubical.Relation.Binary.Setoid -open import Cubical.Categories.Category.Path - open import Cubical.Categories.Instances.Cat open import Cubical.Categories.Monoidal @@ -54,87 +52,6 @@ open Category hiding (_∘_) open Functor - --- SETPullback : ∀ ℓ → Pullbacks (SET ℓ) --- SETPullback ℓ (cospan l m r s₁ s₂) = w --- where --- open Pullback --- w : Pullback (SET ℓ) (cospan l m r s₁ s₂) --- pbOb w = _ , isSetΣ (isSet× (snd l) (snd r)) --- (uncurry λ x y → isOfHLevelPath 2 (snd m) (s₁ x) (s₂ y)) --- pbPr₁ w = fst ∘ fst --- pbPr₂ w = snd ∘ fst --- pbCommutes w = funExt snd --- fst (fst (univProp w h k H')) d = _ , (H' ≡$ d) --- snd (fst (univProp w h k H')) = refl , refl --- snd (univProp w h k H') y = --- Σ≡Prop --- (λ _ → isProp× (isSet→ (snd l) _ _) (isSet→ (snd r) _ _)) --- (funExt λ x → Σ≡Prop (λ _ → (snd m) _ _) --- λ i → fst (snd y) i x , snd (snd y) i x) - --- module SetLCCC ℓ {X@(_ , isSetX) Y@(_ , isSetY) : hSet ℓ} (f : ⟨ X ⟩ → ⟨ Y ⟩) where --- open BaseChange (SETPullback ℓ) - --- open Cubical.Categories.Adjoint.NaturalBijection --- open _⊣_ - --- open import Cubical.Categories.Instances.Cospan --- open import Cubical.Categories.Limits.Limits - --- Π/ : Functor (SliceCat (SET ℓ) X) (SliceCat (SET ℓ) Y) --- F-ob Π/ (sliceob {S-ob = _ , isSetA} h) = --- sliceob {S-ob = _ , (isSetΣ isSetY $ --- λ y → isSetΠ λ ((x , _) : fiber f y) → --- isOfHLevelFiber 2 isSetA isSetX h x)} fst --- F-hom Π/ {a} {b} (slicehom g p) = --- slicehom (map-snd (map-sndDep (λ q → (p ≡$ _) ∙ q ) ∘_)) refl --- F-id Π/ = SliceHom-≡-intro' _ _ $ --- funExt λ x' → cong ((fst x') ,_) --- (funExt λ y → Σ≡Prop (λ _ → isSetX _ _) refl) --- F-seq Π/ _ _ = SliceHom-≡-intro' _ _ $ --- funExt λ x' → cong ((fst x') ,_) --- (funExt λ y → Σ≡Prop (λ _ → isSetX _ _) refl) - --- f*⊣Π/ : f ＊ ⊣ Π/ --- Iso.fun (adjIso f*⊣Π/) (slicehom h p) = --- slicehom (λ _ → _ , λ (_ , q) → h (_ , q) , (p ≡$ _)) refl --- Iso.inv (adjIso f*⊣Π/) (slicehom h p) = --- slicehom _ $ funExt λ (_ , q) → snd (snd (h _) (_ , q ∙ ((sym p) ≡$ _))) --- Iso.rightInv (adjIso f*⊣Π/) b = SliceHom-≡-intro' _ _ $ --- funExt λ _ → cong₂ _,_ (sym (S-comm b ≡$ _)) --- $ toPathP $ funExt λ _ → --- Σ≡Prop (λ _ → isSetX _ _) $ transportRefl _ ∙ --- cong (fst ∘ snd (S-hom b _)) --- (Σ≡Prop (λ _ → isSetY _ _) $ transportRefl _) --- Iso.leftInv (adjIso f*⊣Π/) a = SliceHom-≡-intro' _ _ $ --- funExt λ _ → cong (S-hom a) $ Σ≡Prop (λ _ → isSetY _ _) refl --- adjNatInD f*⊣Π/ _ _ = SliceHom-≡-intro' _ _ $ --- funExt λ _ → cong₂ _,_ refl $ --- funExt λ _ → Σ≡Prop (λ _ → isSetX _ _) refl --- adjNatInC f*⊣Π/ g h = SliceHom-≡-intro' _ _ $ --- funExt λ _ → cong (fst ∘ (snd (S-hom g (S-hom h _)) ∘ (_ ,_))) $ isSetY _ _ _ _ - --- -- Σ/ : Functor (SliceCat (SET ℓ) X) (SliceCat (SET ℓ) Y) --- -- F-ob Σ/ (sliceob {S-ob = ob} arr) = sliceob {S-ob = ob} (f ∘ arr ) --- -- F-hom Σ/ (slicehom g p) = slicehom _ (cong (f ∘_) p) --- -- F-id Σ/ = refl --- -- F-seq Σ/ _ _ = SliceHom-≡-intro' _ _ $ refl - --- -- Σ/⊣f* : Σ/ ⊣ BaseChangeFunctor --- -- Iso.fun (adjIso Σ/⊣f*) (slicehom g p) = slicehom (λ _ → _ , (sym p ≡$ _ )) refl --- -- Iso.inv (adjIso Σ/⊣f*) (slicehom g p) = slicehom (snd ∘ fst ∘ g) $ --- -- funExt (λ x → sym (snd (g x))) ∙ cong (f ∘_) p --- -- Iso.rightInv (adjIso Σ/⊣f*) (slicehom g p) = --- -- SliceHom-≡-intro' _ _ $ --- -- funExt λ xx → Σ≡Prop (λ _ → isSetY _ _) --- -- (ΣPathP (sym (p ≡$ _) , refl)) --- -- Iso.leftInv (adjIso Σ/⊣f*) _ = SliceHom-≡-intro' _ _ $ refl --- -- adjNatInD Σ/⊣f* _ _ = SliceHom-≡-intro' _ _ $ --- -- funExt λ x → Σ≡Prop (λ _ → isSetY _ _) refl --- -- adjNatInC Σ/⊣f* _ _ = SliceHom-≡-intro' _ _ $ refl - - module _ ℓ where SETOID : Category (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ)) (ℓ-max ℓ ℓ) ob SETOID = Setoid ℓ ℓ @@ -413,9 +330,15 @@ module _ ℓ where open WeakEquivalence open isWeakEquivalence + + -- SET is subcategory of SETOID in two ways: + + -- 1. As as subcategory of SETOIDs with FullRelations + module FullRelationsSubcategory = FullSubcategory SETOID (BinaryRelation.isFull ∘ EquivPropRel→Rel ∘ snd) + FullRelationsSubcategory : Category _ _ FullRelationsSubcategory = FullRelationsSubcategory.FullSubcategory @@ -427,6 +350,8 @@ module _ ℓ where esssurj (isWeakEquiv FullRelationsSubcategory≅SET) d = ∣ (FullRel ⟅ d ⟆ , _) , idCatIso ∣₁ + -- 2. As as subcategory of SETOIDs with Identity relations + module IdRelationsSubcategory = FullSubcategory SETOID (BinaryRelation.impliesIdentity ∘ EquivPropRel→Rel ∘ snd) @@ -446,11 +371,13 @@ module _ ℓ where ∣ (IdRel ⟅ d ⟆ , idfun _) , idCatIso ∣₁ - - + -- base change functor does not have right adjoint (so SETOID cannot be LCCC) + -- implementation of `Setoids are not an LCCC` by Thorsten Altenkirch and Nicolai Kraus + -- (https://www.cs.nott.ac.uk/~psznk/docs/setoids.pdf) open BaseChange pullbacks public + ¬BaseChange⊣SetoidΠ : ({X Y : ob SETOID} (f : SETOID .Hom[_,_] X Y) → Σ (Functor (SliceCat SETOID X) (SliceCat SETOID Y)) (λ Πf → (_＊ {c = X} {d = Y} f) ⊣ Πf)) → ⊥.⊥ @@ -577,7 +504,7 @@ module _ ℓ where Πob-full-rel rr = elim𝟚 Date: Mon, 2 Sep 2024 21:35:06 +0200 Subject: [PATCH 13/17] small fixes --- Cubical/Categories/Constructions/Slice/Functor.agda | 6 +++--- Cubical/Categories/Functor/Properties.agda | 2 +- Cubical/Categories/Instances/Sets.agda | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Cubical/Categories/Constructions/Slice/Functor.agda b/Cubical/Categories/Constructions/Slice/Functor.agda index 1ab6901ff9..aabe059920 100644 --- a/Cubical/Categories/Constructions/Slice/Functor.agda +++ b/Cubical/Categories/Constructions/Slice/Functor.agda @@ -41,7 +41,7 @@ F-seq (F F/ c) _ _ = SliceHom-≡-intro' _ _ $ F-seq F _ _ ∑_ : ∀ {c d} f → Functor (SliceCat C c) (SliceCat C d) -F-ob (∑_ {C = C} f) (sliceob x) = sliceob (_⋆_ C x f) +F-ob (∑_ {C = C} f) (sliceob x) = sliceob (x ⋆⟨ C ⟩ f) F-hom (∑_ {C = C} f) (slicehom h p) = slicehom _ $ sym (C .⋆Assoc _ _ _) ∙ cong (comp' C f) p F-id (∑ f) = SliceHom-≡-intro' _ _ refl @@ -153,7 +153,7 @@ module _ (Pbs : Pullbacks C) where ∙∙ sym (C .⋆Assoc _ _ _)) .fst .snd .fst inv (adjIso L/b⊣R/b) (slicehom f s) = slicehom _ (D .⋆Assoc _ _ _ - ∙∙ congS (_⋆ᵈ (ε ⟦ _ ⟧ ⋆ᵈ _)) (F-seq L _ _) + ∙∙ congS (_⋆ᵈ (ε ⟦ _ ⟧ ⋆⟨ D ⟩ _)) (F-seq L _ _) ∙∙ D .⋆Assoc _ _ _ ∙ cong (L ⟪ f ⟫ ⋆ᵈ_) (cong (L ⟪ pbPr₂ ⟫ ⋆ᵈ_) (sym (N-hom ε _)) ∙∙ sym (D .⋆Assoc _ _ _) @@ -166,7 +166,7 @@ module _ (Pbs : Pullbacks C) where ∙∙ cong (L ⟪_⟫) s) rightInv (adjIso L/b⊣R/b) h = SliceHom-≡-intro' _ _ $ - let p₂ : ∀ {x} → η ⟦ _ ⟧ ⋆ᶜ R ⟪ L ⟪ x ⟫ ⋆ᵈ ε ⟦ _ ⟧ ⟫ ≡ x + let p₂ : ∀ {x} → η ⟦ _ ⟧ ⋆ᶜ R ⟪ L ⟪ x ⟫ ⋆⟨ D ⟩ ε ⟦ _ ⟧ ⟫ ≡ x p₂ = cong (_ ⋆ᶜ_) (F-seq R _ _) ∙ AssocCong₂⋆L C (sym (N-hom η _)) ∙∙ cong (_ ⋆ᶜ_) (Δ₂ _) ∙∙ C .⋆IdR _ diff --git a/Cubical/Categories/Functor/Properties.agda b/Cubical/Categories/Functor/Properties.agda index def27b2477..33f80a0455 100644 --- a/Cubical/Categories/Functor/Properties.agda +++ b/Cubical/Categories/Functor/Properties.agda @@ -123,7 +123,7 @@ isSetFunctor = isOfHLevelFunctor 0 module _ (F : Functor C D) where - -- functors preserve commutative diagrams (specificallysqures here) + -- functors preserve commutative diagrams (specifically squres here) preserveCommF : ∀ {x y z w} {f : C [ x , y ]} {g : C [ y , w ]} {h : C [ x , z ]} {k : C [ z , w ]} → f ⋆⟨ C ⟩ g ≡ h ⋆⟨ C ⟩ k → (F ⟪ f ⟫) ⋆⟨ D ⟩ (F ⟪ g ⟫) ≡ (F ⟪ h ⟫) ⋆⟨ D ⟩ (F ⟪ k ⟫) diff --git a/Cubical/Categories/Instances/Sets.agda b/Cubical/Categories/Instances/Sets.agda index 3084d571c4..a2212ae7ba 100644 --- a/Cubical/Categories/Instances/Sets.agda +++ b/Cubical/Categories/Instances/Sets.agda @@ -213,4 +213,4 @@ module _ {ℓ : Level} where fst (limSetIso J D) cc = lift (lowerCone J D cc) cInv (snd (limSetIso J D)) cc = liftCone J D (cc .lower) sec (snd (limSetIso J D)) = funExt (λ _ → liftExt (cone≡ λ _ → refl)) - ret (snd (limSetIso J D)) = funExt (λ _ → cone≡ λ _ → refl) \ No newline at end of file + ret (snd (limSetIso J D)) = funExt (λ _ → cone≡ λ _ → refl) From cc3264c6d020cc4e25a5c183985da5f6a3b12be3 Mon Sep 17 00:00:00 2001 From: Marcin Grzybowski Date: Mon, 2 Sep 2024 21:50:45 +0200 Subject: [PATCH 14/17] removed unviPropEq, replaced its occurence with existing helper --- .../Constructions/Slice/Functor.agda | 12 +++---- Cubical/Categories/Limits/Pullback.agda | 31 +++++++++---------- 2 files changed, 20 insertions(+), 23 deletions(-) diff --git a/Cubical/Categories/Constructions/Slice/Functor.agda b/Cubical/Categories/Constructions/Slice/Functor.agda index aabe059920..424fa85052 100644 --- a/Cubical/Categories/Constructions/Slice/Functor.agda +++ b/Cubical/Categories/Constructions/Slice/Functor.agda @@ -66,11 +66,11 @@ module _ (Pbs : Pullbacks C) where _＊ : Functor (SliceCat C d) (SliceCat C c) F-ob _＊ x = sliceob (pbPr₁ {x = x}) F-hom _＊ f = slicehom _ (sym (fst (pbU f))) - F-id _＊ = SliceHom-≡-intro' _ _ $ univPropEq (sym (C .⋆IdL _)) (C .⋆IdR _ ∙ sym (C .⋆IdL _)) + F-id _＊ = SliceHom-≡-intro' _ _ $ pullbackArrowUnique (sym (C .⋆IdL _)) (C .⋆IdR _ ∙ sym (C .⋆IdL _)) F-seq _＊ _ _ = let (u₁ , v₁) = pbU _ ; (u₂ , v₂) = pbU _ - in SliceHom-≡-intro' _ _ $ univPropEq + in SliceHom-≡-intro' _ _ $ pullbackArrowUnique (u₂ ∙∙ cong (C ⋆ _) u₁ ∙∙ sym (C .⋆Assoc _ _ _)) (sym (C .⋆Assoc _ _ _) ∙∙ cong (comp' C _) v₂ ∙∙ AssocCong₂⋆R C v₁) @@ -91,14 +91,14 @@ module _ (Pbs : Pullbacks C) where inv (adjIso ∑𝑓⊣𝑓＊) (slicehom h o) = slicehom _ $ AssocCong₂⋆R C (sym (pbCommutes)) ∙ cong (_⋆ᶜ 𝑓) o rightInv (adjIso ∑𝑓⊣𝑓＊) (slicehom h o) = - SliceHom-≡-intro' _ _ (univPropEq (sym o) refl) + SliceHom-≡-intro' _ _ (pullbackArrowUnique (sym o) refl) leftInv (adjIso ∑𝑓⊣𝑓＊) (slicehom h o) = let ((_ , (_ , q)) , _) = univProp _ _ _ in SliceHom-≡-intro' _ _ (sym q) adjNatInD ∑𝑓⊣𝑓＊ f k = SliceHom-≡-intro' _ _ $ let ((h' , (v' , u')) , _) = univProp _ _ _ ((_ , (v'' , u'')) , _) = univProp _ _ _ - in univPropEq (v' ∙∙ cong (h' ⋆ᶜ_) v'' ∙∙ sym (C .⋆Assoc _ _ _)) + in pullbackArrowUnique (v' ∙∙ cong (h' ⋆ᶜ_) v'' ∙∙ sym (C .⋆Assoc _ _ _)) (cong (_⋆ᶜ _) u' ∙ AssocCong₂⋆R C u'') adjNatInC ∑𝑓⊣𝑓＊ g h = SliceHom-≡-intro' _ _ $ C .⋆Assoc _ _ _ @@ -172,7 +172,7 @@ module _ (Pbs : Pullbacks C) where ∙∙ cong (_ ⋆ᶜ_) (Δ₂ _) ∙∙ C .⋆IdR _ - in univPropEq (sym (S-comm h)) p₂ + in pullbackArrowUnique (sym (S-comm h)) p₂ leftInv (adjIso L/b⊣R/b) _ = SliceHom-≡-intro' _ _ $ cong ((_⋆ᵈ _) ∘ L ⟪_⟫) (sym (snd (snd (fst (univProp _ _ _))))) @@ -181,7 +181,7 @@ module _ (Pbs : Pullbacks C) where let (h , (u , v)) = univProp _ _ _ .fst (u' , v') = pbU _ - in univPropEq + in pullbackArrowUnique (u ∙∙ cong (h ⋆ᶜ_) u' ∙∙ sym (C .⋆Assoc h _ _)) (cong (_ ⋆ᶜ_) (F-seq R _ _) ∙∙ sym (C .⋆Assoc _ _ _) ∙∙ diff --git a/Cubical/Categories/Limits/Pullback.agda b/Cubical/Categories/Limits/Pullback.agda index 2236cbcad0..bba4e78f1b 100644 --- a/Cubical/Categories/Limits/Pullback.agda +++ b/Cubical/Categories/Limits/Pullback.agda @@ -53,16 +53,23 @@ module _ (C : Category ℓ ℓ') where pbCommutes : pbPr₁ ⋆ cspn .s₁ ≡ pbPr₂ ⋆ cspn .s₂ univProp : isPullback cspn pbPr₁ pbPr₂ pbCommutes - univPropEq : ∀ {c p₁ p₂ H g} p q → fst (fst (univProp {c} p₁ p₂ H)) ≡ g - univPropEq p q = cong fst (snd (univProp _ _ _) (_ , (p , q))) + pullbackArrow : + {c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ]) + (H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) → C [ c , pbOb ] + pullbackArrow p₁ p₂ H = univProp p₁ p₂ H .fst .fst + + pullbackArrowUnique : + {c : ob} {p₁ : C [ c , cspn .l ]} {p₂ : C [ c , cspn .r ]} + {H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂} + {pbArrow' : C [ c , pbOb ]} + (H₁ : p₁ ≡ pbArrow' ⋆ pbPr₁) (H₂ : p₂ ≡ pbArrow' ⋆ pbPr₂) + → pullbackArrow p₁ p₂ H ≡ pbArrow' + pullbackArrowUnique H₁ H₂ = + cong fst (univProp _ _ _ .snd (_ , (H₁ , H₂))) + open Pullback - pullbackArrow : - {cspn : Cospan} (pb : Pullback cspn) - {c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ]) - (H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) → C [ c , pb . pbOb ] - pullbackArrow pb p₁ p₂ H = pb .univProp p₁ p₂ H .fst .fst pullbackArrowPr₁ : {cspn : Cospan} (pb : Pullback cspn) @@ -78,16 +85,6 @@ module _ (C : Category ℓ ℓ') where p₂ ≡ pullbackArrow pb p₁ p₂ H ⋆ pbPr₂ pb pullbackArrowPr₂ pb p₁ p₂ H = pb .univProp p₁ p₂ H .fst .snd .snd - pullbackArrowUnique : - {cspn : Cospan} (pb : Pullback cspn) - {c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ]) - (H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) - (pbArrow' : C [ c , pb .pbOb ]) - (H₁ : p₁ ≡ pbArrow' ⋆ pbPr₁ pb) (H₂ : p₂ ≡ pbArrow' ⋆ pbPr₂ pb) - → pullbackArrow pb p₁ p₂ H ≡ pbArrow' - pullbackArrowUnique pb p₁ p₂ H pbArrow' H₁ H₂ = - cong fst (pb .univProp p₁ p₂ H .snd (pbArrow' , (H₁ , H₂))) - Pullbacks : Type (ℓ-max ℓ ℓ') Pullbacks = (cspn : Cospan) → Pullback cspn From 96ca9667d7e5b8881c114beeecd3b9fb08a9579c Mon Sep 17 00:00:00 2001 From: Marcin Grzybowski Date: Mon, 2 Sep 2024 21:59:26 +0200 Subject: [PATCH 15/17] added requested comment --- Cubical/Categories/Instances/Sets.agda | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Cubical/Categories/Instances/Sets.agda b/Cubical/Categories/Instances/Sets.agda index a2212ae7ba..7917105ba1 100644 --- a/Cubical/Categories/Instances/Sets.agda +++ b/Cubical/Categories/Instances/Sets.agda @@ -152,6 +152,11 @@ univProp (completeSET J D) c cc = module _ {ℓ} where +-- While pullbacks can be obtained from limits +-- (using `completeSET` & `LimitsOfShapeCospanCat→Pullbacks` from `Cubical.Categories.Limits.Pullback`), +-- this direct construction can be more convenient when only pullbacks are needed. +-- It also has better behavior in terms of inferring implicit arguments + open Pullback PullbacksSET : Pullbacks (SET ℓ) From ac23253ec2c115e3902f4204357875ba9977658b Mon Sep 17 00:00:00 2001 From: MJG Date: Tue, 10 Sep 2024 15:38:18 +0200 Subject: [PATCH 16/17] Update Cat.agda removed unifnished code --- Cubical/Categories/Instances/Cat.agda | 43 --------------------------- 1 file changed, 43 deletions(-) diff --git a/Cubical/Categories/Instances/Cat.agda b/Cubical/Categories/Instances/Cat.agda index 3fa88518b5..845e113a33 100644 --- a/Cubical/Categories/Instances/Cat.agda +++ b/Cubical/Categories/Instances/Cat.agda @@ -35,46 +35,3 @@ module _ (ℓ ℓ' : Level) where ⋆IdR Cat _ = F-rUnit ⋆Assoc Cat _ _ _ = F-assoc isSetHom Cat {y = _ , isSetObY} = isSetFunctor isSetObY - - - -- isUnivalentCat : isUnivalent Cat - -- isUnivalent.univ isUnivalentCat (C , isSmallC) (C' , isSmallC') = - -- {!!} - - -- where - -- w : Iso (CategoryPath C C') (CatIso Cat (C , isSmallC) (C' , isSmallC')) - -- Iso.fun w = pathToIso ∘ Σ≡Prop (λ _ → isPropIsSet) ∘ CategoryPath.mk≡ - -- Iso.inv w (m , isiso inv sec ret) = ww - -- where - -- obIsom : Iso (C .ob) (C' .ob) - -- Iso.fun obIsom = F-ob m - -- Iso.inv obIsom = F-ob inv - -- Iso.rightInv obIsom = cong F-ob sec ≡$_ - -- Iso.leftInv obIsom = cong F-ob ret ≡$_ - - -- homIsom : (x y : C .ob) → - -- Iso (C .Hom[_,_] x y) - -- (C' .Hom[_,_] (fst (isoToEquiv obIsom) x) - -- (fst (isoToEquiv obIsom) y)) - -- Iso.fun (homIsom x y) = F-hom m - -- Iso.inv (homIsom x y) f = - -- subst2 (C [_,_]) (cong F-ob ret ≡$ x) ((cong F-ob ret ≡$ y)) - -- (F-hom inv f) - - -- Iso.rightInv (homIsom x y) b = - -- -- cong (F-hom m) - -- -- (fromPathP {A = (λ i → Hom[ C , F-ob (ret i) x ] (F-ob (ret i) y))} - -- -- {!!}) ∙ - -- {!!} ∙ - -- λ i → (fromPathP (cong F-hom sec)) i b - -- -- {!!} ∙ λ i → {!sec i .F-hom b!} - -- Iso.leftInv (homIsom x y) a = {!!} - - -- open CategoryPath - -- ww : CategoryPath C C' - -- ob≡ ww = ua (isoToEquiv obIsom) - -- Hom≡ ww = RelPathP _ λ x y → isoToEquiv $ homIsom x y - -- id≡ ww = {!!} - -- ⋆≡ ww = {!!} - -- Iso.rightInv w = {!!} - -- Iso.leftInv w = {!!} From d0431e726c2b7c03679ec50a486622eab91a4e6f Mon Sep 17 00:00:00 2001 From: MJG Date: Tue, 10 Sep 2024 16:05:48 +0200 Subject: [PATCH 17/17] Update Setoids.agda fixed dead link --- Cubical/Categories/Instances/Setoids.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Cubical/Categories/Instances/Setoids.agda b/Cubical/Categories/Instances/Setoids.agda index 2dc17f63e3..0c4e980b5d 100644 --- a/Cubical/Categories/Instances/Setoids.agda +++ b/Cubical/Categories/Instances/Setoids.agda @@ -372,8 +372,8 @@ module _ ℓ where -- base change functor does not have right adjoint (so SETOID cannot be LCCC) - -- implementation of `Setoids are not an LCCC` by Thorsten Altenkirch and Nicolai Kraus - -- (https://www.cs.nott.ac.uk/~psznk/docs/setoids.pdf) + -- implementation of `Thorsten Altenkirch and Nicolai Kraus. Setoids are not an LCCC, 2012.` + -- (https://nicolaikraus.github.io/docs/setoids.pdf) open BaseChange pullbacks public