Update src/foundation/functoriality-coproduct-types.lagda.md

UniMath · Feb 26, 2024 · 59998a2 · 59998a2
1 parent e89b873
commit 59998a2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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