Definition folds_precat_from_precat : folds_precat. Proof. exists (folds_id_comp_from_precat_data C hs). repeat split. - intro a. apply hinhpr. exists (identity a). apply idpath. - intros; unfold T; simpl. intermediate_path (compose f (identity _ )). + apply maponpaths; assumption. + apply id_right. - intros; unfold T; simpl. intermediate_path (compose (identity _ ) f). + rewrite X. apply idpath. + apply id_left. - intros a b c f g. apply hinhpr. exists (compose f g). apply idpath. - simpl. intros a b c f g h k H1 H2. intermediate_path (compose f g). + apply pathsinv0. apply H1. + apply H2. - simpl. intros a b c d f g h fg gh fg_h f_gh H1 H2 H3 H4. rewrite <- H4, <- H3, <- H2, <- H1. apply assoc. Defined.
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.