Characterization of Rezk Completion

Cubical/Categories/Functor/Properties.agda

@@ -189,6 +189,17 @@ module _ {F : Functor C D} where
       ∙ isoFf .ret
       ∙ sym (F .F-id))
 
+  -- Lifting isomorphism upwards a fully faithful functor
+
+  module _ (fullfaith : isFullyFaithful F) where
+
+    liftIso : {x y : C .ob} → CatIso D (F .F-ob x) (F .F-ob y) → CatIso C x y
+    liftIso f .fst = invEq (_ , fullfaith _ _) (f .fst)
+    liftIso f .snd = isFullyFaithful→Conservative fullfaith (subst (isIso D) (sym (secEq (_ , fullfaith _ _) (f .fst))) (f .snd))
+
+    liftIso≡ : {x y : C .ob} → (f : CatIso D (F .F-ob x) (F .F-ob y)) → F-Iso {F = F} (liftIso f) ≡ f
+    liftIso≡ f = CatIso≡ _ _ (secEq (_ , fullfaith _ _) (f .fst))
+
 
 -- Functors inducing surjection on objects is essentially surjective
 

Cubical/Categories/Instances/Functors.agda

@@ -66,20 +66,23 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where
   open Iso
   open NatIso
 
-  Iso→NatIso : {F G : Functor C D} → CatIso FUNCTOR F G → NatIso F G
-  Iso→NatIso α .trans = α .fst
-  Iso→NatIso α .nIso = FUNCTORIso' _ (α .snd)
+  FUNCTORIso→NatIso : {F G : Functor C D} → CatIso FUNCTOR F G → NatIso F G
+  FUNCTORIso→NatIso α .trans = α .fst
+  FUNCTORIso→NatIso α .nIso = FUNCTORIso' _ (α .snd)
 
-  Path→Iso→NatIso : {F G : Functor C D} → (p : F ≡ G) → pathToNatIso p ≡ Iso→NatIso (pathToIso p)
-  Path→Iso→NatIso {F = F} p = J (λ _ p → pathToNatIso p ≡ Iso→NatIso (pathToIso p)) (NatIso≡ refl-helper) p
+  NatIso→FUNCTORIso : {F G : Functor C D} → NatIso F G → CatIso FUNCTOR F G
+  NatIso→FUNCTORIso α = α .trans , FUNCTORIso _ (α .nIso)
+
+  Path→FUNCTORIso→NatIso : {F G : Functor C D} → (p : F ≡ G) → pathToNatIso p ≡ FUNCTORIso→NatIso (pathToIso p)
+  Path→FUNCTORIso→NatIso {F = F} p = J (λ _ p → pathToNatIso p ≡ FUNCTORIso→NatIso (pathToIso p)) (NatIso≡ refl-helper) p
     where
     refl-helper : _
     refl-helper i x = ((λ i → pathToIso-refl {C = D} {x = F .F-ob x} i .fst)
       ∙ (λ i → pathToIso-refl {C = FUNCTOR} {x = F} (~ i) .fst .N-ob x)) i
 
   Iso-FUNCTORIso-NatIso : {F G : Functor C D} → Iso (CatIso FUNCTOR F G) (NatIso F G)
-  Iso-FUNCTORIso-NatIso .fun = Iso→NatIso
-  Iso-FUNCTORIso-NatIso .inv α = α .trans , FUNCTORIso _ (α .nIso)
+  Iso-FUNCTORIso-NatIso .fun = FUNCTORIso→NatIso
+  Iso-FUNCTORIso-NatIso .inv = NatIso→FUNCTORIso
   Iso-FUNCTORIso-NatIso .rightInv α i .trans = α .trans
   Iso-FUNCTORIso-NatIso .rightInv α i .nIso =
     isProp→PathP (λ i → isPropΠ (λ _ → isPropIsIso _)) (FUNCTORIso' (α .trans) (FUNCTORIso _ (α .nIso))) (α .nIso) i
@@ -98,4 +101,4 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where
   isUnivalentFUNCTOR : isUnivalent D → isUnivalent FUNCTOR
   isUnivalentFUNCTOR isUnivD .univ _ _ =
     isEquiv[equivFunA≃B∘f]→isEquiv[f] _ FUNCTORIso≃NatIso
-      (subst isEquiv (λ i p → Path→Iso→NatIso p i) (Path≃NatIso isUnivD .snd))
+      (subst isEquiv (λ i p → Path→FUNCTORIso→NatIso p i) (Path≃NatIso isUnivD .snd))

Cubical/Categories/Isomorphism.agda

@@ -19,6 +19,16 @@ module _ {C : Category ℓC ℓC'} where
   open isIso
 
 
+  invIso : {x y : ob} → CatIso C x y → CatIso C y x
+  invIso f .fst = f .snd .inv
+  invIso f .snd .inv = f .fst
+  invIso f .snd .sec = f .snd .ret
+  invIso f .snd .ret = f .snd .sec
+
+  invIsoIdem : {x y : ob} → (f : CatIso C x y) → invIso (invIso f) ≡ f
+  invIsoIdem f = refl
+
+
   ⋆Iso : {x y z : ob} → (f : CatIso C x y)(g : CatIso C y z) → CatIso C x z
   ⋆Iso f g .fst = f .fst ⋆ g .fst
   ⋆Iso f g .snd .inv = g .snd .inv ⋆ f .snd .inv
@@ -43,6 +53,9 @@ module _ {C : Category ℓC ℓC'} where
   ⋆IsoIdR : {x y : ob} → (f : CatIso C x y) → ⋆Iso f idCatIso ≡ f
   ⋆IsoIdR _ = CatIso≡ _ _ (⋆IdR _)
 
+  ⋆IsoInvRev : {x y z : ob} → (f : CatIso C x y)(g : CatIso C y z) → invIso (⋆Iso f g) ≡ ⋆Iso (invIso g) (invIso f)
+  ⋆IsoInvRev _ _ = refl
+
 
   pathToIso-∙ : {x y z : ob}(p : x ≡ y)(q : y ≡ z) → pathToIso (p ∙ q) ≡ ⋆Iso (pathToIso p) (pathToIso q)
   pathToIso-∙ p q = J2 (λ y p z q → pathToIso (p ∙ q) ≡ ⋆Iso (pathToIso p) (pathToIso q)) pathToIso-∙-refl p q
@@ -53,6 +66,11 @@ module _ {C : Category ℓC ℓC'} where
       ∙ (λ i → ⋆Iso (pathToIso-refl (~ i)) (pathToIso refl))
 
 
+  transportPathToIso : {x y z : ob}(f : C [ x , y ])(p : y ≡ z) → PathP (λ i → C [ x , p i ]) f (f ⋆ pathToIso {C = C} p .fst)
+  transportPathToIso {x = x} f = J (λ _ p → PathP (λ i → C [ x , p i ]) f (f ⋆ pathToIso {C = C} p .fst))
+    (sym (⋆IdR _) ∙ cong (λ x → f ⋆ x) (sym (cong fst (pathToIso-refl {C = C}))))
+
+
   pathToIso-Comm : {x y z w : ob}
     → (p : x ≡ y)(q : z ≡ w)
     → (f : Hom[ x , z ])(g : Hom[ y , w ])
@@ -96,6 +114,22 @@ module _ {C : Category ℓC ℓC'} where
 
     open isUnivalent isUnivC
 
+
+    transportIsoToPath : {x y z : ob}(f : C [ x , y ])(p : CatIso C y z)
+      → PathP (λ i → C [ x , CatIsoToPath p i ]) f (f ⋆ p .fst)
+    transportIsoToPath f p i =
+      hcomp (λ j → λ
+        { (i = i0) → f
+        ; (i = i1) → f ⋆ secEq (univEquiv _ _) p j .fst })
+      (transportPathToIso f (CatIsoToPath p) i)
+
+    transportIsoToPathIso : {x y z : ob}(f : CatIso C x y)(p : CatIso C y z)
+      → PathP (λ i → CatIso C x (CatIsoToPath p i)) f (⋆Iso f p)
+    transportIsoToPathIso f p i .fst = transportIsoToPath (f .fst) p i
+    transportIsoToPathIso f p i .snd =
+      isProp→PathP (λ i → isPropIsIso (transportIsoToPath (f .fst) p i)) (f .snd) (⋆Iso f p .snd) i
+
+
     isoToPath-Square : {x y z w : ob}
       → (p : CatIso C x y)(q : CatIso C z w)
       → (f : Hom[ x , z ])(g : Hom[ y , w ])
@@ -106,6 +140,60 @@ module _ {C : Category ℓC ℓC'} where
         ((λ i → f ⋆ secEq (univEquiv _ _) q i .fst) ∙ comm ∙ (λ i → secEq (univEquiv _ _) p (~ i) .fst ⋆ g))
 
 
+module _ {C : Category ℓC ℓC'} where
+
+  open Category C
+  open isIso
+
+  ⋆InvLMove : {x y z : ob}
+    (f : CatIso C x y)
+    {g : Hom[ y , z ]}{h : Hom[ x , z ]}
+    → f .fst ⋆ g ≡ h
+    → g ≡ f .snd .inv ⋆ h
+  ⋆InvLMove f {g = g} p =
+      sym (⋆IdL _)
+    ∙ (λ i → f .snd .sec (~ i) ⋆ g)
+    ∙ ⋆Assoc _ _ _
+    ∙ (λ i → f .snd .inv ⋆ p i)
+
+  ⋆InvRMove : {x y z : ob}
+    (f : CatIso C y z)
+    {g : Hom[ x , y ]}{h : Hom[ x , z ]}
+    → g ⋆ f .fst ≡ h
+    → g ≡ h ⋆ f .snd .inv
+  ⋆InvRMove f {g = g} p =
+      sym (⋆IdR _)
+    ∙ (λ i → g ⋆ f .snd .ret (~ i))
+    ∙ sym (⋆Assoc _ _ _)
+    ∙ (λ i → p i ⋆ f .snd .inv)
+
+  ⋆CancelL : {x y z : ob}
+    (f : CatIso C x y){g h : Hom[ y , z ]}
+    → f .fst ⋆ g ≡ f .fst ⋆ h
+    → g ≡ h
+  ⋆CancelL f {g = g} {h = h} p =
+      sym (⋆IdL _)
+    ∙ (λ i → f .snd .sec (~ i) ⋆ g)
+    ∙ ⋆Assoc _ _ _
+    ∙ (λ i → f .snd .inv ⋆ p i)
+    ∙ sym (⋆Assoc _ _ _)
+    ∙ (λ i → f .snd .sec i ⋆ h)
+    ∙ ⋆IdL _
+
+  ⋆CancelR : {x y z : ob}
+    (f : CatIso C y z){g h : Hom[ x , y ]}
+    → g ⋆ f .fst ≡ h ⋆ f .fst
+    → g ≡ h
+  ⋆CancelR f {g = g} {h = h} p =
+      sym (⋆IdR _)
+    ∙ (λ i → g ⋆ f .snd .ret (~ i))
+    ∙ sym (⋆Assoc _ _ _)
+    ∙ (λ i → p i ⋆ f .snd .inv)
+    ∙ ⋆Assoc _ _ _
+    ∙ (λ i → h ⋆ f .snd .ret i)
+    ∙ ⋆IdR _
+
+
 module _ {C : Category ℓC ℓC'} where
 
   open Category

Cubical/Categories/NaturalTransformation/Base.agda

@@ -94,6 +94,11 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
 
   syntax idTrans F = 1[ F ]
 
+  idNatIso : (F : Functor C D) → NatIso F F
+  idNatIso F .trans = idTrans F
+  idNatIso F .nIso _ = idCatIso .snd
+
+
   -- Natural isomorphism induced by path of functors
 
   pathToNatTrans : {F G : Functor C D} → F ≡ G → NatTrans F G

Cubical/Categories/NaturalTransformation/Properties.agda

@@ -97,7 +97,6 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
   module _ where
     open NatTransP
 
-    -- if the target category has hom Sets, then any natural transformation is a set
     isSetNatTrans : {F G : Functor C D} → isSet (NatTrans F G)
     isSetNatTrans =
       isSetRetract (fun NatTransIsoΣ) (inv NatTransIsoΣ) (leftInv NatTransIsoΣ)

Cubical/Categories/RezkCompletion.agda

@@ -0,0 +1,5 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.RezkCompletion where
+
+open import Cubical.Categories.RezkCompletion.Base public

Cubical/Categories/RezkCompletion/Base.agda

@@ -0,0 +1,44 @@
+{-
+
+The Rezk Completion
+
+-}
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.RezkCompletion.Base where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Functor.ComposeProperty
+open import Cubical.Categories.Equivalence
+open import Cubical.Categories.Equivalence.WeakEquivalence
+open import Cubical.Categories.Instances.Functors
+open import Cubical.Data.Prod
+
+private
+  variable
+    ℓC ℓC' ℓD ℓD' : Level
+    C : Category ℓC ℓC'
+    D : Category ℓD ℓD'
+
+-- Rezk Completion of a given category is the initial functor from it towards univalent categories.
+
+-- It's a bit technical to formulate the universal property of Rezk completion,
+-- because the universal property is naturally universal polymorphic,
+-- and so the predicate is not inside any universe of finite level.
+
+
+isRezkCompletion : (F : Functor C D) → Typeω
+isRezkCompletion {D = D} F =
+      isUnivalent D
+  ×ω ({ℓ ℓ' : Level}{E : Category ℓ ℓ'} → isUnivalent E → isEquivalence (precomposeF E F))
+
+-- The criterion of being Rezk completion, c.f. HoTT Book Chapter 9.9.
+
+open _×ω_
+
+makeIsRezkCompletion : {F : Functor C D} → isUnivalent D → isWeakEquivalence F → isRezkCompletion F
+makeIsRezkCompletion univ w-equiv .fst = univ
+makeIsRezkCompletion univ w-equiv .snd univE = isWeakEquiv→isEquivPrecomp univE _ w-equiv

Cubical/Data/Prod/Base.agda

@@ -49,3 +49,12 @@ map f g = intro (f ∘ proj₁) (g ∘ proj₂)
 
 ×-η : {A : Type ℓ} {B : Type ℓ'} (x : A × B) → x ≡ ((proj₁ x) , (proj₂ x))
 ×-η (x , x₁) = refl
+
+
+-- The product type with one parameter in Typeω
+
+record _×ω_ {a} (A : Type a) (B : Typeω) : Typeω where
+  constructor _,_
+  field
+    fst : A
+    snd : B

Cubical/Foundations/HLevels.agda

@@ -36,6 +36,7 @@ private
     D : (x : A) (y : B x) → C x y → Type ℓ
     E : (x : A) (y : B x) → (z : C x y) → D x y z → Type ℓ
     F : (x : A) (y : B x) (z : C x y) (w : D x y z) (v : E x y z w) → Type ℓ
+    G : (x : A) (y : B x) (z : C x y) (w : D x y z) (v : E x y z w) (u : F x y z w v) → Type ℓ
     w x y z : A
     n : HLevel
 
@@ -433,9 +434,13 @@ isPropΠ4 : (h : (x : A) (y : B x) (z : C x y) (w : D x y z) → isProp (E x y z
 isPropΠ4 h = isPropΠ λ _ → isPropΠ3 (h _)
 
 isPropΠ5 : (h : (x : A) (y : B x) (z : C x y) (w : D x y z) (v : E x y z w) → isProp (F x y z w v))
-            → isProp ((x : A) (y : B x) (z : C x y) (w : D x y z)  (v : E x y z w) → F x y z w v)
+            → isProp ((x : A) (y : B x) (z : C x y) (w : D x y z) (v : E x y z w) → F x y z w v)
 isPropΠ5 h = isPropΠ λ _ → isPropΠ4 (h _)
 
+isPropΠ6 : (h : (x : A) (y : B x) (z : C x y) (w : D x y z) (v : E x y z w) (u : F x y z w v) → isProp (G x y z w v u))
+            → isProp ((x : A) (y : B x) (z : C x y) (w : D x y z) (v : E x y z w) (u : F x y z w v) → G x y z w v u)
+isPropΠ6 h = isPropΠ λ _ → isPropΠ5 (h _)
+
 isPropImplicitΠ : (h : (x : A) → isProp (B x)) → isProp ({x : A} → B x)
 isPropImplicitΠ h f g i {x} = h x (f {x}) (g {x}) i
 

Cubical/HITs/PropositionalTruncation/Properties.agda

@@ -40,6 +40,12 @@ rec2 Pprop f ∣ x ∣₁ ∣ y ∣₁ = f x y
 rec2 Pprop f ∣ x ∣₁ (squash₁ y z i) = Pprop (rec2 Pprop f ∣ x ∣₁ y) (rec2 Pprop f ∣ x ∣₁ z) i
 rec2 Pprop f (squash₁ x y i) z = Pprop (rec2 Pprop f x z) (rec2 Pprop f y z) i
 
+rec3 : {P : Type ℓ} → isProp P → (A → B → C → P) → ∥ A ∥₁ → ∥ B ∥₁ → ∥ C ∥₁ → P
+rec3 Pprop f ∣ x ∣₁ ∣ y ∣₁ ∣ z ∣₁ = f x y z
+rec3 Pprop f ∣ x ∣₁ ∣ y ∣₁ (squash₁ z w i) = Pprop (rec3 Pprop f ∣ x ∣₁ ∣ y ∣₁ z) (rec3 Pprop f ∣ x ∣₁ ∣ y ∣₁ w) i
+rec3 Pprop f ∣ x ∣₁ (squash₁ y z i) w = Pprop (rec3 Pprop f ∣ x ∣₁ y w) (rec3 Pprop f ∣ x ∣₁ z w) i
+rec3 Pprop f (squash₁ x y i) z w = Pprop (rec3 Pprop f x z w) (rec3 Pprop f y z w) i
+
 -- Old version
 -- rec2 : ∀ {P : Type ℓ} → isProp P → (A → A → P) → ∥ A ∥ → ∥ A ∥ → P
 -- rec2 Pprop f = rec (isProp→ Pprop) (λ a → rec Pprop (f a))