proposition: Lemma is_z_iso_lunitor {a b : C} (f : hom_precategory a b) : is_z_isomorphism (lunitor f : (hom_precategory a b) ⟦ identity a · f, f ⟧).
proof: Proof. exists (linvunitor f). split. - apply lunitor_linvunitor. - apply linvunitor_lunitor. Defined.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct