Definition unitary_functors_equiv_unitary : unitary_functors dagF dagG ≃ unitary (dagger_functor_cat_structure dagC dagD) (F,,dagF) (G,,dagG). Proof. use weq_iso. - intro α. exists (make_dagger_transformation dagC dagD _ _ (pr1 α : nat_trans (pr1 (F,,dagF)) (pr1 (G,,dagG)))). abstract (split ; apply dagger_transformation_equality ; intro c ; apply (pr2 α c)). - intro α. exists (pr11 α). abstract ( intro c ; split ; [ exact (eqtohomot (base_paths _ _ (base_paths _ _ (pr12 α))) c) | exact (eqtohomot (base_paths _ _ (base_paths _ _ (pr22 α))) c) ]). - abstract ( intro α ; use total2_paths_f ; [ use (nat_trans_eq (pr2 D)) ; intro ; apply idpath | use proofirrelevance ; apply impred_isaprop ; intro ; apply Isos.isaprop_is_inverse_in_precat]). - abstract ( intro α ; use total2_paths_f ; [ apply dagger_transformation_equality ; intro ; apply idpath | apply isaprop_is_unitary]). Defined.
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.