diff --git a/src/orthogonal-factorization-systems/function-classes.lagda.md b/src/orthogonal-factorization-systems/function-classes.lagda.md
index 92c46b42509..56e789dbf99 100644
--- a/src/orthogonal-factorization-systems/function-classes.lagda.md
+++ b/src/orthogonal-factorization-systems/function-classes.lagda.md
@@ -179,6 +179,11 @@ module _
   {l1 l2 : Level} (F : function-class l1 l1 l2)
   where
 
+  has-identity-maps-has-equivalences-function-class :
+    has-equivalences-function-class F → has-identity-maps-function-class F
+  has-identity-maps-has-equivalences-function-class has-equivs-F A =
+    has-equivs-F A A id is-equiv-id
+
   htpy-has-identity-maps-function-class :
     has-identity-maps-function-class F →
     {X Y : UU l1} → (p : X ＝ Y) → type-Prop (F (map-eq p))
@@ -186,18 +191,13 @@ module _
 
   has-equivalence-has-identity-maps-function-class :
     has-identity-maps-function-class F →
-    {X Y : UU l1} → (e : X ≃ Y) → type-Prop (F (map-equiv e))
+    {X Y : UU l1} (e : X ≃ Y) → type-Prop (F (map-equiv e))
   has-equivalence-has-identity-maps-function-class has-ids-F {X} {Y} e =
     tr
       ( type-Prop ∘ F)
       ( ap pr1 (is-section-eq-equiv e))
       ( htpy-has-identity-maps-function-class has-ids-F (eq-equiv X Y e))
 
-  has-identity-maps-has-equivalences-function-class :
-    has-equivalences-function-class F → has-identity-maps-function-class F
-  has-identity-maps-has-equivalences-function-class has-equivs-F A =
-    has-equivs-F A A id is-equiv-id
-
   has-equivalences-has-identity-maps-function-class :
     has-identity-maps-function-class F → has-equivalences-function-class F
   has-equivalences-has-identity-maps-function-class has-ids-F A B f is-equiv-f =
diff --git a/src/orthogonal-factorization-systems/lifting-operations.lagda.md b/src/orthogonal-factorization-systems/lifting-operations.lagda.md
index cf175564e59..be316d716d3 100644
--- a/src/orthogonal-factorization-systems/lifting-operations.lagda.md
+++ b/src/orthogonal-factorization-systems/lifting-operations.lagda.md
@@ -27,7 +27,6 @@ and `g`_ is a choice of lifting square for every commuting square
   A ------> B
   |         |
  f|         |g
-  |         |
   V         V
   X ------> Y.
 ```
@@ -36,20 +35,20 @@ Given a lifting operation we can say that `f` has a _left lifting structure_
 with respect to `g` and that `g` has a _right lifting structure_ with respect to
 `f`.
 
-## Warning
-
-This is the Curry–Howard interpretation of what is classically called _lifting
-properties_. However, these are generally additional structure on the maps. For
-the proof-irrelevant notion see
+**Warning**: This is the Curry–Howard interpretation of what is classically
+called _lifting properties_. However, these are generally additional structure
+on the maps. For the proof-irrelevant notion see
 [mere lifting properties](orthogonal-factorization-systems.mere-lifting-properties.md).
 
 ## Definition
 
-We define lifting operations to be sections of the pullback-hom.
+We define lifting operations to be [sections](foundation-core.sections.md) of
+the [pullback-hom](orthogonal-factorization-systems.pullback-hom.md).
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  {l1 l2 l3 l4 : Level}
+  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
   (f : A → X) (g : B → Y)
   where