Lemma identity_is_iso (C : precategory) (a : ob C) : is_iso (identity a). 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.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories.