Lemma is_unitary_comp {C : category} {dag : dagger C} {x y z : C} {f : C⟦x,y⟧} (ff : is_unitary dag f) {g : C⟦y,z⟧} (gg : is_unitary dag g) : is_unitary dag (f · g). Proof. split. - etrans. { apply maponpaths, dagger_to_law_comp. } etrans. { apply assoc. } etrans. { apply maponpaths_2, assoc'. } etrans. { apply maponpaths_2, maponpaths, gg. } etrans. { apply maponpaths_2, id_right. } apply ff. - etrans. { apply maponpaths_2, dagger_to_law_comp. } etrans. { apply assoc. } etrans. { apply maponpaths_2, assoc'. } etrans. { apply maponpaths_2, maponpaths, ff. } etrans. { apply maponpaths_2, id_right. } apply gg. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DaggerCategories.Categories.