proposition: Lemma REL_is_precategory : is_precategory REL_precategory_data.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Categories.HSET.All