Lemma fully_faithful_reflects_unitary {C D : category} {dagC : dagger C} {dagD : dagger D} {F : functor C D} (dagF : is_dagger_functor dagC dagD F) (ff : fully_faithful F) : ∏ c c' : C, unitary dagD (F c) (F c') -> unitary dagC c c'. Proof. intros c c' u. exists (fully_faithful_inv_hom ff c c' (pr1 u)). apply (fully_faithful_reflects_is_unitary dagF ff c c' (fully_faithful_inv_hom ff c c' (pr1 u))). set (p := ! maponpaths (is_unitary dagD) (functor_on_fully_faithful_inv_hom ff _ _ (pr1 u))). exact (path_to_fun p (pr2 u)). 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.DaggerCategories.Categories. Require Import UniMath.CategoryTheory.DaggerCategories.Functors. Require Import UniMath.CategoryTheory.DaggerCategories.Unitary.