Lemma remove_id_right (C : precategory) (a b : C) (f g : a --> b) (h : b --> b): h = identity _ -> f = g -> f · h = g. Proof. intros H eq. intermediate_path (f · identity _). - destruct H. apply idpath. - intermediate_path f. + apply id_right. + apply eq. Defined.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations.