fact: Definition id2_left {a b : C} {f g : C⟦a, b⟧} (x : f ==> g) : id2 f • x = x := pr1 (pr2 C) _ _ _ _ x.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence