From 5a92d3c12ff9a5fe95d4c980747c9afe6daa40e8 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sun, 16 Feb 2025 17:53:19 +0530
Subject: [PATCH 1/9] Add Rezk Completion by HIT

---
 .../RezkCompletion/Construction.agda          | 410 +++++++++++++++++-
 1 file changed, 406 insertions(+), 4 deletions(-)

diff --git a/Cubical/Categories/RezkCompletion/Construction.agda b/Cubical/Categories/RezkCompletion/Construction.agda
index 26f420355..4d73994ad 100644
--- a/Cubical/Categories/RezkCompletion/Construction.agda
+++ b/Cubical/Categories/RezkCompletion/Construction.agda
@@ -8,6 +8,17 @@ The Construction of Rezk Completion
 module Cubical.Categories.RezkCompletion.Construction where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Transport hiding (pathToIso)
+open import Cubical.Foundations.Isomorphism using (isoToPath; Iso; isoToIsEquiv; iso)
+open import Cubical.Foundations.Univalence using (uaβ)
+open import Cubical.Foundations.Equiv.Base
+open import Cubical.Functions.FunExtEquiv
+open import Cubical.Functions.Surjection
+open import Cubical.HITs.PropositionalTruncation using (∥_∥₁; ∣_∣₁; isPropPropTrunc)
 
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
@@ -15,12 +26,13 @@ open import Cubical.Categories.Equivalence.WeakEquivalence
 open import Cubical.Categories.Constructions.EssentialImage
 open import Cubical.Categories.Presheaf.Base
 open import Cubical.Categories.Yoneda
+open import Cubical.Categories.Isomorphism
 
 open import Cubical.Categories.RezkCompletion.Base
 
-private
-  variable
-    ℓ ℓ' : Level
+private variable
+  ℓ ℓ' ℓ'' ℓ''' : Level
+  A B C D : Type ℓ
 
 open isWeakEquivalence
 
