Univalent Category of SETOIDs , Setoids are not LCCC

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

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

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 _ _ _)

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

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

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

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 _ _ _
+