Definition is_dagger_functor_comp {C D E : category} {dagC : dagger C} {dagD : dagger D} {dagE : dagger E} {F : functor C D} {G : functor D E} (dF : is_dagger_functor dagC dagD F) (dG : is_dagger_functor dagD dagE G) : is_dagger_functor dagC dagE (functor_composite F G).
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.