proposition: Lemma isisomorphism_set_cat_natural_transformation_paths `{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: 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.
imports: Category.Core NaturalTransformation.Core Category.Morphisms NaturalTransformation.Paths Category.Univalent SetCategory.Core HoTT.Basics HoTT.Types TruncType