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