diff --git a/src/Cat/Functor/Adjoint/Epireflective.lagda.md b/src/Cat/Functor/Adjoint/Epireflective.lagda.md
index a0198bccd..e4bfedf26 100644
--- a/src/Cat/Functor/Adjoint/Epireflective.lagda.md
+++ b/src/Cat/Functor/Adjoint/Epireflective.lagda.md
@@ -180,10 +180,7 @@ diagram:
    X &&&& {R(L(X))} \\
    && I \\
    {R(L(X))} &&&& {R(L(R(L(X))))} \\
-   && {R(L(I))} \\
-   \\
-   \\
-   && \bullet
+   && {R(L(I))}
    \arrow["{\eta_{X}}", no head, from=1-1, to=1-5]
    \arrow["e"', two heads, from=1-1, to=2-3]
    \arrow["{\eta_{X}}"', from=1-1, to=3-1]
diff --git a/src/Cat/Morphism/Orthogonal.lagda.md b/src/Cat/Morphism/Orthogonal.lagda.md
index ed5a5fd9b..4a9a660cc 100644
--- a/src/Cat/Morphism/Orthogonal.lagda.md
+++ b/src/Cat/Morphism/Orthogonal.lagda.md
@@ -15,7 +15,7 @@ import Cat.Reasoning as Cr
 module Cat.Morphism.Orthogonal where
 ```
 
-# Orthogonal maps {defines="left-orthogonal right-orthogonal"}
+# Orthogonal maps {defines="left-orthogonal right-orthogonal orthogonality"}
 
 A pair of maps $f : a \to b$ and $g : c \ to d$ are called
 **orthogonal**, written $f \ortho g$^[Though hang tight for a note on
@@ -36,32 +36,56 @@ diagram like
 ~~~
 
 the space of arrows $c \to b$ (dashed) which commute with everything is
-contractible.
+contractible. We refer to the type of these dashed arrows as a
+`Lifting`{.Agda}, and this type is parametrised over all maps in the
+square.
 
 <!--
 ```agda
 module _ {o ℓ} (C : Precategory o ℓ) where
-  private module C = Cr C
+  private
+    module C = Cr C
+    variable
+      a b c d : ⌞ C ⌟
+      f g h u v : C.Hom a b
+  open C using (Ob ; Hom ; _∘_ ; _≅_)
 ```
 -->
 
 ```agda
-  m⊥m : ∀ {a b c d} → C.Hom a b → C.Hom c d → Type _
+  Lifting
+    : (f : Hom a b) (g : Hom c d) (u : Hom a c) (v : Hom b d)
+    → Type _
+  Lifting f g u v = Σ[ w ∈ Hom _ _ ] w ∘ f ≡ u × g ∘ w ≡ v
+
+  m⊥m : Hom a b → Hom c d → Type _
   m⊥m {b = b} {c = c} f g =
-    ∀ {u v} → v C.∘ f ≡ g C.∘ u
-    → is-contr (Σ[ w ∈ C.Hom b c ] ((w C.∘ f ≡ u) × (g C.∘ w ≡ v)))
+    ∀ {u v} → v ∘ f ≡ g ∘ u
+    → is-contr (Lifting f g u v)
 ```
 
+:::{.definition #lifts-against}
+In some of the proofs below, we'll also need a name for a weakening of
+orthogonality, where the requirement that lifts are unique is dropped.
+We say $f$ *lifts against* $g$ if there is a map assigning lifts to
+every commutative squares with opposing $f$ and $g$ faces, as above.
+
+```agda
+  lifts-against : (f : Hom a b) (g : Hom c d) → Type _
+  lifts-against f g = ∀ {u v} → v ∘ f ≡ g ∘ u → Lifting f g u v
+```
+:::
+
 We also outline concepts of a map being orthogonal to an object, which
 is informally written $f \ortho X$, and an object being orthogonal to a
 map $Y \ortho f$.
 
 ```agda
-  m⊥o : ∀ {a b} → C.Hom a b → C.Ob → Type _
-  m⊥o {A} {B} f X = (a : C.Hom A X) → is-contr (Σ[ b ∈ C.Hom B X ] (b C.∘ f ≡ a))
+  m⊥o : Hom a b → ⌞ C ⌟ → Type _
+  m⊥o {a} {b} f X = (a : Hom a X) → is-contr (Σ[ b ∈ Hom b X ] (b ∘ f ≡ a))
 
-  o⊥m : ∀ {a b} → C.Ob → C.Hom a b → Type _
-  o⊥m {A} {B} Y f = (c : C.Hom Y B) → is-contr (Σ[ d ∈ C.Hom Y A ] (f C.∘ d ≡ c))
+  o⊥m : ⌞ C ⌟ → Hom a b → Type _
+  o⊥m {a} {b} Y f = (c : Hom Y b) → is-contr (Σ[ d ∈ Hom Y a ] (f ∘ d ≡ c))
 ```
 
 :::{.note}
@@ -86,7 +110,7 @@ The proof is mostly a calculation, so we present it without a lot of comment.
 
 ```agda
   object-orthogonal-!-orthogonal
-    : ∀ {A B X} (T : Terminal C) (f : C.Hom A B) → m⊥o f X ≃ m⊥m f (! T)
+    : ∀ {X} (T : Terminal C) (f : Hom a b) → m⊥o f X ≃ m⊥m f (! T)
   object-orthogonal-!-orthogonal {X = X} T f =
     prop-ext (hlevel 1) (hlevel 1) to from
     where
@@ -107,21 +131,21 @@ then $f \ortho Y$. Of course, this is immediate in categories, but it
 holds in the generality of precategories.
 
 ```agda
-  m⊥-iso : ∀ {a b} {X Y} (f : C.Hom a b) → X C.≅ Y → m⊥o f X → m⊥o f Y
+  m⊥-iso : ∀ {a b} {X Y} (f : Hom a b) → X ≅ Y → m⊥o f X → m⊥o f Y
 ```
 
 <!--
 ```agda
   m⊥-iso f x≅y f⊥X a =
     contr
-      ( g.to C.∘ contr' .centre .fst
+      ( g.to ∘ contr' .centre .fst
       , C.pullr (contr' .centre .snd) ∙ C.cancell g.invl )
       λ x → Σ-prop-path! $
-        ap₂ C._∘_ refl (ap fst (contr' .paths (g.from C.∘ x .fst , C.pullr (x .snd))))
+        ap₂ _∘_ refl (ap fst (contr' .paths (g.from ∘ x .fst , C.pullr (x .snd))))
         ∙ C.cancell g.invl
     where
       module g = C._≅_ x≅y
-      contr' = f⊥X (g.from C.∘ a)
+      contr' = f⊥X (g.from ∘ a)
 ```
 -->
 
@@ -129,7 +153,7 @@ A slightly more interesting lemma is that, if $f$ is orthogonal to
 itself, then it is an isomorphism:
 
 ```agda
-  self-orthogonal→invertible : ∀ {a b} (f : C.Hom a b) → m⊥m f f → C.is-invertible f
+  self-orthogonal→invertible : ∀ {a b} (f : Hom a b) → m⊥m f f → C.is-invertible f
   self-orthogonal→invertible f f⊥f =
     C.make-invertible (gpq .fst) (gpq .snd .snd) (gpq .snd .fst)
     where
@@ -141,15 +165,15 @@ $l$ and $k$ are both lifts of the outer square.
 
 ~~~{.quiver}
 \begin{tikzcd}
-	a && b \\
-	\\
-	c && d
-	\arrow["f", from=1-1, to=1-3]
-	\arrow["u"', from=1-1, to=3-1]
-	\arrow["l"', shift right, from=1-3, to=3-1]
-	\arrow["k", shift left, from=1-3, to=3-1]
-	\arrow["v", from=1-3, to=3-3]
-	\arrow["g"', from=3-1, to=3-3]
+  a && b \\
+  \\
+  c && d
+  \arrow["f", from=1-1, to=1-3]
+  \arrow["u"', from=1-1, to=3-1]
+  \arrow["l"', shift right, from=1-3, to=3-1]
+  \arrow["k", shift left, from=1-3, to=3-1]
+  \arrow["v", from=1-3, to=3-3]
+  \arrow["g"', from=3-1, to=3-3]
 \end{tikzcd}
 ~~~
 
@@ -158,11 +182,7 @@ type of lifts of such a square is a proposition.
 
 ```agda
   left-epic→lift-is-prop
-    : ∀ {a b c d}
-    → {f : C.Hom a b} {g : C.Hom c d} {u : C.Hom a c} {v : C.Hom b d}
-    → C.is-epic f
-    → v C.∘ f ≡ g C.∘ u
-    → is-prop (Σ[ w ∈ C.Hom b c ] ((w C.∘ f ≡ u) × (g C.∘ w ≡ v)))
+    : C.is-epic f → v C.∘ f ≡ g C.∘ u → is-prop (Lifting f g u v)
   left-epic→lift-is-prop f-epi vf=gu (l , lf=u , _) (k , kf=u , _) =
     Σ-prop-path! (f-epi l k (lf=u ∙ sym kf=u))
 ```
@@ -172,11 +192,7 @@ a propostion.
 
 ```agda
   right-monic→lift-is-prop
-    : ∀ {a b c d}
-    → {f : C.Hom a b} {g : C.Hom c d} {u : C.Hom a c} {v : C.Hom b d}
-    → C.is-monic g
-    → v C.∘ f ≡ g C.∘ u
-    → is-prop (Σ[ w ∈ C.Hom b c ] ((w C.∘ f ≡ u) × (g C.∘ w ≡ v)))
+    : C.is-monic g → v C.∘ f ≡ g C.∘ u → is-prop (Lifting f g u v)
   right-monic→lift-is-prop g-mono vf=gu (l , _ , gl=v) (k , _ , gk=v) =
     Σ-prop-path! (g-mono l k (gl=v ∙ sym gk=v))
 ```
@@ -186,18 +202,14 @@ to find _any_ lift to establish that $f \bot g$.
 
 ```agda
   left-epic-lift→orthogonal
-    : ∀ {a b c d} {f : C.Hom a b}
-    → C.is-epic f → (g : C.Hom c d)
-    → (∀ {u v} → v C.∘ f ≡ g C.∘ u → Σ[ w ∈ C.Hom b c ] ((w C.∘ f ≡ u) × (g C.∘ w ≡ v)))
-    → m⊥m f g
-  left-epic-lift→orthogonal f-epi g lifts vf=gu =
+    : (g : C.Hom c d)
+    → C.is-epic f → lifts-against f g → m⊥m f g
+  left-epic-lift→orthogonal g f-epi lifts vf=gu =
     is-prop∙→is-contr (left-epic→lift-is-prop f-epi vf=gu) (lifts vf=gu)
 
   right-monic-lift→orthogonal
-    : ∀ {a b c d} {g : C.Hom c d}
-    → (f : C.Hom a b) → C.is-monic g
-    → (∀ {u v} → v C.∘ f ≡ g C.∘ u → Σ[ w ∈ C.Hom b c ] ((w C.∘ f ≡ u) × (g C.∘ w ≡ v)))
-    → m⊥m f g
+    : (f : C.Hom a b)
+    → C.is-monic g → lifts-against f g → m⊥m f g
   right-monic-lift→orthogonal f g-mono lifts vf=gu =
     is-prop∙→is-contr (right-monic→lift-is-prop g-mono vf=gu) (lifts vf=gu)
 ```
@@ -205,15 +217,8 @@ to find _any_ lift to establish that $f \bot g$.
 Isomorphisms are left and right orthogonal to every other morphism.
 
 ```agda
-  invertible→left-orthogonal
-    : ∀ {a b c d} {f : C.Hom a b}
-    → C.is-invertible f → (g : C.Hom c d)
-    → m⊥m f g
-
-  invertible→right-orthogonal
-    : ∀ {a b c d} {g : C.Hom c d}
-    → (f : C.Hom a b) → C.is-invertible g
-    → m⊥m f g
+  invertible→left-orthogonal  : (g : C.Hom c d) → C.is-invertible f → m⊥m f g
+  invertible→right-orthogonal : (f : C.Hom a b) → C.is-invertible g → m⊥m f g
 ```
 
 We will focus our attention on the left orthogonal case, as the proof
@@ -240,14 +245,14 @@ diagonal:
 A short calculation verifies that $u \circ f^{-1}$ is indeed a lift.
 
 ```agda
-  invertible→left-orthogonal {f = f} f-inv g =
-    left-epic-lift→orthogonal (C.invertible→epic f-inv) g λ {u} {v} vf=gu →
-      u C.∘ f.inv ,
+  invertible→left-orthogonal {f = f} g f-inv =
+    left-epic-lift→orthogonal g (C.invertible→epic f-inv) λ {u} {v} vf=gu →
+      u ∘ f.inv ,
       C.cancelr f.invr ,
       Equiv.from
-        (g C.∘ u C.∘ f.inv ≡ v   ≃⟨ C.reassocl e⁻¹ ∙e C.pre-invr f-inv ⟩
-         g C.∘ u ≡ v C.∘ f       ≃⟨ sym-equiv ⟩
-         v C.∘ f ≡ g C.∘ u       ≃∎)
+        (g ∘ u ∘ f.inv ≡ v   ≃⟨ C.reassocl e⁻¹ ∙e C.pre-invr f-inv ⟩
+         g ∘ u ≡ v ∘ f       ≃⟨ sym-equiv ⟩
+         v ∘ f ≡ g ∘ u       ≃∎)
         vf=gu
     where module f = C.is-invertible f-inv
 ```
@@ -259,16 +264,110 @@ so we omit the details.
 ```agda
   invertible→right-orthogonal {g = g} f g-inv =
     right-monic-lift→orthogonal f (C.invertible→monic g-inv) λ {u} {v} vf=gu →
-      g.inv C.∘ v ,
+      g.inv ∘ v ,
       Equiv.from
-        ((g.inv C.∘ v) C.∘ f ≡ u ≃⟨ C.reassocl ∙e C.pre-invl g-inv ⟩
-          v C.∘ f ≡ g C.∘ u      ≃∎)
+        ((g.inv ∘ v) ∘ f ≡ u ≃⟨ C.reassocl ∙e C.pre-invl g-inv ⟩
+          v ∘ f ≡ g ∘ u      ≃∎)
         vf=gu ,
       C.cancell g.invl
     where module g = C.is-invertible g-inv
 ```
 </details>
 
+<!--
+```agda
+  orthogonal→lifts-against : m⊥m f g → lifts-against f g
+  orthogonal→lifts-against o p = o p .centre
+```
+-->
+
+We also have the following two properties, which state that "lifting
+against" is, as a property of morphisms, closed under composition on
+both the left and the right. To understand the proof, it's helpful to
+visualise the inputs in a diagram. Suppose we have $f : b \to c$, $g : a
+\to b$, $h : x \to y$, and assume that both $f$ and $g$ lift against
+$h$. Showing that $fg$ lifts against $h$ amounts to finding a diagonal
+for the rectangle
+
+~~~{.quiver}
+\[\begin{tikzcd}[ampersand replacement=\&]
+  a \&\& b \&\& c \\
+  \\
+  x \&\&\&\& y
+  \arrow["g", from=1-1, to=1-3]
+  \arrow["u"', from=1-1, to=3-1]
+  \arrow["f", from=1-3, to=1-5]
+  \arrow["v", from=1-5, to=3-5]
+  \arrow["h"', from=3-1, to=3-5]
+\end{tikzcd}\]
+~~~
+
+under the assumption that $vfg = hu$. We'll populate this diagram a bit
+by observing that, by composing the $f$ and $v$ edges together, we have
+a commutative square with faces $g$, $vf$, $u$ and $h$ --- and since $g$
+lifts against $h$, this implies that we have a diagonal map $w$, which
+appears dashed in
+
+~~~{.quiver}
+\[\begin{tikzcd}[ampersand replacement=\&]
+  a \&\& b \&\& c \\
+  \\
+  x \&\&\&\& {y.}
+  \arrow["g", from=1-1, to=1-3]
+  \arrow["u"', from=1-1, to=3-1]
+  \arrow["f", from=1-3, to=1-5]
+  \arrow["w"', dashed, from=1-3, to=3-1]
+  \arrow["v", from=1-5, to=3-5]
+  \arrow["h"', from=3-1, to=3-5]
+\end{tikzcd}\]
+~~~
+
+This map satisfies $wg = u$, and, importantly, $hw = vf$. This latter
+equation implies that we can now treat the right half of the diagram as
+another square, with faces $f$, $h$, $w$, and $v$. Since $f$ *also*
+lifts against $h$, this implies that we can find the *dotted* map $t$ in
+the diagram
+
+~~~{.quiver}
+\[\begin{tikzcd}[ampersand replacement=\&]
+  a \&\& b \&\& c \\
+  \\
+  x \&\&\&\& y
+  \arrow["g", from=1-1, to=1-3]
+  \arrow["u"', from=1-1, to=3-1]
+  \arrow["f", from=1-3, to=1-5]
+  \arrow["w"', dashed, from=1-3, to=3-1]
+  \arrow["t", dotted, from=1-5, to=3-1]
+  \arrow["v", from=1-5, to=3-5]
+  \arrow["h"', from=3-1, to=3-5]
+\end{tikzcd}\]
+~~~
+
+satisfying $tf = w$ and $mt = v$. The map $t$ fits the *type* of fillers
+for our original rectangle, but we must still show that it makes both
+triangles commute. But this is easy: we have $tfg = wg = u$ by a short
+calculation and $ht = w$ immediately.
+
+```agda
+  ∘l-lifts-against : lifts-against f h → lifts-against g h → lifts-against (f ∘ g) h
+  ∘l-lifts-against f-lifts g-lifts vfg=hu =
+    let (w , wg=u , hw=vf) = g-lifts (C.reassocl.from vfg=hu)
+        (t , tf=w , ht=v)  = f-lifts (sym hw=vf)
+    in t , C.pulll tf=w ∙ wg=u , ht=v
+```
+
+This proof dualises almost term-for-term the case where we're composing
+on the bottom face, i.e., when we have some $f$ which lifts against both
+$g$ and $h$, and we want to show $f$ lifts against $gh$.
+
+```agda
+  ∘r-lifts-against : lifts-against f g → lifts-against f h → lifts-against f (g ∘ h)
+  ∘r-lifts-against f-lifts g-lifts ve=fgu =
+    let (w , we=gu , fw=v) = f-lifts (C.reassocr.to ve=fgu)
+        (t , te=u , gt=w)  = g-lifts we=gu
+    in t , te=u , C.pullr gt=w ∙ fw=v
+```
+
 ## Regarding reflections
 
 <!--
@@ -388,7 +487,7 @@ the subcategory:
   orthogonal-to-ηs→in-subcategory {X} ortho =
     C.make-invertible x lemma (ortho X C.id .centre .snd)
     where
-      x = ortho X (C .Precategory.id) .centre .fst
+      x = ortho X C.id .centre .fst
       lemma = unit.η _ C.∘ x             ≡⟨ unit.is-natural _ _ _ ⟩
               ιr.₁ x C.∘ unit.η (ιr.₀ X) ≡⟨ C.refl⟩∘⟨ η-comonad-commute r⊣ι ι-ff ⟩
               ιr.₁ x C.∘ ιr.₁ (unit.η X) ≡⟨ ιr.annihilate (ortho X C.id .centre .snd) ⟩
diff --git a/src/Cat/Morphism/Strong/Epi.lagda.md b/src/Cat/Morphism/Strong/Epi.lagda.md
index e9608074c..e971dc66d 100644
--- a/src/Cat/Morphism/Strong/Epi.lagda.md
+++ b/src/Cat/Morphism/Strong/Epi.lagda.md
@@ -56,7 +56,7 @@ lifts→is-strong-epi
   : ∀ {a b} {f : Hom a b}
   → is-epic f
   → ( ∀ {c d} (m : c ↪ d) {u} {v} → v ∘ f ≡ m .mor ∘ u
-    → Σ[ w ∈ Hom b c ] ((w ∘ f ≡ u) × (m .mor ∘ w ≡ v)))
+    → Lifting C f (m .mor) u v)
   → is-strong-epi f
 lifts→is-strong-epi epic lift-it = epic , λ {c} {d} mm sq →
   contr (lift-it mm sq) λ { (x , p , q) → Σ-prop-path!
@@ -95,10 +95,29 @@ by commutativity of the lower triangles we have $g\alpha = u = g\beta$.
 
 ## Properties
 
-The proofs here are transcribed from [@Borceux:vol1, §4.3]. Strong
-epimorphisms are closed under composition, for suppose that $f$ and $g$
-are strong epics, and $m$ is the monomorphism to lift against. Fit them
-in a skewed commutative _rectangle_ like
+The first thing we show is that strong epimorphisms are closed under
+composition. It will suffice to show that the composite $fg$ of a pair
+of strong epimorphisms is epic, and that it [[lifts against]] every
+monomorphism. But this is just a pasting of existing results: we already
+know that being epic is `closed under composition`{.Agda ident=epic-∘},
+and that so is `lifting against a given map`{.Agda
+ident=∘l-lifts-against} --- in this case, an arbitrary monomorphism $m$.
+
+```agda
+strong-epi-∘
+  : ∀ {a b c} (f : Hom b c) (g : Hom a b)
+  → is-strong-epi f
+  → is-strong-epi g
+  → is-strong-epi (f ∘ g)
+strong-epi-∘ f g (f-epi , f-str) (g-epi , g-str) =
+  lifts→is-strong-epi (epic-∘ f-epi g-epi) λ e → ∘l-lifts-against C
+    (orthogonal→lifts-against C (f-str e))
+    (orthogonal→lifts-against C (g-str e))
+```
+
+Additionally, there is a partial converse to this result: If the
+composite $gf$ is a strong epi, then $g$ is, too! It'll help to diagram
+the situation:
 
 ~~~{.quiver}
 \[\begin{tikzcd}
@@ -110,43 +129,14 @@ in a skewed commutative _rectangle_ like
   \arrow["u"', from=1-1, to=3-1]
   \arrow["z"', hook, from=3-1, to=3-5]
   \arrow["v", from=1-5, to=3-5]
-  \arrow["w"{description}, dashed, from=1-3, to=3-1]
-  \arrow["t"{description}, dashed, from=1-5, to=3-1]
+  \arrow["w"', dashed, from=1-3, to=3-1]
+  \arrow["t", dashed, from=1-5, to=3-1]
 \end{tikzcd}\]
 ~~~
 
-By considering most of the right half as a single, weirdly-shaped square
-(the $vfg = zu$ commutative "square"), we get an intermediate lift $w :
-b \to d$ such that $wg = u$ and $zw=vf$ --- such that $z$, $w$, $f$, and
-$v$ organise into the faces of a lifting diagram, too$ Since $f$ is a
-strong epic, we have a _second_ lift $t : c \to d$, now satisfying
-$tf=w$ and $zt=v$. A quick calculation, implicit in the diagram, shows
-that $t$ is precisely the lift for $fg$ against $z$.
-
-```agda
-strong-epi-∘
-  : ∀ {a b c} (f : Hom b c) (g : Hom a b)
-  → is-strong-epi f
-  → is-strong-epi g
-  → is-strong-epi (f ∘ g)
-strong-epi-∘ f g (f-epi , f-str) (g-epi , g-str) =
-  lifts→is-strong-epi fg-epi fg-str
-  where
-    fg-epi : is-epic (f ∘ g)
-    fg-epi = epic-∘ f-epi g-epi
-
-    fg-str : ∀ {c d} (m : c ↪ d) {u v} → v ∘ f ∘ g ≡ m .mor ∘ u → _
-    fg-str m {u} {v} vfg=zu =
-      let (w , wg=u , mw=vf) = g-str m (reassocl.from vfg=zu) .centre
-          (t , tf=w , mt=v)  = f-str m (sym mw=vf) .centre
-      in t , pulll tf=w ∙ wg=u , mt=v
-```
-
-Additionally, there is a partial converse to this result: If the
-composite $gf$ is a strong epi, then $g$ is, too! Still thinking of the
-same diagram, suppose the whole diagram is a strong epi, and you're
-given $zw = vf$ to lift $f$ against $z$. We don't have a $u$ as before,
-but we can take $u = wg$ to get a lift $t$.
+We can now name our assumptions: we're given $zw = vf$ to lift $f$
+against $z$. We don't have a $u$ as before, but we can take $u = wg$ to
+get a lift $t$.
 
 ```agda
 strong-epi-cancelr
@@ -422,7 +412,7 @@ is-extremal-epi→is-strong-epi {a} {b} {e} lex extremal =
     module lex = Finitely-complete lex
 ```
 
-We adapt the proof from [@Borceux:vol1; §4.3.7]. After
+We adapt the proof from [@Borceux:vol1, §4.3.7]. After
 `equaliser-lifts→is-strong-epi`{.Agda}, it will suffice to construct
 _some_ lift for a square with $ve = mu$, with $m$ monic. Pull $v$ back
 along $m$ to obtain the square
@@ -506,7 +496,7 @@ invertible→strong-epi
   → is-strong-epi f
 invertible→strong-epi f-inv =
   invertible→epic f-inv , λ m →
-  invertible→left-orthogonal C f-inv (m .mor)
+  invertible→left-orthogonal C (m .mor) f-inv
 
 cast-is-strong-epi
   : ∀ {a b} {f g : Hom a b}
diff --git a/src/Cat/Morphism/Strong/Mono.lagda.md b/src/Cat/Morphism/Strong/Mono.lagda.md
index bc3d3ab0a..2975dfaf4 100644
--- a/src/Cat/Morphism/Strong/Mono.lagda.md
+++ b/src/Cat/Morphism/Strong/Mono.lagda.md
@@ -54,7 +54,7 @@ lifts→is-strong-mono
   : ∀ {c d} {f : Hom c d}
   → is-monic f
   → (∀ {a b} (e : a ↠ b) {u v} → v ∘ e .mor ≡ f ∘ u
-    → Σ[ w ∈ Hom b c ] w ∘ e .mor ≡ u × f ∘ w ≡ v)
+    → Lifting C (e .mor) f u v)
   → is-strong-mono f
 lifts→is-strong-mono monic lift-it =
   monic , λ e →
@@ -113,17 +113,9 @@ strong-mono-∘
   → is-strong-mono g
   → is-strong-mono (f ∘ g)
 strong-mono-∘ f g (f-mono , f-str) (g-mono , g-str) =
-  lifts→is-strong-mono fg-mono fg-str
-    where
-      fg-mono : is-monic (f ∘ g)
-      fg-mono = monic-∘ f-mono g-mono
-
-      fg-str : ∀ {a b} (e : a ↠ b) {u v} → v ∘ e .mor ≡ (f ∘ g) ∘ u → _
-      fg-str e {u} {v} ve=fgu =
-          let (w , we=gu , fw=v) = f-str e (reassocr.to ve=fgu) .centre
-              (t , te=u , gt=w) = g-str e we=gu .centre
-          in t , te=u , pullr gt=w ∙ fw=v
-
+  lifts→is-strong-mono (monic-∘ f-mono g-mono) λ e → ∘r-lifts-against C
+    (orthogonal→lifts-against C (f-str e))
+    (orthogonal→lifts-against C (g-str e))
 ```
 
 Like their non-strong counterparts, strong monomorphisms satisfy a