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. 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.
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.