Lemma is_univalent_implies_is_folds_precat : is_folds_precategory C. Proof. apply make_dirprod. - intros a b f g. apply (isofhlevelweqb _ (make_weq _ (H a b f g))). apply isaprop_folds_2_iso. - apply make_dirprod. + intros. apply (isotoid2 _ H). apply E_implies_folds_iso. set (T_unique := pr1 (pr2 (pr2 (pr1 (pr2 (pr1 C)))))). apply (T_unique _ _ _ f g); auto. + intros. apply (isotoid2 _ H). apply E_implies_folds_iso. set (T_assoc := pr2 (pr2 (pr2 (pr1 (pr2 (pr1 C)))))). simpl in T_assoc. apply (T_assoc _ _ _ _ f g h fg gh fg_h f_gh); auto. Qed.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.