Lemma cancel_postcomposition {C : precategory_data} {a b c: C} (f f' : a --> b) (g : b --> c) : f = f' -> f · g = f' · g. Proof. intro; apply maponpaths_2; assumption. Defined.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations.