proposition: Lemma identity_is_iso (C : precategory) (a : ob C) : is_iso (identity a).
proof: Proof. intros c. set (T := @isweqhomot (a --> c) (a --> c) (λ t, t) (precomp_with (identity a))). apply T. - intro g. apply pathsinv0. apply id_left. - apply idisweq. Defined.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories