diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md
index f42fcba793..b382e46390 100644
--- a/src/category-theory.lagda.md
+++ b/src/category-theory.lagda.md
@@ -112,6 +112,7 @@ open import category-theory.pregroupoids public
 open import category-theory.presheaf-categories public
 open import category-theory.products-in-precategories public
 open import category-theory.products-of-precategories public
+open import category-theory.pullbacks-in-large-precategories public
 open import category-theory.pullbacks-in-precategories public
 open import category-theory.representable-functors-categories public
 open import category-theory.representable-functors-large-precategories public
@@ -119,6 +120,7 @@ open import category-theory.representable-functors-precategories public
 open import category-theory.representing-arrow-category public
 open import category-theory.sieves-in-categories public
 open import category-theory.slice-precategories public
+open import category-theory.subobject-classifier-in-large-precategories public
 open import category-theory.subprecategories public
 open import category-theory.terminal-objects-precategories public
 open import category-theory.yoneda-lemma-categories public
diff --git a/src/category-theory/monomorphisms-in-large-precategories.lagda.md b/src/category-theory/monomorphisms-in-large-precategories.lagda.md
index e43fe859d6..ad4e1ae3c1 100644
--- a/src/category-theory/monomorphisms-in-large-precategories.lagda.md
+++ b/src/category-theory/monomorphisms-in-large-precategories.lagda.md
@@ -11,6 +11,7 @@ open import category-theory.isomorphisms-in-large-precategories
 open import category-theory.large-precategories
 
 open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.equivalences
 open import foundation.identity-types
@@ -51,6 +52,31 @@ module _
     is-prop-type-Prop is-mono-prop-Large-Precategory
 ```
 
+## The type of monomorphisms in a large precategory
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β) {l1 l2 : Level} (l3 : Level)
+  (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2)
+  where
+
+  mono-Large-Precategory : UU (α l3 ⊔ β l3 l1 ⊔ β l3 l2 ⊔ β l1 l2)
+  mono-Large-Precategory =
+    Σ
+      ( hom-Large-Precategory C X Y)
+      ( is-mono-Large-Precategory C l3 X Y)
+
+  hom-mono-Large-Precategory :
+    (f : mono-Large-Precategory) → hom-Large-Precategory C X Y
+  hom-mono-Large-Precategory f = pr1 f
+
+  is-mono-mono-Large-Precategory :
+    (f : mono-Large-Precategory) →
+    is-mono-Large-Precategory C l3 X Y (hom-mono-Large-Precategory f)
+  is-mono-mono-Large-Precategory f = pr2 f
+```
+
 ## Properties
 
 ### Isomorphisms are monomorphisms
@@ -70,34 +96,34 @@ module _
       ( λ P →
         ( inv
           ( left-unit-law-comp-hom-Large-Precategory C g)) ∙
-          ( ( ap
+          ( ap
             ( λ h' → comp-hom-Large-Precategory C h' g)
             ( inv (is-retraction-hom-inv-iso-Large-Precategory C f))) ∙
-            ( ( associative-comp-hom-Large-Precategory C
+          ( associative-comp-hom-Large-Precategory C
+            ( hom-inv-iso-Large-Precategory C f)
+            ( hom-iso-Large-Precategory C f)
+            ( g)) ∙
+          ( ap
+            ( comp-hom-Large-Precategory C
+              ( hom-inv-iso-Large-Precategory C f))
+            ( P)) ∙
+          ( inv
+            ( associative-comp-hom-Large-Precategory C
               ( hom-inv-iso-Large-Precategory C f)
               ( hom-iso-Large-Precategory C f)
-              ( g)) ∙
-              ( ( ap
-                ( comp-hom-Large-Precategory C
-                  ( hom-inv-iso-Large-Precategory C f))
-                ( P)) ∙
-                ( ( inv
-                  ( associative-comp-hom-Large-Precategory C
-                    ( hom-inv-iso-Large-Precategory C f)
-                    ( hom-iso-Large-Precategory C f)
-                    ( h))) ∙
-                  ( ( ap
-                    ( λ h' → comp-hom-Large-Precategory C h' h)
-                    ( is-retraction-hom-inv-iso-Large-Precategory C f)) ∙
-                    ( left-unit-law-comp-hom-Large-Precategory C h)))))))
+              ( h))) ∙
+          ( ap
+            ( λ h' → comp-hom-Large-Precategory C h' h)
+            ( is-retraction-hom-inv-iso-Large-Precategory C f)) ∙
+          ( left-unit-law-comp-hom-Large-Precategory C h))
       ( λ p →
-        eq-is-prop
+        ( eq-is-prop
           ( is-set-hom-Large-Precategory C Z Y
             ( comp-hom-Large-Precategory C
               ( hom-iso-Large-Precategory C f)
               ( g))
             ( comp-hom-Large-Precategory C
               ( hom-iso-Large-Precategory C f)
-              ( h))))
+              ( h)))))
       ( λ p → eq-is-prop (is-set-hom-Large-Precategory C Z X g h))
 ```
diff --git a/src/category-theory/pullbacks-in-large-precategories.lagda.md b/src/category-theory/pullbacks-in-large-precategories.lagda.md
new file mode 100644
index 0000000000..16500013ba
--- /dev/null
+++ b/src/category-theory/pullbacks-in-large-precategories.lagda.md
@@ -0,0 +1,186 @@
+# Pullbacks in large precategories
+
+```agda
+module category-theory.pullbacks-in-large-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.large-precategories
+
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.unique-existence
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A pullback of two morphisms `f : hom y x` and `g : hom z x` in a category `C`
+consists of:
+
+- an object `w`
+- morphisms `p : hom w y` and `q : hom w z` such that
+- `f ∘ p = g ∘ q` together with the universal property that for every object
+  `w'` and pair of morphisms `p' : hom w' y` and `q' : hom w' z` such that
+  `f ∘ p' = g ∘ q'` there exists a unique morphism `h : hom w' w` such that
+- `p ∘ h = p'`
+- `q ∘ h = q'`.
+
+We say that `C` has all pullbacks if there is a choice of a pullback for each
+object `x` and pair of morphisms into `x` in `C`.
+
+## Definition
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β) {l1 l2 l3 l4 : Level}
+  where
+
+  is-pullback-Large-Precategory :
+    (x : obj-Large-Precategory C l1)
+    (y : obj-Large-Precategory C l2)
+    (z : obj-Large-Precategory C l3)
+    (f : hom-Large-Precategory C y x)
+    (g : hom-Large-Precategory C z x) →
+    (w : obj-Large-Precategory C l4)
+    (p : hom-Large-Precategory C w y) →
+    (q : hom-Large-Precategory C w z) →
+    comp-hom-Large-Precategory C f p ＝ comp-hom-Large-Precategory C g q →
+    UU (α l1 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔ β l1 l4)
+  is-pullback-Large-Precategory x y z f g w p q _ =
+    (w' : obj-Large-Precategory C l1) →
+    (p' : hom-Large-Precategory C w' y) →
+    (q' : hom-Large-Precategory C w' z) →
+    comp-hom-Large-Precategory C f p' ＝ comp-hom-Large-Precategory C g q' →
+    ∃!
+      ( hom-Large-Precategory C w' w)
+      ( λ h →
+        ( comp-hom-Large-Precategory C p h ＝ p') ×
+        ( comp-hom-Large-Precategory C q h ＝ q'))
+
+  pullback-Large-Precategory :
+    (x : obj-Large-Precategory C l1) →
+    (y : obj-Large-Precategory C l2) →
+    (z : obj-Large-Precategory C l3) →
+    hom-Large-Precategory C y x →
+    hom-Large-Precategory C z x →
+    UU (α l1 ⊔ α l4 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔
+        β l1 l4 ⊔ β l4 l1 ⊔ β l4 l2 ⊔ β l4 l3)
+  pullback-Large-Precategory x y z f g =
+    Σ (obj-Large-Precategory C l4) λ w →
+    Σ (hom-Large-Precategory C w y) λ p →
+    Σ (hom-Large-Precategory C w z) λ q →
+    Σ (comp-hom-Large-Precategory C f p
+    ＝ comp-hom-Large-Precategory C g q) λ α →
+      is-pullback-Large-Precategory x y z f g w p q α
+
+  has-all-pullbacks-Large-Precategory :
+    UU (α l1 ⊔ α l2 ⊔ α l3 ⊔ α l4 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔
+        β l1 l4 ⊔ β l2 l1 ⊔ β l3 l1 ⊔ β l4 l1 ⊔ β l4 l2 ⊔ β l4 l3)
+  has-all-pullbacks-Large-Precategory =
+    (x : obj-Large-Precategory C l1) →
+    (y : obj-Large-Precategory C l2) →
+    (z : obj-Large-Precategory C l3) →
+    (f : hom-Large-Precategory C y x) →
+    (g : hom-Large-Precategory C z x) →
+    pullback-Large-Precategory x y z f g
+
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β) {l1 l2 : Level}
+  (t : has-all-pullbacks-Large-Precategory C)
+  (x y z : obj-Large-Precategory C l1)
+  (f : hom-Large-Precategory C y x)
+  (g : hom-Large-Precategory C z x)
+  where
+
+  object-pullback-Large-Precategory : obj-Large-Precategory C l2
+  object-pullback-Large-Precategory = pr1 (t x y z f g)
+
+  pr1-pullback-Large-Precategory :
+    hom-Large-Precategory C object-pullback-Large-Precategory y
+  pr1-pullback-Large-Precategory = pr1 (pr2 (t x y z f g))
+
+  pr2-pullback-Large-Precategory :
+    hom-Large-Precategory C object-pullback-Large-Precategory z
+  pr2-pullback-Large-Precategory = pr1 (pr2 (pr2 (t x y z f g)))
+
+  pullback-square-Large-Precategory-comm :
+    comp-hom-Large-Precategory C f pr1-pullback-Large-Precategory ＝
+    comp-hom-Large-Precategory C g pr2-pullback-Large-Precategory
+  pullback-square-Large-Precategory-comm = pr1 (pr2 (pr2 (pr2 (t x y z f g))))
+
+  module _
+    (w' : obj-Large-Precategory C l1)
+    (p' : hom-Large-Precategory C w' y)
+    (q' : hom-Large-Precategory C w' z)
+    (ε : comp-hom-Large-Precategory C f p'
+      ＝ comp-hom-Large-Precategory C g q')
+    where
+
+    morphism-into-pullback-Large-Precategory :
+      hom-Large-Precategory C w' object-pullback-Large-Precategory
+    morphism-into-pullback-Large-Precategory =
+      pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε))
+
+    morphism-into-pullback-comm-pr1-Large-Precategory :
+      comp-hom-Large-Precategory C
+        pr1-pullback-Large-Precategory
+        morphism-into-pullback-Large-Precategory ＝
+      p'
+    morphism-into-pullback-comm-pr1-Large-Precategory =
+      pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε)))
+
+    morphism-into-pullback-comm-pr2-Large-Precategory :
+      comp-hom-Large-Precategory C
+        pr2-pullback-Large-Precategory
+        morphism-into-pullback-Large-Precategory ＝
+      q'
+    morphism-into-pullback-comm-pr2-Large-Precategory =
+      pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε)))
+
+    is-unique-morphism-into-pullback-Large-Precategory :
+      (h' : hom-Large-Precategory C w' object-pullback-Large-Precategory) →
+      comp-hom-Large-Precategory C pr1-pullback-Large-Precategory h' ＝ p' →
+      comp-hom-Large-Precategory C pr2-pullback-Large-Precategory h' ＝ q' →
+      morphism-into-pullback-Large-Precategory ＝ h'
+    is-unique-morphism-into-pullback-Large-Precategory h' η θ =
+      ap
+        ( pr1)
+        ( pr2 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε) (h' , η , θ))
+
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  {l1 l2 l3 l4 : Level} (C : Large-Precategory α β)
+  (x : obj-Large-Precategory C l1)
+  (y : obj-Large-Precategory C l2)
+  (z : obj-Large-Precategory C l3)
+  (f : hom-Large-Precategory C y x)
+  (g : hom-Large-Precategory C z x)
+  (w : obj-Large-Precategory C l4)
+  (p : hom-Large-Precategory C w y)
+  (q : hom-Large-Precategory C w z)
+  (ε : comp-hom-Large-Precategory C f p ＝ comp-hom-Large-Precategory C g q)
+  where
+
+  is-prop-is-pullback-Large-Precategory :
+    is-prop (is-pullback-Large-Precategory C x y z f g w p q ε)
+  is-prop-is-pullback-Large-Precategory =
+    is-prop-Π³ (λ w' p' q' → is-prop-function-type is-property-is-contr)
+
+  is-pullback-prop-Large-Precategory :
+    Prop (α l1 ⊔ β l1 l1 ⊔ β l1 l2 ⊔ β l1 l3 ⊔ β l1 l4)
+  pr1 is-pullback-prop-Large-Precategory =
+    is-pullback-Large-Precategory C x y z f g w p q ε
+  pr2 is-pullback-prop-Large-Precategory =
+    is-prop-is-pullback-Large-Precategory
+```
diff --git a/src/category-theory/pullbacks-in-precategories.lagda.md b/src/category-theory/pullbacks-in-precategories.lagda.md
index 6a5d2efeb8..e529c81d9a 100644
--- a/src/category-theory/pullbacks-in-precategories.lagda.md
+++ b/src/category-theory/pullbacks-in-precategories.lagda.md
@@ -27,12 +27,12 @@ A pullback of two morphisms `f : hom y x` and `g : hom z x` in a category `C`
 consists of:
 
 - an object `w`
-- morphisms `p₁ : hom w y` and `p₂ : hom w z` such that
-- `f ∘ p₁ = g ∘ p₂` together with the universal property that for every object
-  `w'` and pair of morphisms `p₁' : hom w' y` and `p₂' : hom w' z` such that
-  `f ∘ p₁' = g ∘ p₂'` there exists a unique morphism `h : hom w' w` such that
-- `p₁ ∘ h = p₁'`
-- `p₂ ∘ h = p₂'`.
+- morphisms `p : hom w y` and `q : hom w z` such that
+- `f ∘ p = g ∘ q` together with the universal property that for every object
+  `w'` and pair of morphisms `p' : hom w' y` and `q' : hom w' z` such that
+  `f ∘ p' = g ∘ q'` there exists a unique morphism `h : hom w' w` such that
+- `p ∘ h = p'`
+- `q ∘ h = q'`.
 
 We say that `C` has all pullbacks if there is a choice of a pullback for each
 object `x` and pair of morphisms into `x` in `C`.
@@ -49,20 +49,20 @@ module _
     (f : hom-Precategory C y x) →
     (g : hom-Precategory C z x) →
     (w : obj-Precategory C) →
-    (p₁ : hom-Precategory C w y) →
-    (p₂ : hom-Precategory C w z) →
-    comp-hom-Precategory C f p₁ ＝ comp-hom-Precategory C g p₂ →
+    (p : hom-Precategory C w y) →
+    (q : hom-Precategory C w z) →
+    comp-hom-Precategory C f p ＝ comp-hom-Precategory C g q →
     UU (l1 ⊔ l2)
-  is-pullback-Precategory x y z f g w p₁ p₂ _ =
+  is-pullback-Precategory x y z f g w p q _ =
     (w' : obj-Precategory C) →
-    (p₁' : hom-Precategory C w' y) →
-    (p₂' : hom-Precategory C w' z) →
-    comp-hom-Precategory C f p₁' ＝ comp-hom-Precategory C g p₂' →
+    (p' : hom-Precategory C w' y) →
+    (q' : hom-Precategory C w' z) →
+    comp-hom-Precategory C f p' ＝ comp-hom-Precategory C g q' →
     ∃!
       ( hom-Precategory C w' w)
       ( λ h →
-        ( comp-hom-Precategory C p₁ h ＝ p₁') ×
-        ( comp-hom-Precategory C p₂ h ＝ p₂'))
+        ( comp-hom-Precategory C p h ＝ p') ×
+        ( comp-hom-Precategory C q h ＝ q'))
 
   pullback-Precategory :
     (x y z : obj-Precategory C) →
@@ -71,13 +71,13 @@ module _
     UU (l1 ⊔ l2)
   pullback-Precategory x y z f g =
     Σ (obj-Precategory C) λ w →
-    Σ (hom-Precategory C w y) λ p₁ →
-    Σ (hom-Precategory C w z) λ p₂ →
-    Σ (comp-hom-Precategory C f p₁ ＝ comp-hom-Precategory C g p₂) λ α →
-      is-pullback-Precategory x y z f g w p₁ p₂ α
+    Σ (hom-Precategory C w y) λ p →
+    Σ (hom-Precategory C w z) λ q →
+    Σ (comp-hom-Precategory C f p ＝ comp-hom-Precategory C g q) λ α →
+      is-pullback-Precategory x y z f g w p q α
 
-  has-all-pullback-Precategory : UU (l1 ⊔ l2)
-  has-all-pullback-Precategory =
+  has-all-pullbacks-Precategory : UU (l1 ⊔ l2)
+  has-all-pullbacks-Precategory =
     (x y z : obj-Precategory C) →
     (f : hom-Precategory C y x) →
     (g : hom-Precategory C z x) →
@@ -85,7 +85,7 @@ module _
 
 module _
   {l1 l2 : Level} (C : Precategory l1 l2)
-  (t : has-all-pullback-Precategory C)
+  (t : has-all-pullbacks-Precategory C)
   (x y z : obj-Precategory C)
   (f : hom-Precategory C y x)
   (g : hom-Precategory C z x)
@@ -109,41 +109,41 @@ module _
 
   module _
     (w' : obj-Precategory C)
-    (p₁' : hom-Precategory C w' y)
-    (p₂' : hom-Precategory C w' z)
-    (α : comp-hom-Precategory C f p₁' ＝ comp-hom-Precategory C g p₂')
+    (p' : hom-Precategory C w' y)
+    (q' : hom-Precategory C w' z)
+    (ε : comp-hom-Precategory C f p' ＝ comp-hom-Precategory C g q')
     where
 
     morphism-into-pullback-Precategory :
       hom-Precategory C w' object-pullback-Precategory
     morphism-into-pullback-Precategory =
-      pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))
+      pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε))
 
-    morphism-into-pullback-comm-pr1 :
+    morphism-into-pullback-comm-pr1-Precategory :
       comp-hom-Precategory C
         pr1-pullback-Precategory
         morphism-into-pullback-Precategory ＝
-      p₁'
-    morphism-into-pullback-comm-pr1 =
-      pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)))
+      p'
+    morphism-into-pullback-comm-pr1-Precategory =
+      pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε)))
 
