Lemma REL_dagger_laws : dagger_laws REL_dagger_structure. Proof. repeat split ; intro ; intros ; repeat (apply funextsec ; intro) ; cbn. - use (invweq (weqeqweqhProp _ _)). use weqimplimpl. + exact (λ p, ! p). + exact (λ p, ! p). + apply eqset. + apply eqset. - use (invweq (weqeqweqhProp _ _)). use weqimplimpl. + intro p. use (factor_through_squash_hProp _ _ p). clear p ; intro p. apply hinhpr. exact (pr1 p ,, pr22 p ,, pr12 p). + intro p. use (factor_through_squash_hProp _ _ p). clear p ; intro p. apply hinhpr. exact (pr1 p ,, pr22 p ,, pr12 p). + apply isapropishinh. + apply isapropishinh. Qed.
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.