Definition z_iso_REL_equiv_dagger_z_iso : z_iso (C := REL) X Y ≃ unitary REL_dagger_structure X Y. Proof. apply weqfibtototal. intro r. apply weqimplimpl. - intro i. unfold is_unitary. unfold REL_dagger_structure. unfold is_inverse_in_precat. cbn. split ; do 2 (apply funextsec ; intro). + apply unique_image_to_inverse_law_in_REL. * apply is_z_iso_in_REL_to_unique_image. use (pr2 (is_z_iso_in_REL_simplified _)). split. -- exact (pr2 (pr1 (is_z_iso_in_REL_simplified r) i)). -- exact (pr1 (pr1 (is_z_iso_in_REL_simplified r) i)). * exact (is_z_iso_in_REL_to_unique_image _ i). + etrans. 2: { use (unique_image_to_inverse_law_in_REL (r := pr1 i)). - exact (pr2 (pr1 (is_z_iso_in_REL_simplified _) (pr2 (z_iso_inv (r,,i))))). - apply (is_z_iso_in_REL_to_unique_image). exact (pr2 (z_iso_inv (r,,i))). } apply hPropUnivalence. * intro px. use (factor_through_squash_hProp _ _ px). clear px ; intro px. apply hinhpr. refine (pr1 px ,, _ ,, _) ; apply inverse_swap_relation, (pr2 px). * intro px. use (factor_through_squash_hProp _ _ px). clear px ; intro px. apply hinhpr. refine (pr1 px ,, _ ,, _) ; apply (inverse_swap_relation_iff i _ _), (pr2 px). - exact (λ i, _ ,, (i : is_inverse_in_precat _ _)). - apply isaprop_is_z_isomorphism. - apply isaprop_is_unitary. 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.Categories.Rel. Require Import UniMath.CategoryTheory.DaggerCategories.Categories. Require Import UniMath.CategoryTheory.DaggerCategories.Unitary. Require Import UniMath.CategoryTheory.DaggerCategories.Univalence.