-    morphism-into-pullback-comm-pr2 :
+    morphism-into-pullback-comm-pr2-Precategory :
       comp-hom-Precategory C
         pr2-pullback-Precategory
         morphism-into-pullback-Precategory ＝
-      p₂'
-    morphism-into-pullback-comm-pr2 =
-      pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)))
+      q'
+    morphism-into-pullback-comm-pr2-Precategory =
+      pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε)))
 
     is-unique-morphism-into-pullback-Precategory :
       (h' : hom-Precategory C w' object-pullback-Precategory) →
-      comp-hom-Precategory C pr1-pullback-Precategory h' ＝ p₁' →
-      comp-hom-Precategory C pr2-pullback-Precategory h' ＝ p₂' →
+      comp-hom-Precategory C pr1-pullback-Precategory h' ＝ p' →
+      comp-hom-Precategory C pr2-pullback-Precategory h' ＝ q' →
       morphism-into-pullback-Precategory ＝ h'
-    is-unique-morphism-into-pullback-Precategory h' α₁ α₂ =
+    is-unique-morphism-into-pullback-Precategory h' η θ =
       ap
         ( pr1)
-        ( pr2 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α) (h' , α₁ , α₂))
+        ( pr2 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p' q' ε) (h' , η , θ))
 
 module _
   {l1 l2 : Level} (C : Precategory l1 l2)
@@ -151,19 +151,19 @@ module _
   (f : hom-Precategory C y x)
   (g : hom-Precategory C z x)
   (w : obj-Precategory C)
-  (p₁ : hom-Precategory C w y)
-  (p₂ : hom-Precategory C w z)
-  (α : comp-hom-Precategory C f p₁ ＝ comp-hom-Precategory C g p₂)
+  (p : hom-Precategory C w y)
+  (q : hom-Precategory C w z)
+  (ε : comp-hom-Precategory C f p ＝ comp-hom-Precategory C g q)
   where
 
   is-prop-is-pullback-Precategory :
-    is-prop (is-pullback-Precategory C x y z f g w p₁ p₂ α)
+    is-prop (is-pullback-Precategory C x y z f g w p q ε)
   is-prop-is-pullback-Precategory =
-    is-prop-Π³ (λ w' p₁' p₂' → is-prop-function-type is-property-is-contr)
+    is-prop-Π³ (λ w' p' q' → is-prop-function-type is-property-is-contr)
 
   is-pullback-prop-Precategory : Prop (l1 ⊔ l2)
   pr1 is-pullback-prop-Precategory =
-    is-pullback-Precategory C x y z f g w p₁ p₂ α
+    is-pullback-Precategory C x y z f g w p q ε
   pr2 is-pullback-prop-Precategory =
     is-prop-is-pullback-Precategory
 ```
diff --git a/src/category-theory/subobject-classifier-in-large-precategories.lagda.md b/src/category-theory/subobject-classifier-in-large-precategories.lagda.md
new file mode 100644
index 0000000000..a9fa34245e
--- /dev/null
+++ b/src/category-theory/subobject-classifier-in-large-precategories.lagda.md
@@ -0,0 +1,29 @@
+# The subobject classifier in large precategories
+
+```agda
+module category-theory.subobject-classifier-in-large-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.large-precategories
+open import category-theory.monomorphisms-in-large-precategories
+
+open import foundation.equivalence-relations
+open import foundation.equivalences
+open import foundation.universe-levels
+```
+
+</details>
+
+## Definition
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β) {l1 l2 : Level} (l3 : Level)
+  (S : obj-Large-Precategory C l1) (X : obj-Large-Precategory C l2)
+  (m : mono-Large-Precategory C l3 S X)
+  where
+```