Lemma GG_is_dagger_functor : is_dagger_functor dagD dagE GG. 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.
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.whiskering. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.TotalCategoryFacts. Require Import UniMath.CategoryTheory.precomp_fully_faithful. Require Import UniMath.CategoryTheory.DaggerCategories.Categories. Require Import UniMath.CategoryTheory.DaggerCategories.Functors. Require Import UniMath.CategoryTheory.DaggerCategories.Transformations. Require Import UniMath.CategoryTheory.DaggerCategories.Unitary. Require Import UniMath.CategoryTheory.DaggerCategories.Univalence. Require Import UniMath.CategoryTheory.DaggerCategories.FunctorCategory. Require Import UniMath.CategoryTheory.DaggerCategories.Functors.FullyFaithful. Require Import UniMath.CategoryTheory.DaggerCategories.Functors.WeakEquivalences.