From 59998a2f2147e1260d7021bd90d3c854781bda1e Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 26 Feb 2024 12:25:43 +0100 Subject: [PATCH] Update src/foundation/functoriality-coproduct-types.lagda.md --- src/foundation/functoriality-coproduct-types.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/foundation/functoriality-coproduct-types.lagda.md b/src/foundation/functoriality-coproduct-types.lagda.md index 081b27be20..72a3e32cc2 100644 --- a/src/foundation/functoriality-coproduct-types.lagda.md +++ b/src/foundation/functoriality-coproduct-types.lagda.md @@ -89,7 +89,7 @@ module _ preserves-comp-map-coproduct : map-coproduct (f' ∘ f) (g' ∘ g) ~ map-coproduct f' g' ∘ map-coproduct f g preserves-comp-map-coproduct (inl x) = refl - preserves-comp-map-coproduct (inr x) = refl + preserves-comp-map-coproduct (inr y) = refl ``` ### Functoriality of coproducts preserves homotopies