Cosmetic change

UniMath · Sep 13, 2023 · ed362d1 · ed362d1
1 parent 7f0c440
commit ed362d1
Showing 1 changed file with 5 additions and 7 deletions.
diff --git a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md
@@ -196,13 +196,11 @@ module _
       ( eq-pair-Σ
         ( refl)
         ( eq-htpy
-          ( λ s →
-            inv
-              ( compute-equiv-htpy-dependent-fuction-dependent-identification-function-type
-                ( Y)
-                ( coherence-square-cocone f g c)
-                ( h)
-                ( s)))))
+          ( inv-htpy
+            ( compute-equiv-htpy-dependent-fuction-dependent-identification-function-type
+              ( Y)
+              ( coherence-square-cocone f g c)
+              ( h)))))
 
   flattening-lemma-pushout :
     flattening-lemma-pushout-statement P f g c dup-pushout