diff --git a/Cubical/Categories/Adjoint.agda b/Cubical/Categories/Adjoint.agda index 5d6c102ac3..6695102064 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 @@ -189,6 +189,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 +235,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 427b17b94f..cfdb1672de 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 @@ -144,8 +144,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 @@ -154,10 +156,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/Category/Properties.agda b/Cubical/Categories/Category/Properties.agda index 0040358578..11a5cf0fb8 100644 --- a/Cubical/Categories/Category/Properties.agda +++ b/Cubical/Categories/Category/Properties.agda @@ -92,26 +92,29 @@ 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 + +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/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/Constructions/Slice/Base.agda b/Cubical/Categories/Constructions/Slice/Base.agda index c11652b7cf..8159d03e81 100644 --- a/Cubical/Categories/Constructions/Slice/Base.agda +++ b/Cubical/Categories/Constructions/Slice/Base.agda @@ -31,6 +31,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 new file mode 100644 index 0000000000..424fa85052 --- /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 (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 +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' _ _ $ pullbackArrowUnique (sym (C .⋆IdL _)) (C .⋆IdR _ ∙ sym (C .⋆IdL _)) + + F-seq _＊ _ _ = + let (u₁ , v₁) = pbU _ ; (u₂ , v₂) = pbU _ + in SliceHom-≡-intro' _ _ $ pullbackArrowUnique + (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' _ _ (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 pullbackArrowUnique (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 (_⋆ᵈ (ε ⟦ _ ⟧ ⋆⟨ D ⟩ _)) (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 ⟫ ⋆⟨ D ⟩ ε ⟦ _ ⟧ ⟫ ≡ x + p₂ = cong (_ ⋆ᶜ_) (F-seq R _ _) ∙ + AssocCong₂⋆L C (sym (N-hom η _)) + ∙∙ cong (_ ⋆ᶜ_) (Δ₂ _) ∙∙ C .⋆IdR _ + + + in pullbackArrowUnique (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 pullbackArrowUnique + (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/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/Functor/Properties.agda b/Cubical/Categories/Functor/Properties.agda index 8bbbb9b8be..33f80a0455 100644 --- a/Cubical/Categories/Functor/Properties.agda +++ b/Cubical/Categories/Functor/Properties.agda @@ -51,20 +51,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') = @@ -131,9 +117,26 @@ isOfHLevelFunctor {D = D} {C = C} hLevel x _ _ = λ _ → isOfHLevelPlus' 1 (isPropImplicitΠ2 λ _ _ → isPropΠ λ _ → isOfHLevelPathP' 1 (λ _ _ → D .isSetHom _ _) _ _ )) + isSetFunctor : isSet (D .ob) → isSet (Functor C D) isSetFunctor = isOfHLevelFunctor 0 +module _ (F : Functor C D) where + + -- 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 ⟫) + 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, -- the morphism f is itself isomorphism. diff --git a/Cubical/Categories/Instances/Cat.agda b/Cubical/Categories/Instances/Cat.agda new file mode 100644 index 0000000000..845e113a33 --- /dev/null +++ b/Cubical/Categories/Instances/Cat.agda @@ -0,0 +1,37 @@ +-- 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 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 new file mode 100644 index 0000000000..0c4e980b5d --- /dev/null +++ b/Cubical/Categories/Instances/Setoids.agda @@ -0,0 +1,540 @@ +{-# OPTIONS --safe #-} + +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 +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 +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 +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 + +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 + +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 ) + + 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 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 + + + -- 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 + 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 + + + -- 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 + + 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 ∣₁ + + -- 2. As as subcategory of SETOIDs with Identity relations + + 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 ∣₁ + + + -- base change functor does not have right adjoint (so SETOID cannot be LCCC) + -- implementation of `Thorsten Altenkirch and Nicolai Kraus. Setoids are not an LCCC, 2012.` + -- (https://nicolaikraus.github.io/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)) → ⊥.⊥ + ¬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} {𝟚/}) + + + + 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𝟚