Proposition iseqrel_smash_hrel : iseqrel smash_hrel. Proof. refine ((_ ,, _) ,, _). - intros x₁ x₂ x₃. use factor_through_squash. { use impred ; intro. apply propproperty. } intros p₁. use factor_through_squash. { apply propproperty. } intros p₂. apply hinhpr. induction p₁ as [ p₁ | p₁ ] ; induction p₂ as [ p₂ | p₂ ] ; cbn in *. + exact (inl (p₁ @ p₂)). + induction p₁. exact (inr p₂). + induction p₂. exact (inr p₁). + exact (inr (pr1 p₁ ,, pr2 p₂)). - intros xy. exact (hinhpr (inl (idpath _))). - intros xy₁ xy₂. use factor_through_squash. { apply propproperty. } intros p. apply hinhpr. induction p as [ p | p ] ; cbn in *. + exact (inl (!p)). + exact (inr (pr2 p ,, pr1 p)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits.