Lemma precat_from_folds_precat_folds_precat_from_precat (C : precategory)(hs: has_homsets C) : precat_from_folds_precat (folds_precat_from_precat C hs) = C. Proof. apply subtypePath'. 2: { intro; apply isaprop_is_precategory. assumption. } destruct C as [Cdata Cax]; simpl in *. destruct Cdata as [Cobmor Cidcomp]; simpl in *. unfold precat_from_folds_data. simpl. apply maponpaths. destruct Cidcomp as [Cid Ccomp]; simpl in *. apply pathsdirprod. - apply funextsec; intro a. apply pathsinv0. apply path_to_ctr. apply idpath. - apply funextsec; intro a. apply funextsec; intro b. apply funextsec; intro c. apply funextsec; intro f. apply funextsec; intro g. apply pathsinv0. apply path_to_ctr. apply idpath. 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.