`{fs : Funext} (X : set_cat) C D F G (T1 T2 : morphism set_cat X (Build_HSet (@NaturalTransformation C D F G))) (H : forall x y, T1 x y = T2 x y) `{@IsIsomorphism set_cat _ _ T1} : @IsIsomorphism set_cat _ _ T2. Proof. exists (T1^-1)%morphism; abstract ( first [ apply @iso_moveR_Vp | apply @iso_moveR_pV ]; repeat first [ intro | solve [ auto | symmetry; auto ] | apply @path_forall | path_natural_transformation ] ). Defined.
Require Import Category.Core NaturalTransformation.Core. Require Import Category.Morphisms NaturalTransformation.Paths. Require Import Category.Univalent. Require Import SetCategory.Core. Require Import HoTT.Basics HoTT.Types TruncType.