proposition: Lemma id_conjugation {A : precategory} {a b : A} (f : a --> b) (g : b --> a) (x : b --> b) : x = identity _ -> f · g = identity _ -> f · x · g = identity _ .
proof: Proof. intros H H'. rewrite H. rewrite id_right. apply H'. Qed.
imports: UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations