Lemma folds_iso_data_prop : folds_iso_prop folds_iso_data_from_z_iso. Proof. repeat split; intros. - simpl. apply logeqweq. + intro H. apply comp_compose2. rewrite assoc. set (H2 := comp_compose2' H). rewrite H2. apply idpath. + intro H. apply comp_compose2. set (H2 := comp_compose2' H). rewrite assoc in H2. eapply post_comp_with_z_iso_is_inj. * apply (z_iso_is_inverse_in_precat f). * apply H2. - simpl. apply logeqweq. + intro H. apply comp_compose2. apply pathsinv0. eapply pathscomp0. * apply (pathsinv0 (comp_compose2' H)). * transitivity ((f0 □ (f □ (inv_from_z_iso f))) □ g). ** rewrite z_iso_inv_after_z_iso. rewrite id_right. apply idpath. ** repeat rewrite assoc; apply idpath. + intro H. apply comp_compose2. set (H2 := comp_compose2' H). apply pathsinv0. eapply pathscomp0. * apply (pathsinv0 H2). * transitivity ((f0 □ (f □ (inv_from_z_iso f))) □ g). ** repeat rewrite assoc; apply idpath. ** rewrite z_iso_inv_after_z_iso. rewrite id_right. apply idpath. - simpl. apply logeqweq. + intro H. apply comp_compose2. rewrite <- assoc. rewrite (comp_compose2' H). apply idpath. + intro H. apply comp_compose2. set (H2:= comp_compose2' H). rewrite <- assoc in H2. use (pre_comp_with_z_iso_inv_is_inj f). exact H2. - simpl; apply logeqweq. + intro H; apply comp_compose2. rewrite <- (comp_compose2' H). transitivity ((f0 □ (f □ (inv_from_z_iso f))) □ (g □ f)). * repeat rewrite assoc; apply idpath. * rewrite z_iso_inv_after_z_iso. rewrite id_right; apply assoc. + intro H; apply comp_compose2. set (H2 := comp_compose2' H). repeat rewrite assoc in H2. use pathscomp0. * exact ((f0 □ (f □ (inv_from_z_iso f))) □ g). * rewrite z_iso_inv_after_z_iso, id_right; apply idpath. * repeat rewrite assoc. use (post_comp_with_z_iso_is_inj f). exact H2. - simpl; apply logeqweq. + intro H. apply comp_compose2. repeat rewrite assoc; rewrite assoc4. rewrite (comp_compose2' H). apply pathsinv0, assoc. + intro H; apply comp_compose2. set (H2 := comp_compose2' H). rewrite <- assoc in H2. use (pre_comp_with_z_iso_inv_is_inj f). use (post_comp_with_z_iso_is_inj f). rewrite assoc. rewrite assoc in H2. rewrite assoc in H2. use (pathscomp0 H2). rewrite <- assoc. apply idpath. - simpl. apply logeqweq. + intro H; apply comp_compose2. rewrite <- (comp_compose2' H); clear H. repeat rewrite <- assoc. apply maponpaths. repeat rewrite assoc. rewrite assoc4, z_iso_inv_after_z_iso, id_right. apply idpath. + intro H; apply comp_compose2. set (H':= comp_compose2' H); generalize H'; clear H' H; intro H. repeat rewrite <- assoc in H. use (pre_comp_with_z_iso_inv_is_inj f). use (pathscomp0 _ H). rewrite (@assoc C' _ _ _ _ f). rewrite z_iso_inv_after_z_iso. rewrite id_left. apply idpath. - simpl; apply logeqweq. + intro H; set (H':=comp_compose2' H); clearbody H'; clear H; rename H' into H; rewrite <- H; clear H. apply comp_compose2. repeat rewrite <- assoc; apply maponpaths; simpl. set (H':=@assoc C' _ _ _ _ f0 g f); clearbody H'; simpl in *. rewrite <- H'; clear H'. apply maponpaths. simpl in *. repeat rewrite (@assoc C'). rewrite z_iso_inv_after_z_iso, id_left; apply idpath. + intro H; set (H':=comp_compose2' H); clearbody H'; clear H; rename H' into H. apply comp_compose2. repeat rewrite <- assoc in H. use (post_comp_with_z_iso_is_inj f). use (pre_comp_with_z_iso_inv_is_inj f). use (pathscomp0 _ H). rewrite (@assoc C' _ _ _ _ f). rewrite z_iso_inv_after_z_iso. rewrite id_left. rewrite <- assoc. apply idpath. - simpl. apply logeqweq. + intro H. apply id_identity2. rewrite (id_identity2' H). rewrite (@id_left C'). apply (z_iso_after_z_iso_inv f). + intro H. apply id_identity2. set (H':=id_identity2' H); clearbody H'; clear H. set (H2:=z_iso_inv_to_left _ _ _ f _ _ H'); clearbody H2. rewrite id_right in H2. transitivity (f □ (inv_from_z_iso f)). * apply (z_iso_inv_on_left (C:=C')), pathsinv0, H2. * apply (z_iso_inv_after_z_iso (C := C')). 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.CategoryTheory.Core.Isos. Require Import UniMath.Folds.folds_precat. Require Import UniMath.Folds.from_precats_to_folds_and_back.