Apply suggestions from code review

src/foundation-core/commuting-triangles-of-maps.lagda.md

@@ -106,7 +106,7 @@ then the triangle
    g\     /f
      \   /
       V V
-       X,
+       X
 ```
 
 commutes.
@@ -138,7 +138,7 @@ then the triangle
    h\     /r
      \   /
       V V
-       B,
+       B
 ```
 
 commutes.

src/foundation-core/equivalences.lagda.md

@@ -34,11 +34,12 @@ also called being **biinvertible**.
 
 The condition of biinvertibility may look odd: Why not say that an equivalence
 is a map that has a [2-sided inverse](foundation-core.invertible-maps.md)? The
-reason is that the condition of invertibility is structure, whereas the
-condition of being biinvertible is a
-[property](foundation-core.propositions.md). To quickly see this: if `f` is an
-equivalence, then it has up to [homotopy](foundation-core.homotopies.md) only
-one section, and it has up to homotopy only one retraction.
+reason is that the condition of invertibility is
+[structure](foundation.structure.md), whereas the condition of being
+biinvertible is a [property](foundation-core.propositions.md). To quickly see
+this: if `f` is an equivalence, then it has up to
+[homotopy](foundation-core.homotopies.md) only one section, and it has up to
+homotopy only one retraction.
 
 ## Definition
 

src/foundation-core/pullbacks.lagda.md

@@ -780,7 +780,9 @@ module _
             ( is-fiberwise-equiv-map-fiber-cone-is-pullback
               ( j ∘ i)
               ( h)
-              ( pasting-horizontal-cone i j h c d) is-pb-rect x))
+              ( pasting-horizontal-cone i j h c d)
+              ( is-pb-rect)
+              ( x)))
 ```
 
 ### The vertical pullback pasting property

src/foundation-core/retractions.lagda.md

@@ -22,8 +22,8 @@ open import foundation-core.whiskering-homotopies
 ## Idea
 
 A **retraction** of a map `f : A → B` consists of a map `r : B → A` equipped
-with a homotopy `r ∘ f ~ id`. In other words, a retraction of a map `f` is a
-left inverse of `f`.
+with a [homotopy](foundation-core.homotopies.md) `r ∘ f ~ id`. In other words, a
+retraction of a map `f` is a left inverse of `f`.
 
 ## Definitions
 
@@ -70,7 +70,7 @@ i.e., that the concatenation
 
 is identical to `p : x ＝ y` for all `p : x ＝ y`, we simply proceed by
 identification elimination. Then it suffices to show that `(H x)⁻¹ ∙ (H x)` is
-identical by `refl`, which is indeed the case by the left inverse law of
+identical to `refl`, which is indeed the case by the left inverse law of
 concatenation of identifications.
 
 ```agda
@@ -161,7 +161,7 @@ that would result in a cyclic module dependency.
 ```agda
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
-  (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h))
+  (f : A → X) (g : B → X) (h : A → B) (H : f ~ g ∘ h)
   (r : retraction f)
   where
 
@@ -195,8 +195,8 @@ In a commuting triangle of the form
        X,
 ```
 
-if `r : X → A` is a section of the map `g` on the right and `t : B → A` is a
-section of the map `h` on top, then `t ∘ s` is a section of the map `f` on the
+if `r : X → A` is a retraction of the map `g` on the right and `s : B → A` is a
+retraction of the map `h` on top, then `s ∘ r` is a retraction of the map `f` on the
 left.
 
 ```agda

src/foundation/descent-coproduct-types.lagda.md

@@ -144,7 +144,8 @@ module _
       is-pullback f i cone-A'
     descent-coprod-inl (pair h (pair f' H)) (pair k (pair g' K)) is-pb-dsq =
         is-pullback-is-fiberwise-equiv-map-fiber-cone f i (triple h f' H)
-          ( λ a → is-equiv-left-map-triangle
+          ( λ a →
+            is-equiv-left-map-triangle
             ( map-fiber-cone f i (triple h f' H) a)
             ( map-fiber-cone (ind-coprod _ f g) i
               ( cone-descent-coprod (triple h f' H) (triple k g' K))
@@ -165,7 +166,8 @@ module _
       is-pullback g i cone-B'
     descent-coprod-inr (pair h (pair f' H)) (pair k (pair g' K)) is-pb-dsq =
         is-pullback-is-fiberwise-equiv-map-fiber-cone g i (triple k g' K)
-          ( λ b → is-equiv-left-map-triangle
+          ( λ b →
+            is-equiv-left-map-triangle
             ( map-fiber-cone g i (triple k g' K) b)
             ( map-fiber-cone (ind-coprod _ f g) i
               ( cone-descent-coprod (triple h f' H) (triple k g' K))

src/foundation/descent-dependent-pair-types.lagda.md

@@ -56,7 +56,8 @@ module _
         ( h)
         ( cone-descent-Σ)
         ( ind-Σ
-          ( λ i a → is-equiv-right-map-triangle
+          ( λ i a →
+            is-equiv-right-map-triangle
             ( map-fiber-cone (f i) h (c i) a)
             ( map-fiber-cone (ind-Σ f) h cone-descent-Σ (pair i a))
             ( map-inv-compute-fiber-tot (λ i → pr1 (c i)) (pair i a))
@@ -71,7 +72,8 @@ module _
       ((i : I) → is-pullback (f i) h (c i))
     descent-Σ' is-pb-dsq i =
       is-pullback-is-fiberwise-equiv-map-fiber-cone (f i) h (c i)
-        ( λ a → is-equiv-left-map-triangle
+        ( λ a →
+          is-equiv-left-map-triangle
           ( map-fiber-cone (f i) h (c i) a)
           ( map-fiber-cone (ind-Σ f) h cone-descent-Σ (pair i a))
           ( map-inv-compute-fiber-tot (λ i → pr1 (c i)) (pair i a))

src/foundation/descent-equivalences.lagda.md

@@ -57,7 +57,8 @@ module _
       ( map-inv-is-equiv-precomp-Π-is-equiv
         ( is-equiv-i)
         ( λ y → is-equiv (map-fiber-cone j h c y))
-        ( λ x → is-equiv-right-map-triangle
+        ( λ x →
+          is-equiv-right-map-triangle
           ( map-fiber-cone (j ∘ i) h
             ( pasting-horizontal-cone i j h c d) x)
           ( map-fiber-cone j h c (i x))

src/foundation/equivalences.lagda.md

@@ -345,9 +345,9 @@ along equivalences. Similarly, the map `j⁻¹ ∘ g` is a retraction of `h`, si
 we have `(g ∘ h ~ j) → (j⁻¹ ∘ g ∘ h ~ id)` by transposing along equivalences.
 Since `h` therefore has a section and a retraction, it is an equivalence.
 
-In fact, the above argument shows that if the top map has a section and the
-bottom map has a retraction, then the diagonal filler, and hence all other maps
-are equivalences.
+In fact, the above argument shows that if the top map `i` has a section and the
+bottom map `j` has a retraction, then the diagonal filler, and hence all other
+maps are equivalences.
 
 ```agda
 module _
