Lemma fully_faithful_reflects_is_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, ∏ f : C⟦c,c'⟧, is_unitary dagD (#F f) -> is_unitary dagC f. Proof. intros c c' f u. set (i := pr2 (fully_faithful_reflects_iso_proof _ _ _ ff c c' (Isos.make_z_iso _ _ u))). cbn in i. split. - refine (_ @ pr1 i). use maponpaths_compose. + apply pathsinv0, homotinvweqweq. + refine (! homotinvweqweq (weq_from_fully_faithful ff c' c) (dagC _ _ f) @ _). apply maponpaths. apply dagF. - refine (_ @ pr2 i). use maponpaths_compose. + refine (! homotinvweqweq (weq_from_fully_faithful ff c' c) (dagC _ _ f) @ _). apply maponpaths. apply dagF. + apply pathsinv0, homotinvweqweq. 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.DaggerCategories.Categories. Require Import UniMath.CategoryTheory.DaggerCategories.Functors. Require Import UniMath.CategoryTheory.DaggerCategories.Unitary.