proposition: Proposition iseqrel_smash_hrel : iseqrel smash_hrel.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits