proposition: 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: Proof. exact (λ p q, maponpaths_12 compose p q). Qed.
imports: UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations