proposition: Lemma unitary_functor_eq_to_unitary_functors_naturality (p : unitary_functors_eq) : is_nat_trans F G (λ c : pr11 C, pr1 (pr1 p c)).
proof: Proof. intros c1 c2 f. refine (_ @ maponpaths (compose _) (! pr2 p _ _ _)). refine (_ @ assoc' _ _ _). apply maponpaths_2. refine (_ @ assoc' _ _ _). refine (! id_left _ @ _). apply maponpaths_2, pathsinv0, (pr1 p). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DaggerCategories.Categories UniMath.CategoryTheory.DaggerCategories.Unitary UniMath.CategoryTheory.DaggerCategories.Univalence UniMath.CategoryTheory.DaggerCategories.Functors UniMath.CategoryTheory.DaggerCategories.Transformations