diff --git a/Cubical/Algebra/CommAlgebra/Localisation.agda b/Cubical/Algebra/CommAlgebra/Localisation.agda
index cdbd82691d..a0d9ecaab4 100644
--- a/Cubical/Algebra/CommAlgebra/Localisation.agda
+++ b/Cubical/Algebra/CommAlgebra/Localisation.agda
@@ -120,7 +120,7 @@ module AlgLoc (R' : CommRing ℓ)
     _⋆_  (snd B') r 1b ∎
 
 
- -- an immediate corrollary:
+ -- an immediate corollary:
  isContrHomS⁻¹RS⁻¹R : isContr (CommAlgebraHom S⁻¹RAsCommAlg S⁻¹RAsCommAlg)
  isContrHomS⁻¹RS⁻¹R = S⁻¹RHasAlgUniversalProp S⁻¹RAsCommAlg S⋆1⊆S⁻¹Rˣ
 
diff --git a/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda b/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda
index c2386885c6..fce941ded0 100644
--- a/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda
+++ b/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda
@@ -118,7 +118,7 @@ module _ (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultClos
                         ⦃ ψS⊆Bˣ s' s'∈S' ⦄ ⦄
      ⦃ ψS⊆Bˣ (u · s) (SMultClosedSubset .multClosed u∈S' s∈S') ⦄
      where
-     -- only a few indidividual steps can be solved by the ring solver yet
+     -- only a few individual steps can be solved by the ring solver yet
      instancepath : ⦃ _ : ψ₀ s ∈ Bˣ ⦄ ⦃ _ : ψ₀ s' ∈ Bˣ ⦄
                     ⦃ _ : ψ₀ (u · s · s') ∈ Bˣ ⦄ ⦃ _ : ψ₀ (u · s) ·B ψ₀ s' ∈ Bˣ ⦄
                     ⦃ _ : ψ₀ (u · s) ∈ Bˣ ⦄
@@ -227,7 +227,7 @@ module _ (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultClos
      ⦃ ψS⊆Bˣ s s∈S' ⦄ ⦃ ψS⊆Bˣ s' s'∈S' ⦄ ⦃ ψS⊆Bˣ (s · s') (SMultClosedSubset .multClosed s∈S' s'∈S') ⦄
      ⦃ BˣMultClosed _ _ ⦃ ψS⊆Bˣ s s∈S' ⦄ ⦃ ψS⊆Bˣ s' s'∈S' ⦄ ⦄
      where
-     -- only a few indidividual steps can be solved by the ring solver yet
+     -- only a few individual steps can be solved by the ring solver yet
      instancepath : ⦃ _ : ψ₀ s ∈ Bˣ ⦄ ⦃ _ : ψ₀ s' ∈ Bˣ ⦄
                     ⦃ _ : ψ₀ (s · s') ∈ Bˣ ⦄ ⦃ _ : ψ₀ s ·B ψ₀ s' ∈ Bˣ ⦄
                 → ψ₀ (r · s' + r' · s) ·B ψ₀ (s · s') ⁻¹ ≡ ψ₀ r ·B ψ₀ s ⁻¹ +B ψ₀ r' ·B ψ₀ s' ⁻¹
@@ -265,7 +265,7 @@ module _ (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultClos
      ⦃ ψS⊆Bˣ s s∈S' ⦄ ⦃ ψS⊆Bˣ s' s'∈S' ⦄ ⦃ ψS⊆Bˣ (s · s') (SMultClosedSubset .multClosed s∈S' s'∈S') ⦄
      ⦃ BˣMultClosed _ _ ⦃ ψS⊆Bˣ s s∈S' ⦄ ⦃ ψS⊆Bˣ s' s'∈S' ⦄ ⦄
      where
-     -- only a indidividual steps can be solved by the ring solver yet
+     -- only a few individual steps can be solved by the ring solver yet
      instancepath : ⦃ _ : ψ₀ s ∈ Bˣ ⦄ ⦃ _ : ψ₀ s' ∈ Bˣ ⦄
                     ⦃ _ : ψ₀ (s · s') ∈ Bˣ ⦄ ⦃ _ : ψ₀ s ·B ψ₀ s' ∈ Bˣ ⦄
                   → ψ₀ (r · r') ·B ψ₀ (s · s') ⁻¹ ≡ (ψ₀ r ·B ψ₀ s ⁻¹) ·B (ψ₀ r' ·B ψ₀ s' ⁻¹)
diff --git a/Cubical/Categories/Constructions/Quotient.agda b/Cubical/Categories/Constructions/Quotient.agda
new file mode 100644
index 0000000000..82b0c2d852
--- /dev/null
+++ b/Cubical/Categories/Constructions/Quotient.agda
@@ -0,0 +1,82 @@
+-- Quotient category
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Constructions.Quotient where
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor.Base
+open import Cubical.Categories.Limits.Terminal
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Prelude
+open import Cubical.HITs.SetQuotients renaming ([_] to ⟦_⟧)
+
+private
+  variable
+    ℓ ℓ' ℓq : Level
+
+module _ (C : Category ℓ ℓ') where
+  open Category C
+
+  module _ (_~_ : {x y : ob} (f g : Hom[ x , y ] ) → Type ℓq)
+           (~refl : {x y : ob} (f : Hom[ x , y ] ) → f ~ f)
+           (~cong : {x y z : ob}
+                    (f f' : Hom[ x , y ]) → f ~ f'
+                  → (g g' : Hom[ y , z ]) → g ~ g'
+                  → (f ⋆ g) ~ (f' ⋆ g')) where
+
+    private
+      Hom[_,_]/~ = λ (x y : ob) → Hom[ x , y ] / _~_
+
+      module _ {x y z : ob} where
+        _⋆/~_ : Hom[ x , y ]/~ → Hom[ y , z ]/~ → Hom[ x , z ]/~
+        _⋆/~_ = rec2 squash/ (λ f g → ⟦ f ⋆ g ⟧)
+                    (λ f f' g f~f' → eq/ _ _ (~cong _ _ f~f' _ _ (~refl _)))
+                    (λ f g g' g~g' → eq/ _ _ (~cong _ _ (~refl _) _ _ g~g'))
+
+    module _ {x y : ob} where
+      ⋆/~IdL : (f : Hom[ x , y ]/~) → (⟦ id ⟧ ⋆/~ f) ≡ f
+      ⋆/~IdL = elimProp (λ _ → squash/ _ _) (λ _ → cong ⟦_⟧ (⋆IdL _))
+
+      ⋆/~IdR : (f : Hom[ x , y ]/~) → (f ⋆/~ ⟦ id ⟧) ≡ f
+      ⋆/~IdR = elimProp (λ _ → squash/ _ _) (λ _ → cong ⟦_⟧ (⋆IdR _))
+
+    module _ {x y z w : ob} where
+      ⋆/~Assoc : (f : Hom[ x , y ]/~)
+                (g : Hom[ y , z ]/~)
+                (h : Hom[ z , w ]/~)
+        → ((f ⋆/~ g) ⋆/~ h) ≡ (f ⋆/~ (g ⋆/~ h))
+
+      ⋆/~Assoc = elimProp3 (λ _ _ _ → squash/ _ _) (λ _ _ _ → cong ⟦_⟧ (⋆Assoc _ _ _))
+
+
+    open Category
+    QuotientCategory : Category ℓ (ℓ-max ℓ' ℓq)
+    QuotientCategory .ob = ob C
+    QuotientCategory .Hom[_,_] x y = (C [ x , y ]) / _~_
+    QuotientCategory .id = ⟦ id C ⟧
+    QuotientCategory ._⋆_ = _⋆/~_
+    QuotientCategory .⋆IdL = ⋆/~IdL
+    QuotientCategory .⋆IdR = ⋆/~IdR
+    QuotientCategory .⋆Assoc = ⋆/~Assoc
+    QuotientCategory .isSetHom = squash/
+
+
+    private
+      C/~ = QuotientCategory
+
+    -- Quotient map
+    open Functor
+    QuoFunctor : Functor C C/~
+    QuoFunctor .F-ob x = x
+    QuoFunctor .F-hom = ⟦_⟧
+    QuoFunctor .F-id = refl
+    QuoFunctor .F-seq f g = refl
+
+    -- Quotients preserve initial / terminal objects
+    isInitial/~ : {z : ob C} → isInitial C z → isInitial C/~ z
+    isInitial/~ zInit x = ⟦ zInit x .fst ⟧ , elimProp (λ _ → squash/ _ _)
+        λ f → eq/ _ _ (subst (_~ f) (sym (zInit x .snd f)) (~refl _))
+
+    isFinal/~ : {z : ob C} → isFinal C z → isFinal C/~ z
+    isFinal/~ zFinal x = ⟦ zFinal x .fst ⟧ , elimProp (λ _ → squash/ _ _)
+        λ f → eq/ _ _ (subst (_~ f) (sym (zFinal x .snd f)) (~refl _))