Lemma REL_is_precategory : is_precategory REL_precategory_data. Proof. repeat split ; intro ; intros ; repeat (apply funextsec ; intro) ; use hPropUnivalence. - intro p. use (factor_through_squash_hProp (f _ _) _ p). clear p ; intro p. induction (! pr12 p). exact (pr22 p). - intro p. apply hinhpr. exact (x ,, idpath _ ,, p). - intro p. use (factor_through_squash_hProp (f _ _) _ p). clear p ; intro p. induction (pr22 p). exact (pr12 p). - intro p. apply hinhpr. exact (x0 ,, p ,, idpath _). - intro p. use (factor_through_squash_hProp ((f · g · h) x x0) _ p). clear p ; intro p. use (factor_through_squash_hProp ((f · g · h) x x0) _ (pr22 p)). intro q. apply hinhpr. exists (pr1 q). split. + apply hinhpr. exact (pr1 p ,, pr12 p ,, pr12 q). + exact (pr22 q). - intro p. use (factor_through_squash_hProp ((f · (g · h)) x x0) _ p). + clear p ; intro p. use (factor_through_squash_hProp ((f · (g · h)) x x0) _ (pr12 p)). intro q. apply hinhpr. exists (pr1 q). split. * exact (pr12 q). * apply hinhpr. exact (pr1 p,, pr22 q ,, pr22 p). - intro p. use (factor_through_squash_hProp ((f · (g · h)) x x0) _ p). + clear p ; intro p. use (factor_through_squash_hProp ((f · (g · h)) x x0) _ (pr12 p)). intro q. apply hinhpr. exists (pr1 q). split. * exact (pr12 q). * apply hinhpr. exact (pr1 p,, pr22 q ,, pr22 p). - intro p. use (factor_through_squash_hProp ((f · g · h) x x0) _ p). + clear p ; intro p. use (factor_through_squash_hProp _ _ (pr22 p)). intro q. apply hinhpr. exists (pr1 q). split. * apply hinhpr. exact (pr1 p ,, pr12 p ,, pr12 q). * exact (pr22 q). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.HSET.All.