@@ -691,4 +691,4 @@ equiv-fiberwise-equiv-fam-equiv B C = distributive-Π-Σ
 
 - The
   [2-out-of-6 property](https://ncatlab.org/nlab/show/two-out-of-six+property)
-  at the nLab.
+  at nlab

src/foundation/functoriality-fibers-of-maps.lagda.md

@@ -325,7 +325,7 @@ constructed as a family of identifications of the form
   eq-Eq-fiber g (γ₀ a) _,
 ```
 
-it follows that when we left-whisker this homotopy with `inclusion-fiber g`, we
+it follows that when we left whisker this homotopy with `inclusion-fiber g`, we
 recover the homotopy `γ₀ ·r inclusion-fiber f`.
 
 Now it remains to fill a coherence for the square of homotopies
@@ -344,13 +344,6 @@ Now it remains to fill a coherence for the square of homotopies
 where `H` is the homotopy that we just constructed, witnessing that the upper
 triangle commutes, and where we have written `i` for all fiber inclusions.
 
-coherence-square-homotopies (pr1 (pr2 htpy-hom-arrow-fiber) ·r inclusion-fiber
-f) (coh-hom-arrow (inclusion-fiber f) (inclusion-fiber g) (comp-hom-arrow
-(inclusion-fiber f) (inclusion-fiber g) (inclusion-fiber g)
-(tr-hom-arrow-inclusion-fiber g (htpy-codomain-htpy-hom-arrow f g α β γ b))
-(hom-arrow-fiber f g α b))) (coh-hom-arrow (inclusion-fiber f) (inclusion-fiber
-g) (hom-arrow-fiber f g β b)) (inclusion-fiber g ·l pr1 htpy-hom-arrow-fiber)
-
 ```agda
 module _
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}

src/foundation/morphisms-arrows.lagda.md

@@ -118,7 +118,7 @@ Consider a commuting diagram of the form
         α₁       β₁
 ```
 
-Then the outer rectangle commutes by horizontal pasing of commuting squares of
+Then the outer rectangle commutes by horizontal pasting of commuting squares of
 maps.
 
 ```agda
@@ -165,7 +165,7 @@ module _
 
 ### Homotopies of morphsims of arrows
 
-A \*\*homotopy of morphisms of arrows from `(i , j , H)` to `(i' , j' , H')` is
+A **homotopy of morphisms of arrows** from `(i , j , H)` to `(i' , j' , H')` is
 a triple `(I , J , K)` consisting of homotopies `I : i ~ i'` and `J : j ~ j'`
 and a homotopy `K` witnessing that the
 [square of homotopies](foundation.commuting-squares-of-homotopies.md)

src/foundation/morphisms-twisted-arrows.lagda.md

@@ -38,6 +38,9 @@ A **morphism of twisted arrows** from `f : A → B` to `g : X → Y` is a triple
 
   commutes.
 
+Thus, a morphism of twisted arrows can also be understood as _a factorization of
+`g` through `f`_.
+
 ## Definitions
 
 ```agda

src/foundation/retracts-of-maps.lagda.md

@@ -657,8 +657,9 @@ module _
           ( preserves-id-hom-arrow-fiber f b)))
 
   retract-map-inclusion-fiber-retract-map :
-    ( inclusion-fiber f {b}) retract-of-map
-    ( inclusion-fiber g {map-codomain-inclusion-retract-map f g R b})
+    retract-map
+      ( inclusion-fiber g {map-codomain-inclusion-retract-map f g R b})
+      ( inclusion-fiber f {b})
   pr1 retract-map-inclusion-fiber-retract-map =
     inclusion-retract-map-inclusion-fiber-retract-map
   pr1 (pr2 retract-map-inclusion-fiber-retract-map) =
@@ -676,8 +677,9 @@ module _
   where
 
   retract-fiber-retract-map :
-    ( fiber f b) retract-of
-    ( fiber g (map-codomain-inclusion-retract-map f g R b))
+    retract
+      ( fiber g (map-codomain-inclusion-retract-map f g R b))
+      ( fiber f b)
   retract-fiber-retract-map =
     retract-domain-retract-map
       ( inclusion-fiber f)