proposition: Lemma is_z_iso_runitor {a b : C} (f : hom_precategory a b) : is_z_isomorphism (runitor f : (hom_precategory a b) ⟦ f · identity b, f ⟧).
proof: Proof. exists (rinvunitor f). split. - apply runitor_rinvunitor. - apply rinvunitor_runitor. 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