proposition: 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: 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.
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom UniMath.CategoryTheory.Core.Categories UniMath.Folds.folds_precat