proposition: Lemma is_univalent_implies_is_folds_precat : is_folds_precategory C.
proof: 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.
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets