proposition: Lemma fully_faithful_reflect_dagger_uniquely {C D : category} {F : functor C D} (dagD : dagger D) (ff : fully_faithful F) : ∃! dagC : dagger C, is_dagger_functor dagC dagD F.
proof: Proof. exists (fully_faithful_reflect_dagger dagD ff ,, fully_faithful_is_dagger_functor dagD ff). intro dag. use subtypePath. { intro ; apply isaprop_is_dagger_functor. } use subtypePath. { intro ; apply isaprop_dagger_laws. } do 3 (apply funextsec ; intro). apply pathsweq1. apply (pr2 dag). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.DaggerCategories.Categories UniMath.CategoryTheory.DaggerCategories.Functors UniMath.CategoryTheory.DaggerCategories.Unitary