Lemma folds_precat_from_precat_precat_from_folds_precat (C : folds_precat)(hs:has_folds_homsets C): folds_precat_from_precat (precat_from_folds_precat C) hs = C. Proof. apply subtypePath'. 2: { intro a; apply isapropdirprod. + apply isaprop_folds_ax_id. + apply isaprop_folds_ax_T. apply hs. } set (Hid := I_contr C). set (Hcomp := T_contr C). destruct C as [Cd CC]; simpl in *. destruct Cd as [Ca Cb]; simpl in *. unfold folds_id_comp_from_precat_data. apply maponpaths. destruct CC as [C1 C2]. simpl in *. destruct Cb as [Cid Ccomp]. simpl in *. apply pathsdirprod. + apply funextsec. intro a. apply funextsec. intro f. unfold id_pred. simpl. apply subtypePath. { intro. apply isapropisaprop. } simpl. apply weqtopaths. apply weqimplimpl. * intro H. rewrite H. set (Hid' := pr1 (Hid a)). apply (pr2 (Hid')). * intro H. unfold precategory_morphisms in f. set (H2 := pr2 (Hid a)). simpl in H2. apply (path_to_ctr). assumption. * apply hs. * apply (pr2 (Cid a f)). + apply funextsec; intro a. apply funextsec; intro b. apply funextsec; intro c. apply funextsec; intro f. apply funextsec; intro g. apply funextsec; intro fg. clear Hid. apply subtypePath. { intro; apply isapropisaprop. } apply weqtopaths. apply weqimplimpl. * intro H. simpl in *. rewrite <- H. apply (pr2 (pr1 (Hcomp a b c f g))). * simpl. intro H. apply pathsinv0. apply path_to_ctr. assumption. * simpl in *. apply hs. * apply (pr2 (Ccomp _ _ _ _ _ _ )). Qed.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Folds.folds_precat.