Definition REL_sym_mon_closed_cat : sym_mon_closed_cat. Proof. use make_sym_mon_closed_cat. - exact REL_sym_monoidal_cat. - exact (λ X Y, X × Y)%set. - exact (λ X Y xyx y, pr11 xyx = pr2 xyx ∧ pr21 xyx = y)%logic. - exact (λ X Y Z R z xy, R (z ,, pr1 xy) (pr2 xy)). - intros X Y Z R. use funextsec ; intros (z₁ & x₁). use funextsec ; intro y₁. use hPropUnivalence. + abstract (use factor_through_squash ; [ apply propproperty | ] ; intros (((x₂ & y₂) & x₃) & (q & p₁ & p₂)) ; cbn in p₁, p₂ ; induction p₁, p₂ ; use (factor_through_squash _ _ q) ; [ apply propproperty | ] ; clear q ; cbn ; intros (((x₄ & y₃) & x₅) & ((p₁ & p₂) & p₃ & p₄)) ; cbn in * ; induction p₁, p₄ ; pose (maponpaths dirprod_pr1 p₃) as r₁ ; pose (maponpaths dirprod_pr2 p₃) as r₂ ; cbn in r₁, r₂ ; rewrite <- r₁, <- r₂ ; exact p₂). + abstract (intro r ; refine (hinhpr (((x₁ ,, y₁) ,, x₁) ,, _)) ; repeat split ; try (apply idpath) ; refine (hinhpr (((x₁ ,, y₁) ,, x₁) ,, _)) ; cbn ; repeat split ; try (apply idpath) ; exact r). - intros X Y Z R. use funextsec ; intro z. use funextsec ; intros (x & y). use hPropUnivalence. + abstract (intro r ; refine (hinhpr (((x ,, y) ,, x) ,, _)) ; repeat split ; try (apply idpath) ; refine (hinhpr (((x ,, y) ,, x) ,, _)) ; repeat split ; try (apply idpath) ; cbn ; exact r). + abstract (use factor_through_squash ; [ apply propproperty | ] ; intros (((x₂ & y₂) & x₃) & (q & p₁ & p₂)) ; cbn in p₁, p₂ ; induction p₁, p₂ ; use (factor_through_squash _ _ q) ; [ apply propproperty | ] ; clear q ; cbn ; intros (((x₄ & y₃) & x₅) & ((p₁ & p₂) & p₃ & p₄)) ; cbn in * ; induction p₁, p₄ ; pose (maponpaths dirprod_pr1 p₃) as r₁ ; pose (maponpaths dirprod_pr2 p₃) as r₂ ; cbn in r₁, r₂ ; rewrite <- r₁, <- r₂ ; exact p₂). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Categories.Rel. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed.