proposition: Lemma unitary_functors_eq_from_unitary_functors_naturality (α : unitary_functors dagF dagG) : ∏ (x y : C) (f : C ⟦ x, y ⟧), # G f = dagD (F x) (G x) ((pr1 α) x) · # F f · (pr1 α) y.
proof: Proof. intros c1 c2 f. apply pathsinv0. refine (assoc' _ _ _ @ _). refine (maponpaths (compose _) (pr21 α _ _ _) @ _). refine (assoc _ _ _ @ _). refine (_ @ id_left _). apply maponpaths_2, (pr2 α). 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