@@ -61,5 +73,395 @@ module RezkByYoneda (C : Category ℓ ℓ) where
 {- The Construction by Higher Inductive Type -}
 
 module RezkByHIT (C : Category ℓ ℓ') where
+  module C = Category C
+  open Category hiding (_∘_)
+  open isUnivalent
+  open Functor
+  open isIso
+  
+  private variable
+    x y z w : ob C
 
-  -- TODO: Write the HIT construction of Rezk completion here.
+  data RezkOb : Type (ℓ-max ℓ ℓ') where
+    inc : ob C → RezkOb
+    inc-ua : (f : CatIso C x y) → inc x ≡ inc y
+    inc-sq : (f : CatIso C x y) (g : CatIso C y z)
+           → Square (inc-ua f) (inc-ua (⋆Iso f g)) refl (inc-ua g)
+    squash : isGroupoid RezkOb
+
+  module _ {P : RezkOb → Type ℓ''}
+    (P-Grpd : ∀ x → isGroupoid (P x))
+    (P-inc : ∀ x → P (inc x))
+    (P-inc-ua : ∀ {x y} f → PathP (λ i → P (inc-ua f i)) (P-inc x) (P-inc y))
+    (P-inc-sq : ∀ {x y z} f g → SquareP (λ i j → P (inc-sq {x = x} {y} {z} f g i j))
+        (P-inc-ua f) (P-inc-ua (⋆Iso f g)) refl (P-inc-ua g))
+    where
+
+    elim : ∀ x → P x
+    elim (inc x) = P-inc x
+    elim (inc-ua f i) = P-inc-ua f i
+    elim (inc-sq f g i j) = P-inc-sq f g i j
+    elim (squash x y p q r s i j k) =
+      isOfHLevel→isOfHLevelDep 3 P-Grpd _ _ _ _ (cong (cong elim) r) (cong (cong elim) s) (squash x y p q r s) i j k
+
+  module _ {P : RezkOb → Type ℓ''}
+    (P-Set : ∀ x → isSet (P x))
+    (P-inc : ∀ x → P (inc x))
+    (P-inc-ua : ∀ {x y} f → PathP (λ i → P (inc-ua f i)) (P-inc x) (P-inc y))
+    where
+
+    elimSet : ∀ x → P x
+    elimSet = elim (λ x → isSet→isGroupoid (P-Set x)) P-inc P-inc-ua λ f g → isSet→SquareP (λ i j → P-Set (inc-sq f g i j)) _ _ _ _
+
+  module _ {P : RezkOb → Type ℓ''}
+    (P-Prop : ∀ x → isProp (P x))
+    (P-inc : ∀ x → P (inc x))
+    where
+
+    elimProp : ∀ x → P x
+    elimProp = elimSet (λ x → isProp→isSet (P-Prop x)) P-inc λ f → isProp→PathP (λ i → P-Prop (inc-ua f i)) _ _
+
+  module _ {P : RezkOb → RezkOb → Type ℓ''}
+    (P-Set : ∀ x y → isSet (P x y))
+    (P-inc : ∀ x y → P (inc x) (inc y))
+    (P-inc-ua : ∀ {x y z} f
+              → PathP (λ i → P (inc x) (inc-ua f i)) (P-inc x y) (P-inc x z))
+    (P-ua-inc : ∀ {x y z} f
+              → PathP (λ i → P (inc-ua f i) (inc z)) (P-inc x z) (P-inc y z))
+    where
+
+    elimSet₂ : ∀ x y → P x y
+    elimSet₂ = elimSet (λ x → isSetΠ (P-Set x)) (λ x → elimSet (P-Set (inc x)) (P-inc x) P-inc-ua) λ f →
+      funExt (elimProp (λ x → isOfHLevelPathP' 1 (P-Set _ _) _ _) λ x → P-ua-inc f)
+
+  module _ {P : RezkOb → RezkOb → Type ℓ''}
+    (P-Prop : ∀ x y → isProp (P x y))
+    (P-inc : ∀ x y → P (inc x) (inc y))
+    where
+
+    elimProp₂ : ∀ x y → P x y
+    elimProp₂ = elimProp (λ x → isPropΠ (P-Prop x)) λ x → elimProp (P-Prop (inc x)) (P-inc x)
+
+  module _ {P : RezkOb → RezkOb → RezkOb → Type ℓ''}
+    (P-Set : ∀ x y z → isSet (P x y z))
+    (P-inc : ∀ x y z → P (inc x) (inc y) (inc z))
+    (P-ua₁ : ∀ {x y z w} f
+           → PathP (λ i → P (inc x) (inc y) (inc-ua f i)) (P-inc x y z) (P-inc x y w))
+    (P-ua₂ : ∀ {x y z w} f
+           → PathP (λ i → P (inc x) (inc-ua f i) (inc w)) (P-inc x y w) (P-inc x z w))
+    (P-ua₃ : ∀ {x y z w} f
+           → PathP (λ i → P (inc-ua f i) (inc z) (inc w)) (P-inc x z w) (P-inc y z w))
+    where
+
+    elimSet₃ : ∀ x y z → P x y z
+    elimSet₃ = elimSet (λ x → isSetΠ2 (P-Set x)) (λ x → elimSet₂ (P-Set (inc x)) (P-inc x) P-ua₁ P-ua₂) λ f → funExt₂ $
+      elimProp₂ (λ x y → isOfHLevelPathP' 1 (P-Set _ _ _) _ _) λ x y → P-ua₃ f
+
+  module _ {P : Type ℓ''}
+    (P-Grpd : isGroupoid P)
+    (P-inc : ob C → P)
+    (P-inc-ua : ∀ {x y} → CatIso C x y → P-inc x ≡ P-inc y)
+    (P-inc-sq : ∀ {x y z} (f : CatIso C x y) (g : CatIso C y z)
+      → Square (P-inc-ua f) (P-inc-ua (⋆Iso f g)) refl (P-inc-ua g))
+    where
+
+    rec : RezkOb → P
+    rec = elim (λ _ → P-Grpd) P-inc P-inc-ua P-inc-sq
+
+  module _ {P : Type ℓ''}
+    (P-Grpd : isGroupoid P)
+    (P-inc : ob C → ob C → P)
+    (P-inc-ua : ∀ {x y z} → CatIso C y z → P-inc x y ≡ P-inc x z)
+    (P-ua-inc : ∀ {x y z} → CatIso C x y → P-inc x z ≡ P-inc y z)
+    (P-ua-inc-ua : ∀ {x y z w} (g : CatIso C z w) (f : CatIso C x y)
+      → Square (P-ua-inc g) (P-ua-inc g) (P-inc-ua f) (P-inc-ua f))
+    (P-inc-sq : ∀ {x y z w} (f : CatIso C y z) (g : CatIso C z w)
+      → Square (P-inc-ua {x = x} f) (P-inc-ua (⋆Iso f g)) refl (P-inc-ua g))
+    (P-sq-inc : ∀ {x y z w} (f : CatIso C x y) (g : CatIso C y z)
+      → Square (P-ua-inc {z = w} f) (P-ua-inc (⋆Iso f g)) refl (P-ua-inc g))
+    where
+
+    rec₂ : RezkOb → RezkOb → P
+    rec₂ = rec (isGroupoidΠ λ _ → P-Grpd)
+      (λ x → rec P-Grpd (P-inc x) P-inc-ua P-inc-sq)
+      (λ f → funExt (elimSet (λ _ → P-Grpd _ _) (λ _ → P-ua-inc f) (P-ua-inc-ua f)))
+      (λ f g → congP (λ _ → funExt) (funExt (elimProp (λ x → isOfHLevelPathP' 1 (P-Grpd _ _) _ _) λ x → P-sq-inc f g)))
+
+  module _ (P : Category ℓ'' ℓ''') (P-univ : isUnivalent P) (P-inc : Functor C P)
+    where
+
+    recCat : RezkOb → ob P
+    recCat = rec (isGroupoid-ob P-univ) (P-inc .F-ob)
+                 (CatIsoToPath P-univ ∘ F-Iso {F = P-inc}) λ f g →
+      congP (λ _ → CatIsoToPath P-univ) $
+        subst⁻ (PathP _ (F-Iso {F = P-inc} f)) (F-Iso-Pres⋆ f g) $
+          transportIsoToPathIso P-univ _ _
+
+  inc-⋆ : (f : CatIso C x y) (g : CatIso C y z)
+        → inc-ua (⋆Iso f g) ≡ inc-ua f ∙ inc-ua g
+  inc-⋆ f g = sym (Square≃doubleComp _ _ _ _ .fst (inc-sq f g))
+
+  inc-id : inc-ua (idCatIso {x = x}) ≡ refl
+  inc-id = 
+    incId ≡⟨ sym (compPathr-cancel (sym incId) incId) ⟩
+    (incId ∙ incId) ∙ sym incId ≡⟨ congL _∙_ (sym (inc-⋆ idCatIso idCatIso)) ⟩
+    inc-ua (⋆Iso idCatIso idCatIso) ∙ sym incId ≡⟨ congL _∙_ (cong inc-ua (⋆IsoIdL _)) ⟩
+    incId ∙ sym incId ≡⟨ rCancel incId ⟩
+    refl ∎
+    where incId = inc-ua idCatIso
+
+  inc-inv : (f : CatIso C x y) → inc-ua (invIso f) ≡ sym (inc-ua f)
+  inc-inv f = 
+    inc-ua (invIso f) ≡⟨ sym (compPathr-cancel (sym (inc-ua f)) (inc-ua (invIso f))) ⟩
+    (inc-ua (invIso f) ∙ inc-ua f) ∙ sym (inc-ua f) ≡⟨ congL _∙_ (sym (inc-⋆ (invIso f) f)) ⟩
+    inc-ua (⋆Iso (invIso f) f) ∙ sym (inc-ua f) ≡⟨ congL _∙_ (cong inc-ua (CatIso≡ _ _ (f .snd .sec))) ⟩
+    inc-ua idCatIso ∙ sym (inc-ua f) ≡⟨ congL _∙_ inc-id ⟩
+    refl ∙ sym (inc-ua f) ≡⟨ sym (lUnit (sym (inc-ua f))) ⟩
+    sym (inc-ua f) ∎
+
+  inc-pathToIso : (p : x ≡ y) → inc-ua (pathToIso p) ≡ cong inc p
+  inc-pathToIso = lemma _ where
+    lemma : ∀ y (p : x ≡ y) → inc-ua (pathToIso p) ≡ cong inc p
+    lemma = J> cong inc-ua pathToIso-refl ∙ inc-id
+
+  inc-surj : isSurjection inc
+  inc-surj = elimProp (λ x → isPropPropTrunc) λ x → ∣ x , refl ∣₁
+
+  RezkHomSet : RezkOb → RezkOb → hSet ℓ'
+  RezkHomSet =
+    rec₂ isGroupoidHSet H-inc H-inc-ua H-ua-inc H-ua-inc-ua H-inc-sq H-sq-inc where
+
+    H-inc : ob C → ob C → hSet ℓ'
+    H-inc x y = C [ x , y ] , C .isSetHom
+
+    H-inc-ua : ∀ {x y z} → CatIso C y z → H-inc x y ≡ H-inc x z
+    H-inc-ua f = TypeOfHLevel≡ 2 $ isoToPath λ where
+      .Iso.fun → C._⋆ f .fst
+      .Iso.inv → C._⋆ f .snd .inv
+      .Iso.rightInv _ → C.⋆Assoc _ _ _ ∙∙ congR C._⋆_ (f .snd .sec) ∙∙ C.⋆IdR _
+      .Iso.leftInv  _ → C.⋆Assoc _ _ _ ∙∙ congR C._⋆_ (f .snd .ret) ∙∙ C.⋆IdR _
+
+    H-ua-inc : ∀ {x y z} → CatIso C x y → H-inc x z ≡ H-inc y z
+    H-ua-inc f = TypeOfHLevel≡ 2 $ isoToPath λ where
+      .Iso.fun → f .snd .inv C.⋆_
+      .Iso.inv → f .fst C.⋆_
+      .Iso.rightInv _ → sym (C.⋆Assoc _ _ _) ∙∙ congL C._⋆_ (f .snd .sec) ∙∙ C.⋆IdL _
+      .Iso.leftInv  _ → sym (C.⋆Assoc _ _ _) ∙∙ congL C._⋆_ (f .snd .ret) ∙∙ C.⋆IdL _
+
+    typeSquare : ∀ {A B C D : Type ℓ''} {P : A ≡ B} {Q : C ≡ D} {R S}
+               → (∀ x → transport S (transport P x) ≡ transport Q (transport R x))
+               → Square P Q R S
+    typeSquare h = compPath→Square $ isInjectiveTransport $ funExt λ x →
+      transportComposite _ _ x ∙∙ sym (h x) ∙∙ sym (transportComposite _ _ x)
+
+    H-ua-inc-ua : ∀ {x y z w} (g : CatIso C z w) (f : CatIso C x y)
+                → Square (H-ua-inc g) (H-ua-inc g) (H-inc-ua f) (H-inc-ua f)
+    H-ua-inc-ua g f = ΣSquareSet (λ _ → isProp→isSet isPropIsSet) $ typeSquare λ h →
+      transport (cong fst (H-inc-ua f)) (transport (cong fst (H-ua-inc g)) h)
+        ≡⟨ uaβ _ _ ⟩
+      transport (cong fst (H-ua-inc g)) h C.⋆ f .fst
+        ≡⟨ congL C._⋆_ (uaβ _ _) ⟩
+      (g .snd .inv C.⋆ h) C.⋆ f .fst
+        ≡⟨ C.⋆Assoc (g .snd .inv) h (f .fst) ⟩
+      g .snd .inv C.⋆ (h C.⋆ f .fst)
+        ≡⟨ congR C._⋆_ (sym (uaβ _ _)) ⟩
+      g .snd .inv C.⋆ (transport (cong fst (H-inc-ua f)) h)
+        ≡⟨ sym (uaβ _ _) ⟩
+      transport (cong fst (H-ua-inc g)) (transport (cong fst (H-inc-ua f)) h) ∎
+    
+    H-inc-sq : ∀ {x y z w} (f : CatIso C y z) (g : CatIso C z w)
+             → Square (H-inc-ua {x = x} f) (H-inc-ua (⋆Iso f g)) refl (H-inc-ua g)
+    H-inc-sq f g = ΣSquareSet (λ _ → isProp→isSet isPropIsSet) $ typeSquare λ h →
+      transport (cong fst (H-inc-ua g)) (transport (cong fst (H-inc-ua f)) h)
+        ≡⟨ uaβ _ _ ⟩
+      transport (cong fst (H-inc-ua f)) h C.⋆ g .fst
+        ≡⟨ congL C._⋆_ (uaβ _ _) ⟩
+      (h C.⋆ f .fst) C.⋆ g .fst
+        ≡⟨ C.⋆Assoc _ _ _ ⟩
+      h C.⋆ (f .fst C.⋆ g .fst)
+        ≡⟨ congL C._⋆_ (sym (transportRefl h)) ⟩
+      transport refl h C.⋆ (f .fst C.⋆ g .fst)
+        ≡⟨ sym (uaβ _ _) ⟩
+      transport (cong fst (H-inc-ua (⋆Iso f g))) (transport refl h) ∎
+    
+    H-sq-inc : ∀ {x y z w} (f : CatIso C x y) (g : CatIso C y z)
+             → Square (H-ua-inc {z = w} f) (H-ua-inc (⋆Iso f g)) refl (H-ua-inc g)
+    H-sq-inc f g = ΣSquareSet (λ _ → isProp→isSet isPropIsSet) $ typeSquare λ h →
+      transport (cong fst (H-ua-inc g)) (transport (cong fst (H-ua-inc f)) h)
+        ≡⟨ uaβ _ _ ⟩
+      g .snd .inv C.⋆ transport (cong fst (H-ua-inc f)) h
+        ≡⟨ congR C._⋆_ (uaβ _ _) ⟩
+      g .snd .inv C.⋆ (f .snd .inv C.⋆ h)
+        ≡⟨ sym (C.⋆Assoc _ _ _) ⟩
+      (g .snd .inv C.⋆ f .snd .inv) C.⋆ h
+        ≡⟨ congR C._⋆_ (sym (transportRefl h)) ⟩
+      (g .snd .inv C.⋆ f .snd .inv) C.⋆ transport refl h
+        ≡⟨ sym (uaβ _ _) ⟩
+      transport (cong fst (H-ua-inc (⋆Iso f g))) (transport refl h) ∎
+    
+  RezkHom : RezkOb → RezkOb → Type ℓ'
+  RezkHom x y = RezkHomSet x y .fst
+
+  isSetRezkHom : ∀ x y → isSet (RezkHom x y)
+  isSetRezkHom x y = RezkHomSet x y .snd
+
+  private
+    tr : transport refl ≡ idfun A
+    tr = funExt transportRefl
+
+  RezkId : ∀ x → RezkHom x x
+  RezkId = elimSet (λ x → isSetRezkHom x x) (λ x → C.id) λ f → toPathP $
+    subst2 RezkHom (inc-ua f) (inc-ua f) C.id
+      ≡[ i ]⟨ tr i (tr i (tr i (tr i (f .snd .inv C.⋆ tr i (tr i (tr i (tr i C.id)) C.⋆ f .fst))))) ⟩
+    f .snd .inv C.⋆ (C.id C.⋆ f .fst)
+      ≡⟨ congR C._⋆_ (C.⋆IdL _) ⟩
+    f .snd .inv C.⋆ f .fst
+      ≡⟨ f .snd .sec ⟩
+    C.id ∎
+
+  Rezk⋆ : ∀ x y z → RezkHom x y → RezkHom y z → RezkHom x z
+  Rezk⋆ = elimSet₃ (λ x y z → isSet→ (isSet→ (isSetRezkHom x z))) (λ x y z → C._⋆_)
+    lem₁ lem₂ lem₃ where
+
+    lem₁ : ∀ {x y z w} (f : Σ C.Hom[ z , w ] (isIso C))
+         → PathP (λ i → RezkHom (inc x) (inc y) →
+             RezkHom (inc y) (inc-ua f i) → RezkHom (inc x) (inc-ua f i)) C._⋆_ C._⋆_
+    lem₁ e = funExt λ f → toPathP $ funExt λ g →
+      transport refl ((f C.⋆ (transport refl g C.⋆ e .snd .inv)) C.⋆ e .fst)
+        ≡⟨ transportRefl _ ⟩
+      (f C.⋆ transport refl g C.⋆ e .snd .inv) C.⋆ e .fst
+        ≡⟨ C.⋆Assoc _ _ _ ⟩
+      f C.⋆ (transport refl g C.⋆ e .snd .inv) C.⋆ e .fst
+        ≡⟨ congR C._⋆_ (
+          (transport refl g C.⋆ e .snd .inv) C.⋆ e .fst
+            ≡⟨ C.⋆Assoc _ _ _ ⟩
+          transport refl g C.⋆ e. snd .inv C.⋆ e .fst
+            ≡⟨ cong₂ C._⋆_ (transportRefl g) (e .snd .sec) ⟩
+          g C.⋆ C.id
+            ≡⟨ C.⋆IdR _ ⟩
+          g ∎
+        ) ⟩
+      f C.⋆ g ∎
+
+    lem₂ : ∀ {x y z w} (f : Σ C.Hom[ y , z ] (isIso C))
+         → PathP (λ i → RezkHom (inc x) (inc-ua f i) →
+             RezkHom (inc-ua f i) (inc w) → RezkHom (inc x) (inc w)) C._⋆_ C._⋆_
+    lem₂ e = toPathP $ funExt₂ λ f g →
+      tr i0 ((tr i0 f C.⋆ e .snd .inv) C.⋆ e .fst C.⋆ tr i0 g)
+        ≡[ i ]⟨ tr i ((tr i f C.⋆ e .snd .inv) C.⋆ e .fst C.⋆ tr i g) ⟩
+      (f C.⋆ e .snd .inv) C.⋆ e .fst C.⋆ g
+        ≡⟨ C.⋆Assoc _ _ _ ⟩
+      f C.⋆ (e .snd .inv C.⋆ e .fst C.⋆ g)
+        ≡⟨ congR C._⋆_ (sym (C.⋆Assoc _ _ _) ∙ congL C._⋆_ (e .snd .sec) ∙ C.⋆IdL _) ⟩
+      f C.⋆ g ∎
+
+    lem₃ : ∀ {x y z w} (f : Σ C.Hom[ x , y ] (isIso C))
+         → PathP (λ i → RezkHom (inc-ua f i) (inc z) →
+             RezkHom (inc z) (inc w) → RezkHom (inc-ua f i) (inc w)) C._⋆_ C._⋆_
+    lem₃ e = toPathP $ funExt₂ λ f g →
+      tr i0 (e .snd .inv C.⋆ (e .fst C.⋆ tr i0 f) C.⋆ tr i0 g)
+        ≡[ i ]⟨ tr i (e .snd .inv C.⋆ (e .fst C.⋆ tr i f) C.⋆ tr i g) ⟩
+      e .snd .inv C.⋆ (e .fst C.⋆ f) C.⋆ g
+        ≡⟨ sym (C.⋆Assoc _ _ _) ⟩
+      (e .snd .inv C.⋆ e .fst C.⋆ f) C.⋆ g
+        ≡⟨ congL C._⋆_ (sym (C.⋆Assoc _ _ _) ∙ congL C._⋆_ (e .snd .sec) ∙ C.⋆IdL _) ⟩
+      f C.⋆ g ∎
+
+  Rezk⋆IdL : ∀ x y f → Rezk⋆ x x y (RezkId x) f ≡ f
+  Rezk⋆IdL = elimProp₂ (λ x y → isPropΠ (λ _ → isSetRezkHom x y _ _)) λ x y → C.⋆IdL
+
+  Rezk⋆IdR : ∀ x y f → Rezk⋆ x y y f (RezkId y) ≡ f
+  Rezk⋆IdR = elimProp₂ (λ x y → isPropΠ (λ _ → isSetRezkHom x y _ _)) λ x y → C.⋆IdR
+
+  Rezk⋆Assoc : ∀ x y z w f g h
+             → Rezk⋆ x z w (Rezk⋆ x y z f g) h ≡ Rezk⋆ x y w f (Rezk⋆ y z w g h)
+  Rezk⋆Assoc = elimProp₂ (λ x y → isPropΠ5 λ z w _ _ _ → isSetRezkHom x w _ _) λ x y →
+    elimProp₂ (λ z w → isPropΠ3 λ _ _ _ → isSetRezkHom (inc x) w _ _) λ z w → C.⋆Assoc
+
+  Rezk : Category (ℓ-max ℓ ℓ') ℓ'
+  Rezk .ob = RezkOb
+  Rezk .Hom[_,_] = RezkHom
+  Rezk .id {x} = RezkId x
+  Rezk ._⋆_ {x} {y} {z} = Rezk⋆ x y z
+  Rezk .⋆IdL {x} {y} = Rezk⋆IdL x y
+  Rezk .⋆IdR {x} {y} = Rezk⋆IdR x y
+  Rezk .⋆Assoc {x} {y} {z} {w} = Rezk⋆Assoc x y z w
+  Rezk .isSetHom {x} {y} = isSetRezkHom x y
+
+  RezkIso→Iso : ∀ {x y} → CatIso Rezk (inc x) (inc y) → CatIso C x y 
+  RezkIso→Iso (f , isiso g s r) = (f , isiso g s r)
+
+  Iso→RezkIso : ∀ {x y} → CatIso C x y → CatIso Rezk (inc x) (inc y)
+  Iso→RezkIso (f , isiso g s r) = (f , isiso g s r)
+    
+  RezkIsoToPath : ∀ x y → CatIso Rezk x y → x ≡ y
+  RezkIsoToPath = elimSet₂ (λ x y → isSet→ (squash x y)) R-inc R-ua₁ R-ua₂ where
+    
+    R-inc = λ x y f → inc-ua (RezkIso→Iso f)
+
+    R-ua₁ : {x y z : C.ob} (f : Σ C.Hom[ y , z ] (isIso C))
+          → PathP (λ i → CatIso Rezk (inc x) (inc-ua f i) → inc x ≡ inc-ua f i)
+              (R-inc x y) (R-inc x z)
+    R-ua₁ e = toPathP $ funExt λ f → let f' = RezkIso→Iso f in
+      subst2 _≡_ refl (inc-ua e) (inc-ua _)
+        ≡⟨ cong (subst2 _≡_ refl (inc-ua e) ∘ inc-ua) (
+          CatIso≡ _ _ (congL C._⋆_ (transportRefl _))
+        ) ⟩
+      subst2 _≡_ refl (inc-ua e) (inc-ua (⋆Iso f' (invIso e)))
+        ≡⟨ fromPathP (compPath-filler (inc-ua (⋆Iso f' (invIso e))) (inc-ua e)) ⟩
+      inc-ua (⋆Iso f' (invIso e)) ∙ inc-ua e
+        ≡⟨ sym (inc-⋆ (⋆Iso f' (invIso e)) e) ⟩
+      inc-ua (⋆Iso (⋆Iso f' (invIso e)) e)
+        ≡⟨ cong inc-ua (CatIso≡ _ _ (
+          C.⋆Assoc _ _ _ ∙ congR C._⋆_ (e .snd .sec) ∙ C.⋆IdR _)
+        ) ⟩
+      inc-ua f' ∎
+
+    R-ua₂ : {x y z : C.ob} (f : Σ C.Hom[ x , y ] (isIso C))
+          → PathP (λ i → CatIso Rezk (inc-ua f i) (inc z) → inc-ua f i ≡ inc z)
+              (R-inc x z) (R-inc y z)
+    R-ua₂ e = toPathP $ funExt λ f → let f' = RezkIso→Iso f in
+      subst2 _≡_ (inc-ua e) refl (inc-ua _)
+        ≡⟨ cong (subst2 _≡_ (inc-ua e) refl ∘ inc-ua) (
+          CatIso≡ _ _ (congR C._⋆_ (transportRefl _))
+        ) ⟩
+      subst2 _≡_ (inc-ua e) refl (inc-ua (⋆Iso e f'))
+        ≡⟨ fromPathP (compPath-filler' (sym (inc-ua e)) (inc-ua (⋆Iso e f'))) ⟩
+      sym (inc-ua e) ∙ inc-ua (⋆Iso e f')
+        ≡⟨ congR _∙_ (inc-⋆ e f') ⟩
+      sym (inc-ua e) ∙ (inc-ua e ∙ inc-ua f')
+        ≡⟨ compPathl-cancel (sym (inc-ua e)) (inc-ua f') ⟩
+      inc-ua f' ∎
+
+  RezkIsoToPathId : ∀ x → RezkIsoToPath x x idCatIso ≡ refl
+  RezkIsoToPathId = elimProp (λ x → squash x x _ _) (λ x → inc-id)
+
+  RezkIsoToPathη : ∀ x y p → RezkIsoToPath x y (pathToIso p) ≡ p
+  RezkIsoToPathη x = J> cong (RezkIsoToPath x x) pathToIso-refl ∙ RezkIsoToPathId x
+
+  RezkIsoToPathβ : ∀ x y f → pathToIso (RezkIsoToPath x y f) ≡ f
+  RezkIsoToPathβ = elimProp₂ (λ x y → isPropΠ λ _ → isSet-CatIso x y _ _) λ x y f →
+    CatIso≡ _ _ $ transportRefl _ ∙ C.⋆IdL _
+
+  isUnivalentRezk : isUnivalent Rezk
+  isUnivalentRezk .univ x y = isoToIsEquiv $
+    iso pathToIso (RezkIsoToPath x y) (RezkIsoToPathβ x y) (RezkIsoToPathη x y)
+
+  →Rezk : Functor C Rezk
+  →Rezk .F-ob = inc
+  →Rezk .F-hom = idfun _
+  →Rezk .F-id = refl
+  →Rezk .F-seq f g = refl
+
+  →RezkFF : isFullyFaithful →Rezk
+  →RezkFF x y = idIsEquiv _
+
+  →RezkSurj : isEssentiallySurj →Rezk
+  →RezkSurj = elimProp (λ x → isPropPropTrunc) λ x → ∣ x , idCatIso ∣₁
+
+  isWkEquiv→Rezk : isWeakEquivalence →Rezk
+  isWkEquiv→Rezk .isWeakEquivalence.fullfaith = →RezkFF
+  isWkEquiv→Rezk .isWeakEquivalence.esssurj = →RezkSurj
+
+  isRezkCompletion→Rezk : isRezkCompletion →Rezk
+  isRezkCompletion→Rezk = makeIsRezkCompletion isUnivalentRezk isWkEquiv→Rezk

From e5cde84826ae9e732c5690f74fdb606685d132cc Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sun, 16 Feb 2025 17:59:18 +0530
Subject: [PATCH 2/9] Update Construction.agda

---
 .../Categories/RezkCompletion/Construction.agda    | 14 +++++---------
 1 file changed, 5 insertions(+), 9 deletions(-)

diff --git a/Cubical/Categories/RezkCompletion/Construction.agda b/Cubical/Categories/RezkCompletion/Construction.agda
index 4d73994ad..80febabb8 100644
--- a/Cubical/Categories/RezkCompletion/Construction.agda
+++ b/Cubical/Categories/RezkCompletion/Construction.agda
@@ -376,7 +376,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
   Rezk⋆Assoc : ∀ x y z w f g h
              → Rezk⋆ x z w (Rezk⋆ x y z f g) h ≡ Rezk⋆ x y w f (Rezk⋆ y z w g h)
   Rezk⋆Assoc = elimProp₂ (λ x y → isPropΠ5 λ z w _ _ _ → isSetRezkHom x w _ _) λ x y →
-    elimProp₂ (λ z w → isPropΠ3 λ _ _ _ → isSetRezkHom (inc x) w _ _) λ z w → C.⋆Assoc
+               elimProp₂ (λ z w → isPropΠ3 λ _ _ _ → isSetRezkHom (inc x) w _ _) λ z w → C.⋆Assoc
 
   Rezk : Category (ℓ-max ℓ ℓ') ℓ'
   Rezk .ob = RezkOb
@@ -412,9 +412,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
       inc-ua (⋆Iso f' (invIso e)) ∙ inc-ua e
         ≡⟨ sym (inc-⋆ (⋆Iso f' (invIso e)) e) ⟩
       inc-ua (⋆Iso (⋆Iso f' (invIso e)) e)
-        ≡⟨ cong inc-ua (CatIso≡ _ _ (
-          C.⋆Assoc _ _ _ ∙ congR C._⋆_ (e .snd .sec) ∙ C.⋆IdR _)
-        ) ⟩
+        ≡⟨ cong inc-ua (CatIso≡ _ _ (C.⋆Assoc _ _ _ ∙ congR C._⋆_ (e .snd .sec) ∙ C.⋆IdR _)) ⟩
       inc-ua f' ∎
 
     R-ua₂ : {x y z : C.ob} (f : Σ C.Hom[ x , y ] (isIso C))
@@ -422,9 +420,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
               (R-inc x z) (R-inc y z)
     R-ua₂ e = toPathP $ funExt λ f → let f' = RezkIso→Iso f in
       subst2 _≡_ (inc-ua e) refl (inc-ua _)
-        ≡⟨ cong (subst2 _≡_ (inc-ua e) refl ∘ inc-ua) (
-          CatIso≡ _ _ (congR C._⋆_ (transportRefl _))
-        ) ⟩
+        ≡⟨ cong (subst2 _≡_ (inc-ua e) refl ∘ inc-ua) (CatIso≡ _ _ (congR C._⋆_ (transportRefl _))) ⟩
       subst2 _≡_ (inc-ua e) refl (inc-ua (⋆Iso e f'))
         ≡⟨ fromPathP (compPath-filler' (sym (inc-ua e)) (inc-ua (⋆Iso e f'))) ⟩
       sym (inc-ua e) ∙ inc-ua (⋆Iso e f')
@@ -460,8 +456,8 @@ module RezkByHIT (C : Category ℓ ℓ') where
   →RezkSurj = elimProp (λ x → isPropPropTrunc) λ x → ∣ x , idCatIso ∣₁
 
   isWkEquiv→Rezk : isWeakEquivalence →Rezk
-  isWkEquiv→Rezk .isWeakEquivalence.fullfaith = →RezkFF
-  isWkEquiv→Rezk .isWeakEquivalence.esssurj = →RezkSurj
+  isWkEquiv→Rezk .fullfaith = →RezkFF
+  isWkEquiv→Rezk .esssurj = →RezkSurj
 
   isRezkCompletion→Rezk : isRezkCompletion →Rezk
   isRezkCompletion→Rezk = makeIsRezkCompletion isUnivalentRezk isWkEquiv→Rezk

From 253b30652af8d142287749efbf62f1db67bf60d0 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sun, 16 Feb 2025 18:19:59 +0530
Subject: [PATCH 3/9] Removed trailing whitespaces

---
 .../RezkCompletion/Construction.agda           | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/Cubical/Categories/RezkCompletion/Construction.agda b/Cubical/Categories/RezkCompletion/Construction.agda
index 80febabb8..4cbee0f36 100644
--- a/Cubical/Categories/RezkCompletion/Construction.agda
+++ b/Cubical/Categories/RezkCompletion/Construction.agda
@@ -78,7 +78,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
   open isUnivalent
   open Functor
   open isIso
-  
+ -- here
   private variable
     x y z w : ob C
 
@@ -202,7 +202,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
   inc-⋆ f g = sym (Square≃doubleComp _ _ _ _ .fst (inc-sq f g))
 
   inc-id : inc-ua (idCatIso {x = x}) ≡ refl
-  inc-id = 
+  inc-id =-- here
     incId ≡⟨ sym (compPathr-cancel (sym incId) incId) ⟩
     (incId ∙ incId) ∙ sym incId ≡⟨ congL _∙_ (sym (inc-⋆ idCatIso idCatIso)) ⟩
     inc-ua (⋆Iso idCatIso idCatIso) ∙ sym incId ≡⟨ congL _∙_ (cong inc-ua (⋆IsoIdL _)) ⟩
@@ -211,7 +211,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
     where incId = inc-ua idCatIso
 
   inc-inv : (f : CatIso C x y) → inc-ua (invIso f) ≡ sym (inc-ua f)
-  inc-inv f = 
+  inc-inv f =-- here
     inc-ua (invIso f) ≡⟨ sym (compPathr-cancel (sym (inc-ua f)) (inc-ua (invIso f))) ⟩
     (inc-ua (invIso f) ∙ inc-ua f) ∙ sym (inc-ua f) ≡⟨ congL _∙_ (sym (inc-⋆ (invIso f) f)) ⟩
     inc-ua (⋆Iso (invIso f) f) ∙ sym (inc-ua f) ≡⟨ congL _∙_ (cong inc-ua (CatIso≡ _ _ (f .snd .sec))) ⟩
@@ -268,7 +268,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
       g .snd .inv C.⋆ (transport (cong fst (H-inc-ua f)) h)
         ≡⟨ sym (uaβ _ _) ⟩
       transport (cong fst (H-ua-inc g)) (transport (cong fst (H-inc-ua f)) h) ∎
-    
+
     H-inc-sq : ∀ {x y z w} (f : CatIso C y z) (g : CatIso C z w)
              → Square (H-inc-ua {x = x} f) (H-inc-ua (⋆Iso f g)) refl (H-inc-ua g)
     H-inc-sq f g = ΣSquareSet (λ _ → isProp→isSet isPropIsSet) $ typeSquare λ h →
@@ -283,7 +283,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
       transport refl h C.⋆ (f .fst C.⋆ g .fst)
         ≡⟨ sym (uaβ _ _) ⟩
       transport (cong fst (H-inc-ua (⋆Iso f g))) (transport refl h) ∎
-    
+
     H-sq-inc : ∀ {x y z w} (f : CatIso C x y) (g : CatIso C y z)
              → Square (H-ua-inc {z = w} f) (H-ua-inc (⋆Iso f g)) refl (H-ua-inc g)
     H-sq-inc f g = ΣSquareSet (λ _ → isProp→isSet isPropIsSet) $ typeSquare λ h →
@@ -298,7 +298,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
       (g .snd .inv C.⋆ f .snd .inv) C.⋆ transport refl h
         ≡⟨ sym (uaβ _ _) ⟩
       transport (cong fst (H-ua-inc (⋆Iso f g))) (transport refl h) ∎
-    
+
   RezkHom : RezkOb → RezkOb → Type ℓ'
   RezkHom x y = RezkHomSet x y .fst
 
@@ -388,15 +388,15 @@ module RezkByHIT (C : Category ℓ ℓ') where
   Rezk .⋆Assoc {x} {y} {z} {w} = Rezk⋆Assoc x y z w
   Rezk .isSetHom {x} {y} = isSetRezkHom x y
 
-  RezkIso→Iso : ∀ {x y} → CatIso Rezk (inc x) (inc y) → CatIso C x y 
+  RezkIso→Iso : ∀ {x y} → CatIso Rezk (inc x) (inc y) → CatIso C x y-- here
   RezkIso→Iso (f , isiso g s r) = (f , isiso g s r)
 
   Iso→RezkIso : ∀ {x y} → CatIso C x y → CatIso Rezk (inc x) (inc y)
   Iso→RezkIso (f , isiso g s r) = (f , isiso g s r)
-    
+
   RezkIsoToPath : ∀ x y → CatIso Rezk x y → x ≡ y
   RezkIsoToPath = elimSet₂ (λ x y → isSet→ (squash x y)) R-inc R-ua₁ R-ua₂ where
-    
+
     R-inc = λ x y f → inc-ua (RezkIso→Iso f)
 
     R-ua₁ : {x y z : C.ob} (f : Σ C.Hom[ y , z ] (isIso C))

From 306f54755bcb16d19d21cfa2a40e1a82fbfed097 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sun, 16 Feb 2025 18:25:35 +0530
Subject: [PATCH 4/9] Remove trailing whitespace

---
 Cubical/Categories/RezkCompletion/Construction.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Cubical/Categories/RezkCompletion/Construction.agda b/Cubical/Categories/RezkCompletion/Construction.agda
index 4cbee0f36..e1a03d202 100644
--- a/Cubical/Categories/RezkCompletion/Construction.agda
+++ b/Cubical/Categories/RezkCompletion/Construction.agda
@@ -78,7 +78,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
   open isUnivalent
   open Functor
   open isIso
- -- here
+
   private variable
     x y z w : ob C
 
@@ -202,7 +202,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
   inc-⋆ f g = sym (Square≃doubleComp _ _ _ _ .fst (inc-sq f g))
 
   inc-id : inc-ua (idCatIso {x = x}) ≡ refl
-  inc-id =-- here
+  inc-id =
     incId ≡⟨ sym (compPathr-cancel (sym incId) incId) ⟩
     (incId ∙ incId) ∙ sym incId ≡⟨ congL _∙_ (sym (inc-⋆ idCatIso idCatIso)) ⟩
     inc-ua (⋆Iso idCatIso idCatIso) ∙ sym incId ≡⟨ congL _∙_ (cong inc-ua (⋆IsoIdL _)) ⟩
@@ -211,7 +211,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
     where incId = inc-ua idCatIso
 
   inc-inv : (f : CatIso C x y) → inc-ua (invIso f) ≡ sym (inc-ua f)
-  inc-inv f =-- here
+  inc-inv f =
     inc-ua (invIso f) ≡⟨ sym (compPathr-cancel (sym (inc-ua f)) (inc-ua (invIso f))) ⟩
     (inc-ua (invIso f) ∙ inc-ua f) ∙ sym (inc-ua f) ≡⟨ congL _∙_ (sym (inc-⋆ (invIso f) f)) ⟩
     inc-ua (⋆Iso (invIso f) f) ∙ sym (inc-ua f) ≡⟨ congL _∙_ (cong inc-ua (CatIso≡ _ _ (f .snd .sec))) ⟩
@@ -388,7 +388,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
   Rezk .⋆Assoc {x} {y} {z} {w} = Rezk⋆Assoc x y z w
   Rezk .isSetHom {x} {y} = isSetRezkHom x y
 
-  RezkIso→Iso : ∀ {x y} → CatIso Rezk (inc x) (inc y) → CatIso C x y-- here
+  RezkIso→Iso : ∀ {x y} → CatIso Rezk (inc x) (inc y) → CatIso C x y
   RezkIso→Iso (f , isiso g s r) = (f , isiso g s r)
 
   Iso→RezkIso : ∀ {x y} → CatIso C x y → CatIso Rezk (inc x) (inc y)

From 07f8c44465358f3bed53abca9d9bbb89a38ffe92 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sun, 2 Mar 2025 11:21:49 +0530
Subject: [PATCH 5/9] Replace HIT with GroupoidQuotient

---
 .../RezkCompletion/Construction.agda          | 118 ++++++++----------
 1 file changed, 49 insertions(+), 69 deletions(-)

diff --git a/Cubical/Categories/RezkCompletion/Construction.agda b/Cubical/Categories/RezkCompletion/Construction.agda
index e1a03d202..fe07beb32 100644
--- a/Cubical/Categories/RezkCompletion/Construction.agda
+++ b/Cubical/Categories/RezkCompletion/Construction.agda
@@ -32,7 +32,6 @@ open import Cubical.Categories.RezkCompletion.Base
 
 private variable
   ℓ ℓ' ℓ'' ℓ''' : Level
-  A B C D : Type ℓ
 
 open isWeakEquivalence
 
@@ -79,48 +78,43 @@ module RezkByHIT (C : Category ℓ ℓ') where
   open Functor
   open isIso
 
-  private variable
-    x y z w : ob C
-
-  data RezkOb : Type (ℓ-max ℓ ℓ') where
-    inc : ob C → RezkOb
-    inc-ua : (f : CatIso C x y) → inc x ≡ inc y
-    inc-sq : (f : CatIso C x y) (g : CatIso C y z)
-           → Square (inc-ua f) (inc-ua (⋆Iso f g)) refl (inc-ua g)
-    squash : isGroupoid RezkOb
-
-  module _ {P : RezkOb → Type ℓ''}
-    (P-Grpd : ∀ x → isGroupoid (P x))
-    (P-inc : ∀ x → P (inc x))
-    (P-inc-ua : ∀ {x y} f → PathP (λ i → P (inc-ua f i)) (P-inc x) (P-inc y))
-    (P-inc-sq : ∀ {x y z} f g → SquareP (λ i j → P (inc-sq {x = x} {y} {z} f g i j))
-        (P-inc-ua f) (P-inc-ua (⋆Iso f g)) refl (P-inc-ua g))
-    where
+  private
+    variable
+      x y z w : ob C
+    
+    IsoC : ob C → ob C → Type ℓ'
+    IsoC = CatIso C
 
-    elim : ∀ x → P x
-    elim (inc x) = P-inc x
-    elim (inc-ua f i) = P-inc-ua f i
-    elim (inc-sq f g i j) = P-inc-sq f g i j
-    elim (squash x y p q r s i j k) =
-      isOfHLevel→isOfHLevelDep 3 P-Grpd _ _ _ _ (cong (cong elim) r) (cong (cong elim) s) (squash x y p q r s) i j k
-
-  module _ {P : RezkOb → Type ℓ''}
-    (P-Set : ∀ x → isSet (P x))
-    (P-inc : ∀ x → P (inc x))
-    (P-inc-ua : ∀ {x y} f → PathP (λ i → P (inc-ua f i)) (P-inc x) (P-inc y))
-    where
+    ⋆IsoC : ∀ x y z → IsoC x y → IsoC y z → IsoC x z
+    ⋆IsoC x y z = ⋆Iso
 
-    elimSet : ∀ x → P x
-    elimSet = elim (λ x → isSet→isGroupoid (P-Set x)) P-inc P-inc-ua λ f g → isSet→SquareP (λ i j → P-Set (inc-sq f g i j)) _ _ _ _
+  RezkOb : Type (ℓ-max ℓ ℓ')
+  RezkOb = ob C // ⋆IsoC
 
-  module _ {P : RezkOb → Type ℓ''}
-    (P-Prop : ∀ x → isProp (P x))
-    (P-inc : ∀ x → P (inc x))
-    where
+  inc : ob C → RezkOb
+  inc = [_]
+
+  inc-ua : IsoC x y → inc x ≡ inc y
+  inc-ua = eq//
+
+  inc-sq : (f : IsoC x y) (g : IsoC y z) → Square (inc-ua f) (inc-ua (⋆Iso f g)) refl (inc-ua g)
+  inc-sq = comp//
+
+  squash : isGroupoid RezkOb
+  squash = squash//
 
-    elimProp : ∀ x → P x
-    elimProp = elimSet (λ x → isProp→isSet (P-Prop x)) P-inc λ f → isProp→PathP (λ i → P-Prop (inc-ua f i)) _ _
+  elim : {P : RezkOb → Type ℓ''} → _ → (f : _) → (feq : _) → _ → ∀ x → P x
+  elim = GQ.elim {A = ob C} ⋆IsoC
 
+  elimSet : {P : RezkOb → Type ℓ''} → _ → (f : _) → _ → ∀ x → P x
+  elimSet = GQ.elimSet {A = ob C} ⋆IsoC
+
+  elimProp : {P : RezkOb → Type ℓ''} → _ → _ → ∀ x → P x
+  elimProp = GQ.elimProp {A = ob C} ⋆IsoC
+
+  rec : {P : Type ℓ''} → _ → (f : _) → (feq : _) → _ → RezkOb → P
+  rec = GQ.rec {A = ob C} ⋆IsoC
+  
   module _ {P : RezkOb → RezkOb → Type ℓ''}
     (P-Set : ∀ x y → isSet (P x y))
     (P-inc : ∀ x y → P (inc x) (inc y))
@@ -157,27 +151,16 @@ module RezkByHIT (C : Category ℓ ℓ') where
     elimSet₃ = elimSet (λ x → isSetΠ2 (P-Set x)) (λ x → elimSet₂ (P-Set (inc x)) (P-inc x) P-ua₁ P-ua₂) λ f → funExt₂ $
       elimProp₂ (λ x y → isOfHLevelPathP' 1 (P-Set _ _ _) _ _) λ x y → P-ua₃ f
 
-  module _ {P : Type ℓ''}
-    (P-Grpd : isGroupoid P)
-    (P-inc : ob C → P)
-    (P-inc-ua : ∀ {x y} → CatIso C x y → P-inc x ≡ P-inc y)
-    (P-inc-sq : ∀ {x y z} (f : CatIso C x y) (g : CatIso C y z)
-      → Square (P-inc-ua f) (P-inc-ua (⋆Iso f g)) refl (P-inc-ua g))
-    where
-
-    rec : RezkOb → P
-    rec = elim (λ _ → P-Grpd) P-inc P-inc-ua P-inc-sq
-
   module _ {P : Type ℓ''}
     (P-Grpd : isGroupoid P)
     (P-inc : ob C → ob C → P)
-    (P-inc-ua : ∀ {x y z} → CatIso C y z → P-inc x y ≡ P-inc x z)
-    (P-ua-inc : ∀ {x y z} → CatIso C x y → P-inc x z ≡ P-inc y z)
-    (P-ua-inc-ua : ∀ {x y z w} (g : CatIso C z w) (f : CatIso C x y)
+    (P-inc-ua : ∀ {x y z} → IsoC y z → P-inc x y ≡ P-inc x z)
+    (P-ua-inc : ∀ {x y z} → IsoC x y → P-inc x z ≡ P-inc y z)
+    (P-ua-inc-ua : ∀ {x y z w} (g : IsoC z w) (f : IsoC x y)
       → Square (P-ua-inc g) (P-ua-inc g) (P-inc-ua f) (P-inc-ua f))
-    (P-inc-sq : ∀ {x y z w} (f : CatIso C y z) (g : CatIso C z w)
+    (P-inc-sq : ∀ {x y z w} (f : IsoC y z) (g : IsoC z w)
       → Square (P-inc-ua {x = x} f) (P-inc-ua (⋆Iso f g)) refl (P-inc-ua g))
-    (P-sq-inc : ∀ {x y z w} (f : CatIso C x y) (g : CatIso C y z)
+    (P-sq-inc : ∀ {x y z w} (f : IsoC x y) (g : IsoC y z)
       → Square (P-ua-inc {z = w} f) (P-ua-inc (⋆Iso f g)) refl (P-ua-inc g))
     where
 
@@ -197,9 +180,8 @@ module RezkByHIT (C : Category ℓ ℓ') where
         subst⁻ (PathP _ (F-Iso {F = P-inc} f)) (F-Iso-Pres⋆ f g) $
           transportIsoToPathIso P-univ _ _
 
-  inc-⋆ : (f : CatIso C x y) (g : CatIso C y z)
-        → inc-ua (⋆Iso f g) ≡ inc-ua f ∙ inc-ua g
-  inc-⋆ f g = sym (Square≃doubleComp _ _ _ _ .fst (inc-sq f g))
+  inc-⋆ : (f : IsoC x y) (g : IsoC y z) → inc-ua (⋆Iso f g) ≡ inc-ua f ∙ inc-ua g
+  inc-⋆ = GQ.comp'// _ ⋆IsoC
 
   inc-id : inc-ua (idCatIso {x = x}) ≡ refl
   inc-id =
@@ -210,7 +192,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
     refl ∎
     where incId = inc-ua idCatIso
 
-  inc-inv : (f : CatIso C x y) → inc-ua (invIso f) ≡ sym (inc-ua f)
+  inc-inv : (f : IsoC x y) → inc-ua (invIso f) ≡ sym (inc-ua f)
   inc-inv f =
     inc-ua (invIso f) ≡⟨ sym (compPathr-cancel (sym (inc-ua f)) (inc-ua (invIso f))) ⟩
     (inc-ua (invIso f) ∙ inc-ua f) ∙ sym (inc-ua f) ≡⟨ congL _∙_ (sym (inc-⋆ (invIso f) f)) ⟩
@@ -220,9 +202,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
     sym (inc-ua f) ∎
 
   inc-pathToIso : (p : x ≡ y) → inc-ua (pathToIso p) ≡ cong inc p
-  inc-pathToIso = lemma _ where
-    lemma : ∀ y (p : x ≡ y) → inc-ua (pathToIso p) ≡ cong inc p
-    lemma = J> cong inc-ua pathToIso-refl ∙ inc-id
+  inc-pathToIso = J (λ y p → inc-ua (pathToIso p) ≡ cong inc p) (cong inc-ua pathToIso-refl ∙ inc-id)
 
   inc-surj : isSurjection inc
   inc-surj = elimProp (λ x → isPropPropTrunc) λ x → ∣ x , refl ∣₁
@@ -232,16 +212,16 @@ module RezkByHIT (C : Category ℓ ℓ') where
     rec₂ isGroupoidHSet H-inc H-inc-ua H-ua-inc H-ua-inc-ua H-inc-sq H-sq-inc where
 
     H-inc : ob C → ob C → hSet ℓ'
-    H-inc x y = C [ x , y ] , C .isSetHom
+    H-inc x y = C .Hom[_,_] x y , C .isSetHom
 
-    H-inc-ua : ∀ {x y z} → CatIso C y z → H-inc x y ≡ H-inc x z
+    H-inc-ua : ∀ {x y z} → IsoC y z → H-inc x y ≡ H-inc x z
     H-inc-ua f = TypeOfHLevel≡ 2 $ isoToPath λ where
       .Iso.fun → C._⋆ f .fst
       .Iso.inv → C._⋆ f .snd .inv
       .Iso.rightInv _ → C.⋆Assoc _ _ _ ∙∙ congR C._⋆_ (f .snd .sec) ∙∙ C.⋆IdR _
       .Iso.leftInv  _ → C.⋆Assoc _ _ _ ∙∙ congR C._⋆_ (f .snd .ret) ∙∙ C.⋆IdR _
 
-    H-ua-inc : ∀ {x y z} → CatIso C x y → H-inc x z ≡ H-inc y z
+    H-ua-inc : ∀ {x y z} → IsoC x y → H-inc x z ≡ H-inc y z
     H-ua-inc f = TypeOfHLevel≡ 2 $ isoToPath λ where
       .Iso.fun → f .snd .inv C.⋆_
       .Iso.inv → f .fst C.⋆_
@@ -254,7 +234,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
     typeSquare h = compPath→Square $ isInjectiveTransport $ funExt λ x →
       transportComposite _ _ x ∙∙ sym (h x) ∙∙ sym (transportComposite _ _ x)
 
-    H-ua-inc-ua : ∀ {x y z w} (g : CatIso C z w) (f : CatIso C x y)
+    H-ua-inc-ua : ∀ {x y z w} (g : IsoC z w) (f : IsoC x y)
                 → Square (H-ua-inc g) (H-ua-inc g) (H-inc-ua f) (H-inc-ua f)
     H-ua-inc-ua g f = ΣSquareSet (λ _ → isProp→isSet isPropIsSet) $ typeSquare λ h →
       transport (cong fst (H-inc-ua f)) (transport (cong fst (H-ua-inc g)) h)
@@ -269,7 +249,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
         ≡⟨ sym (uaβ _ _) ⟩
       transport (cong fst (H-ua-inc g)) (transport (cong fst (H-inc-ua f)) h) ∎
 
-    H-inc-sq : ∀ {x y z w} (f : CatIso C y z) (g : CatIso C z w)
+    H-inc-sq : ∀ {x y z w} (f : IsoC y z) (g : IsoC z w)
              → Square (H-inc-ua {x = x} f) (H-inc-ua (⋆Iso f g)) refl (H-inc-ua g)
     H-inc-sq f g = ΣSquareSet (λ _ → isProp→isSet isPropIsSet) $ typeSquare λ h →
       transport (cong fst (H-inc-ua g)) (transport (cong fst (H-inc-ua f)) h)
@@ -284,7 +264,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
         ≡⟨ sym (uaβ _ _) ⟩
       transport (cong fst (H-inc-ua (⋆Iso f g))) (transport refl h) ∎
 
-    H-sq-inc : ∀ {x y z w} (f : CatIso C x y) (g : CatIso C y z)
+    H-sq-inc : ∀ {x y z w} (f : IsoC x y) (g : IsoC y z)
              → Square (H-ua-inc {z = w} f) (H-ua-inc (⋆Iso f g)) refl (H-ua-inc g)
     H-sq-inc f g = ΣSquareSet (λ _ → isProp→isSet isPropIsSet) $ typeSquare λ h →
       transport (cong fst (H-ua-inc g)) (transport (cong fst (H-ua-inc f)) h)
@@ -388,10 +368,10 @@ module RezkByHIT (C : Category ℓ ℓ') where
   Rezk .⋆Assoc {x} {y} {z} {w} = Rezk⋆Assoc x y z w
   Rezk .isSetHom {x} {y} = isSetRezkHom x y
 
-  RezkIso→Iso : ∀ {x y} → CatIso Rezk (inc x) (inc y) → CatIso C x y
+  RezkIso→Iso : ∀ {x y} → CatIso Rezk (inc x) (inc y) → IsoC x y
   RezkIso→Iso (f , isiso g s r) = (f , isiso g s r)
 
-  Iso→RezkIso : ∀ {x y} → CatIso C x y → CatIso Rezk (inc x) (inc y)
+  Iso→RezkIso : ∀ {x y} → IsoC x y → CatIso Rezk (inc x) (inc y)
   Iso→RezkIso (f , isiso g s r) = (f , isiso g s r)
 
   RezkIsoToPath : ∀ x y → CatIso Rezk x y → x ≡ y

From 37b20a4560415902500dcfdea8eb4fc824010149 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sun, 2 Mar 2025 11:39:28 +0530
Subject: [PATCH 6/9] shorter proof of `inc-surj`

---
 Cubical/Categories/RezkCompletion/Construction.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cubical/Categories/RezkCompletion/Construction.agda b/Cubical/Categories/RezkCompletion/Construction.agda
index fe07beb32..664035779 100644
--- a/Cubical/Categories/RezkCompletion/Construction.agda
+++ b/Cubical/Categories/RezkCompletion/Construction.agda
@@ -205,7 +205,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
   inc-pathToIso = J (λ y p → inc-ua (pathToIso p) ≡ cong inc p) (cong inc-ua pathToIso-refl ∙ inc-id)
 
   inc-surj : isSurjection inc
-  inc-surj = elimProp (λ x → isPropPropTrunc) λ x → ∣ x , refl ∣₁
+  inc-surj = GQ.isSurjective[] ⋆IsoC
 
   RezkHomSet : RezkOb → RezkOb → hSet ℓ'
   RezkHomSet =

From 2f2f817b054a83cfaf930c766c1e27aa3420acbc Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sun, 2 Mar 2025 11:40:41 +0530
Subject: [PATCH 7/9] fix whitespace

---
 Cubical/Categories/RezkCompletion/Construction.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cubical/Categories/RezkCompletion/Construction.agda b/Cubical/Categories/RezkCompletion/Construction.agda
index 664035779..d2ecd6921 100644
--- a/Cubical/Categories/RezkCompletion/Construction.agda
+++ b/Cubical/Categories/RezkCompletion/Construction.agda
@@ -81,7 +81,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
   private
     variable
       x y z w : ob C
-    
+
     IsoC : ob C → ob C → Type ℓ'
     IsoC = CatIso C
 
@@ -114,7 +114,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
 
   rec : {P : Type ℓ''} → _ → (f : _) → (feq : _) → _ → RezkOb → P
   rec = GQ.rec {A = ob C} ⋆IsoC
-  
+
   module _ {P : RezkOb → RezkOb → Type ℓ''}
     (P-Set : ∀ x y → isSet (P x y))
     (P-inc : ∀ x y → P (inc x) (inc y))

From 0308ad0f0ff75adf286a8f7f2ec1789f4d7b3ea3 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sun, 2 Mar 2025 17:34:04 +0530
Subject: [PATCH 8/9] Forgot to import GroupoidQuotients

---
 Cubical/Categories/RezkCompletion/Construction.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cubical/Categories/RezkCompletion/Construction.agda b/Cubical/Categories/RezkCompletion/Construction.agda
index d2ecd6921..231256754 100644
--- a/Cubical/Categories/RezkCompletion/Construction.agda
+++ b/Cubical/Categories/RezkCompletion/Construction.agda
@@ -19,6 +19,7 @@ open import Cubical.Foundations.Equiv.Base
 open import Cubical.Functions.FunExtEquiv
 open import Cubical.Functions.Surjection
 open import Cubical.HITs.PropositionalTruncation using (∥_∥₁; ∣_∣₁; isPropPropTrunc)
+open import Cubical.HITs.GroupoidQuotients as GQ using (_//_; [_]; eq//; comp//; squash//)
 
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor

From 152c2de3456535b36ee8286740d5d0e65d3ff4be Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Mon, 3 Mar 2025 20:46:20 +0530
Subject: [PATCH 9/9] add implicit argument

---
 Cubical/Categories/RezkCompletion/Construction.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cubical/Categories/RezkCompletion/Construction.agda b/Cubical/Categories/RezkCompletion/Construction.agda
index 231256754..415d33e4c 100644
--- a/Cubical/Categories/RezkCompletion/Construction.agda
+++ b/Cubical/Categories/RezkCompletion/Construction.agda
@@ -287,7 +287,7 @@ module RezkByHIT (C : Category ℓ ℓ') where
   isSetRezkHom x y = RezkHomSet x y .snd
 
   private
-    tr : transport refl ≡ idfun A
+    tr : {A : Type ℓ''} → transport refl ≡ idfun A
     tr = funExt transportRefl
 
   RezkId : ∀ x → RezkHom x x