Definition dagger_functor_dagger_img_factorization : ∑ (I : category) (dagI : dagger I) (F0 : functor C I) (F1 : functor I D) (dagF0 : is_dagger_functor dagC dagI F0) (dagF1 : is_dagger_functor dagI dagD F1), is_unitarily_eso dagF0 × fully_faithful F1 × functor_composite F0 F1 = F. Proof. exists full_dagger_img. exists full_img_dagger. exists functor_full_dagger_img. exists (sub_precategory_inclusion D (full_sub_precategory P)). exists functor_full_img_is_dagger_functor. exists (inclusion_is_dagger_functor _ _). exists functor_full_img_is_unitarily_eso. exists (fully_faithful_sub_precategory_inclusion _ _). apply factorization_full_dagger_inclusion_equal. 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.Core.Isos. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Subcategory.Full. 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.Functors.WeakEquivalences. Require Import UniMath.CategoryTheory.DaggerCategories.Examples.Fullsub.