proposition: Lemma lunitor_CAT_pointwise_is_z_iso {C D : category} (F : [C, D]) : is_z_isomorphism (lunitor_CAT F).
proof: Proof. exists (linvunitor_CAT F). split. - apply lunitor_linvunitor_CAT. - apply linvunitor_lunitor_CAT. Defined.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering