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. intros H H'. rewrite H. rewrite id_right. apply H'. Qed.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations.