(C ≃ᶜ C') ≃ (C ≡ C') for univalent categories

Cubical/Categories/Category/Base.agda

@@ -38,6 +38,10 @@ open Category
 _[_,_] : (C : Category ℓ ℓ') → (x y : C .ob) → Type ℓ'
 _[_,_] = Hom[_,_]
 
+_End[_] : (C : Category ℓ ℓ') → (x : C .ob) → Type ℓ'
+C End[ x ] = C [ x , x ]
+
+
 -- Needed to define this in order to be able to make the subsequence syntax declaration
 seq' : ∀ (C : Category ℓ ℓ') {x y z} (f : C [ x , y ]) (g : C [ y , z ]) → C [ x , z ]
 seq' = _⋆_
@@ -124,6 +128,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,142 @@
+{-
+
+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
+ no-eta-equality
+ 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
+ ob≡ (Iso.leftInv CategoryPathIso a i) = ob≡ a
+ Hom≡ (Iso.leftInv CategoryPathIso a i) = Hom≡ a
+ id≡ (Iso.leftInv CategoryPathIso a i) = id≡ a
+ ⋆≡ (Iso.leftInv CategoryPathIso a i) = ⋆≡ a
+
+ CategoryPath≡ : (cp cp' : CategoryPath C C') →
+     (p≡ : ob≡ cp ≡ ob≡ cp') →
+     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' 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' 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/Equivalence/AdjointEquivalence.agda

@@ -8,6 +8,9 @@ open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
 open import Cubical.Categories.NaturalTransformation
 
+open import Cubical.Categories.Equivalence.Base
+open import Cubical.HITs.PropositionalTruncation
+
 module Cubical.Categories.Equivalence.AdjointEquivalence
   {ℓC ℓ'C : Level} {ℓD ℓ'D : Level}
   where
@@ -72,6 +75,11 @@ module _ (C : Category ℓC ℓ'C) (D : Category ℓD ℓ'D) where
       η : 𝟙⟨ C ⟩ ≅ᶜ inv ∘F fun
       ε : fun ∘F inv ≅ᶜ 𝟙⟨ D ⟩
       triangleIdentities : TriangleIdentities fun inv (NatIso.trans η) (NatIso.trans ε)
+
+    to≃ᶜ : C ≃ᶜ D
+    _≃ᶜ_.func to≃ᶜ = fun
+    _≃ᶜ_.isEquiv to≃ᶜ = ∣ record { invFunc = inv ; η = η ; ε = ε } ∣₁
+
 module _
   {C : Category ℓC ℓ'C} {D : Category ℓD ℓ'D}
   (adj-equiv : AdjointEquivalence C D)

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

Cubical/Categories/Equivalence/WeakEquivalence.agda

@@ -9,11 +9,24 @@ module Cubical.Categories.Equivalence.WeakEquivalence where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
-  renaming (isEquiv to isEquivMap)
+  renaming (isEquiv to isEquivMap ; equivFun to _≃$_)
+open import Cubical.Foundations.Function renaming (_∘_ to _∘f_)
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.HLevels
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.Foundations.Transport hiding (pathToIso)
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.Data.Sigma
+
+open import Cubical.Relation.Binary
+
 open import Cubical.Functions.Surjection
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Equivalence
+open import Cubical.Categories.Category.Path
+
 
 private
   variable
@@ -37,6 +50,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,13 +59,30 @@ 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₁))
 
 -- Equivalence is always weak equivalence.
 
 isEquiv→isWeakEquiv : isEquivalence F → isWeakEquivalence F
 isEquiv→isWeakEquiv isequiv .fullfaith = isEquiv→FullyFaithful isequiv
 isEquiv→isWeakEquiv isequiv .esssurj   = isEquiv→Surj isequiv
 
+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
+
 
 -- Weak equivalence between univalent categories is equivalence,
 -- in other words, they admit explicit inverse functor.
@@ -71,3 +102,101 @@ 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 _ {F : Functor C C'} (we : isWeakEquivalence F) where
+
+  open Category
+
+  ob≃ : C .ob ≃ C' .ob
+  ob≃ = _ , isEquivF-ob isUnivC isUnivC' we
+
+  Hom≃ : ∀ x y → C [ x , y ] ≃ C' [ ob≃ ≃$ x , ob≃ ≃$ y ]
+  Hom≃ _ _ = F-hom F , fullfaith we _ _
+
+  HomPathP : PathP (λ i → ua ob≃ i → ua ob≃ i → Type ℓC')
+               (C [_,_]) (C' [_,_])
+  HomPathP = RelPathP _ Hom≃
+
+  WeakEquivlance→CategoryPath : CategoryPath C C'
+  ob≡ WeakEquivlance→CategoryPath = ua ob≃
+  Hom≡ WeakEquivlance→CategoryPath = HomPathP
+  id≡ WeakEquivlance→CategoryPath = EquivJRel {_∻_ = C' [_,_]}
+    (λ 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 {_} {C' [_,_]} 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 {_∻_ = C' [_,_]}
+    (λ 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≡
+   (WeakEquivlance→CategoryPath (isWeakEquiv (≡→WeakEquivlance (mk≡ b)))) b
+   (λ i j → Glue (C' .Category.ob) {φ = ~ j ∨ j ∨ i}
+         (λ _ → _ , equivPathP
+         {e = ob≃ (isWeakEquiv (≡→WeakEquivlance (mk≡ b)))} {f = idEquiv _}
+         (transport-fillerExt⁻ (ob≡ b)) j))
+    λ i j x y → Glue (C' [ unglue (~ j ∨ j ∨ i) x , unglue (~ j ∨ j ∨ i) y ])
+        λ {(j = i0) → _ , Hom≃ (isWeakEquiv (≡→WeakEquivlance (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))
+                (λ _ _ → fullfaith (isWeakEquiv (≡→WeakEquivlance (mk≡ b))) _ _)
+                (λ _ _ → idIsEquiv _) 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') _ _)