From eff490bea2b6b72dc4ec536c6369536f2c586ea6 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 24 Feb 2024 18:35:34 +0100 Subject: [PATCH] pre-commit --- src/foundation/standard-pullbacks.lagda.md | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/foundation/standard-pullbacks.lagda.md b/src/foundation/standard-pullbacks.lagda.md index 39bbc353ee..a9c7b7786b 100644 --- a/src/foundation/standard-pullbacks.lagda.md +++ b/src/foundation/standard-pullbacks.lagda.md @@ -259,14 +259,18 @@ module _ inr (x , y , is-injective-inr p) is-section-map-inv-coproduct-cone-standard-pullback : - is-section map-coproduct-cone-standard-pullback map-inv-coproduct-cone-standard-pullback + is-section + ( map-coproduct-cone-standard-pullback) + ( map-inv-coproduct-cone-standard-pullback) is-section-map-inv-coproduct-cone-standard-pullback (inl x , inl y , p) = eq-pair-eq-fiber (eq-pair-eq-fiber (is-section-is-injective-inl p)) is-section-map-inv-coproduct-cone-standard-pullback (inr x , inr y , p) = eq-pair-eq-fiber (eq-pair-eq-fiber (is-section-is-injective-inr p)) is-retraction-map-inv-coproduct-cone-standard-pullback : - is-retraction map-coproduct-cone-standard-pullback map-inv-coproduct-cone-standard-pullback + is-retraction + ( map-coproduct-cone-standard-pullback) + ( map-inv-coproduct-cone-standard-pullback) is-retraction-map-inv-coproduct-cone-standard-pullback (inl (x , y , p)) = ap ( inl)