Definition full_subcat_nat_trans_is_z_iso {C D : category} {F : functor C D} {G : functor C D} (eta : nat_trans F G) : sub_precategories C. Proof. apply full_sub_precategory. intro c; use make_hProp. - exact (is_z_isomorphism (eta c)). - apply isaprop_is_z_isomorphism. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.Foundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Subcategory.Full. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.whiskering.