wording 26-descent

fredrik-bakke · May 10, 2023 · 469dba3 · 469dba3
1 parent a426ad1
commit 469dba3
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/synthetic-homotopy-theory/26-descent.lagda.md b/src/synthetic-homotopy-theory/26-descent.lagda.md
@@ -309,9 +309,9 @@ dependent-pullback-property-pushout l {S} {A} {B} f g {X}
     4. dependent-universal-property-pushout
     5. Ind-pushout
 
-We have already shown that (1) ↔ (2). Therefore we will first show that (3) ↔
-(4) ↔ (5). Finally, we will show that (2) ↔ (3). Here are the precise references
-to the proofs of those parts:
+We have already shown (1) ↔ (2). Therefore we will first show (3) ↔ (4) ↔ (5).
+Finally, we will show (2) ↔ (3). Here are the precise references to the proofs
+of those parts:
 
 - Proof of (1) → (2): `pullback-property-pushout-universal-property-pushout`
 - Proof of (2) → (1): `universal-property-pushout-pullback-property-pushout`