From e099ad6494dc2b8b9e6b60a82840d23f82813a50 Mon Sep 17 00:00:00 2001 From: VojtechStep Date: Mon, 9 Oct 2023 21:40:38 +0200 Subject: [PATCH] Prose --- .../flattening-lemma-pushouts.lagda.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md index d71888f573a..33d92629b8e 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md @@ -129,7 +129,9 @@ module _ ### The statement of the flattening lemma for pushouts, phrased using descent data -In the above statement, bla bla +The above statement of the flattening lemma works with a provided type family +over the pushout. We can instead accept a definition of this family via descent +data for the pushout. ```agda module _ @@ -183,7 +185,7 @@ module _ ( {l : Level} → dependent-universal-property-pushout l f g c) → { l : Level} → universal-property-pushout l - ( map-Σ (pr1 P) f (λ s → id)) + ( map-Σ-map-base f (pr1 P)) ( map-Σ (pr1 (pr2 P)) g (λ s → map-equiv (pr2 (pr2 P) s))) ( cocone-flattening-descent-data-pushout) ```