proposition: Lemma runitor_CAT_pointwise_is_z_iso {C D : category} (F : [C, D]) : is_z_isomorphism (runitor_CAT F).
proof: Proof. exists (rinvunitor_CAT F). split. - apply runitor_rinvunitor_CAT. - apply rinvunitor_runitor_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