fact: Definition id_right (C : precategory) : ∏ (a b : C) (f : a --> b), f · identity b = f := pr212 C.
imports: UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations