Definition functor_eq_from_functor_z_iso {C : precategory_data} {D : category} (H : is_univalent D) (F G : ob [C , D, D]) (H' : z_iso F G) : F = G. Proof. apply (functor_eq _ _ D F G). apply pr1_functor_eq_from_functor_z_iso; assumption. Defined.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence.