Lemma maponpaths_compose {C : category} {x y z : C} (f1 f2 : C⟦x,y⟧) (g1 g2 : C⟦y,z⟧) : f1 = f2 -> g1 = g2 -> f1 · g1 = f2 · g2. Proof. exact (λ p q, maponpaths_12 compose p q). Qed.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations.