proposition: Lemma GG_is_dagger_functor : is_dagger_functor dagD dagE GG.
proof: Proof. intros x y f. transparent assert (rhs : (Y (dagD x y f))). { exists (dagE (Go x) (Go y) (G f)). intros c h c' h' l p. apply (dagger_injective dagE). do 2 rewrite dagger_to_law_comp. rewrite dagger_to_law_idemp. rewrite <- dagF. apply unitary_inv_on_left. { apply k. } unfold G. set (p0 := pr21 (Y_iscontr _ _ (dagD _ _ f)) _ h _ h' l p). rewrite assoc'. assert (pf : # H (dagC c c' l) · h = h' · f). { rewrite dagH. apply (dagger_injective dagD). do 2 rewrite dagger_to_law_comp. rewrite dagger_to_law_idemp. use unitary_inv_on_left. { apply h'. } rewrite assoc'. rewrite p. rewrite assoc. etrans. 2: apply maponpaths_2, pathsinv0, (pr22 h). apply pathsinv0, id_left. } etrans. 2: { apply maponpaths, pathsinv0. exact (pr21 (Y_iscontr _ _ f) _ h' _ h (dagC _ _ l) pf). } rewrite assoc. etrans. 2: apply maponpaths_2, pathsinv0, k. apply pathsinv0, id_left. } exact (base_paths _ _ (! pr2 (Y_iscontr _ _ (dagD x y f)) rhs)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.TotalCategoryFacts UniMath.CategoryTheory.precomp_fully_faithful UniMath.CategoryTheory.DaggerCategories.Categories UniMath.CategoryTheory.DaggerCategories.Functors UniMath.CategoryTheory.DaggerCategories.Transformations UniMath.CategoryTheory.DaggerCategories.Unitary UniMath.CategoryTheory.DaggerCategories.Univalence UniMath.CategoryTheory.DaggerCategories.FunctorCategory UniMath.CategoryTheory.DaggerCategories.Functors.FullyFaithful UniMath.CategoryTheory.DaggerCategories.Functors.WeakEquivalences