From 92ccbff9f5aa1039ff642a76688a9f978e0a1705 Mon Sep 17 00:00:00 2001 From: Marcin Grzybowski Date: Mon, 4 Dec 2023 20:36:25 +0100 Subject: [PATCH 1/3] 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 2/3] 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 3/3] 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)))