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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DaggerCategories.Categories. Require Import UniMath.CategoryTheory.DaggerCategories.Unitary. Require Import UniMath.CategoryTheory.DaggerCategories.Univalence. Require Import UniMath.CategoryTheory.DaggerCategories.Functors. Require Import UniMath.CategoryTheory.DaggerCategories.Transformations.