(C ≃ᶜ C') ≃ (C ≡ C') & univalent category of setoids

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

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 ℓ ℓ'

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}

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/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