proposition: Lemma post_comp_with_z_iso_inv_is_inj {C : precategory} {a b b' : C} {f : a --> b} {g : b --> a} (i : is_inverse_in_precat f g) : ∏ (f' g' : b' --> b), f' · g = g' · g -> f' = g'.
proof: Proof. intros f' g' H. apply (maponpaths (postcompose f)) in H. unfold postcompose in H. do 2 rewrite <- assoc in H. rewrite (is_inverse_in_precat2 i) in H. do 2 rewrite id_right in H. exact H. Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories