Definition full_dagger_img_to_full_img : functor (full_sub_category D P) (full_sub_category D (λ d : D, is_in_img_functor F d)). Proof. use full_sub_category_functor. - exact (functor_identity D). - intros d in_dag_im. use (factor_through_squash_hProp _ _ in_dag_im). clear in_dag_im ; intro in_dag_im. apply hinhpr. exists (pr1 in_dag_im). exact (make_z_iso _ _ (pr22 in_dag_im)). 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.