proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.DaggerCategories.Categories