Definition pr1_pr1_functor_eq_from_functor_iso (C : precategory_data) (D : category) (H : is_univalent D) (F G : functor_category C D) : z_iso F G -> pr1 (pr1 F) = pr1 (pr1 G). Proof. intro A. apply funextsec. intro t. apply isotoid. assumption. apply (functor_z_iso_pointwise_if_z_iso _ _ _ _ _ A). apply (pr2 A). 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.