Definition z_iso_is_nat_z_iso {C D : category} (F G : C ⟶ D) : @z_iso (functor_category C D) F G ≃ nat_z_iso F G. Proof. refine (make_weq (nat_z_iso_from_z_iso D (F:=F)(G:=G)) _). use isweq_iso. - apply z_iso_from_nat_z_iso. - intros X. use subtypePath. + intro. apply (isaprop_is_z_isomorphism(C:=functor_category C D)). + apply nat_trans_eq. { apply D. } reflexivity. - intros X. use subtypePath. + intro. apply isaprop_is_nat_z_iso. + reflexivity. 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.