Definition daggercatiso (C D : dagger_category) : UU := ∑ i : catiso C D, is_dagger_functor C D i.
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.catiso. Require Import UniMath.CategoryTheory.CategoryEquality. Require Import UniMath.CategoryTheory.DaggerCategories.Categories. Require Import UniMath.CategoryTheory.DaggerCategories.Functors.