Definition z_iso_is_unitary (x y : C) : z_iso x y ≃ unitary (GRP_dagger C) x y. Proof. use weq_iso. - exact (λ p, univalence_to_dagger_univalence p). - exact (λ p, dagger_univalence_to_univalence p). - intro ; apply z_iso_eq, idpath. - intro ; apply unitary_eq, idpath. 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.Core.Univalence. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.CategoryTheory.DaggerCategories.Categories. Require Import UniMath.CategoryTheory.DaggerCategories.Unitary. Require Import UniMath.CategoryTheory.DaggerCategories.Univalence.