proposition: Lemma triangle_id_inverse' (a : A) : inv_from_z_iso (functor_on_z_iso F (eta a)) = eps (F a).
proof: Proof. apply (base_paths _ _ (triangle_id_inverse a)). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core