Lemma inv_folds_iso_prop : folds_iso_prop inv_folds_iso_data. Proof. repeat split; intros. - simpl. apply invweq. set (q:=pr1 (pr1 (pr1 (pr1 (pr2 i))))). clearbody q. set (q':= q _ _ f (invmap (ϕ₁ i) g) (invmap (ϕ₁ i) h)). repeat rewrite (homotweqinvweq (ϕ₁ i)) in q'. apply q'. - simpl. apply invweq. set (q:=pr2 (pr1 (pr1 (pr1 (pr2 i))))). simpl in q; clearbody q. set (q':= q _ _ (invmap (ϕ₁ i) f) (invmap (ϕ₂ i) g) h); clearbody q'. repeat rewrite homotweqinvweq in q'. apply q'. - simpl. apply invweq. set (q:= ((pr2 (pr1 (pr1 (pr2 i)))))). clearbody q; simpl in q. set (q':= q _ _ (invmap (ϕ₂ i) f) g (invmap (ϕ₂ i) h) ). repeat rewrite homotweqinvweq in q'. apply q'. - simpl; apply invweq. set (q:= pr1 (pr1 (pr2 (pr1 (pr2 i))))). clearbody q; simpl in q. set (q':= q _ (invmap (ϕ₁ i) f) (invmap (ϕ∙ i) g) (invmap (ϕ₁ i) h)). repeat rewrite homotweqinvweq in q'. apply q'. - simpl; apply invweq. set (q:= pr2 (pr1 (pr2 (pr1 (pr2 i))))). clearbody q; simpl in q. set (q':= q _ (invmap (ϕ₂ i) f) (invmap (ϕ₁ i) g) (invmap (ϕ∙ i) h)). repeat rewrite homotweqinvweq in q'. apply q'. - simpl. apply invweq. set (q:= pr1 (pr2 (pr2 (pr1 (pr2 i))))). clearbody q; simpl in q. specialize (q _ (invmap (ϕ∙ i) f) (invmap (ϕ₂ i) g) (invmap (ϕ₂ i) h)). repeat rewrite homotweqinvweq in q. apply q. - simpl. apply invweq. set (q:= pr2 (pr2 (pr2 (pr1 (pr2 i))))). clearbody q; simpl in q. specialize (q (invmap (ϕ∙ i) f) (invmap (ϕ∙ i) g) (invmap (ϕ∙ i) h)). repeat rewrite homotweqinvweq in q. apply q. - simpl. apply invweq. set (q:= pr2 (pr2 i)). simpl in q; clearbody q. specialize (q (invmap (ϕ∙ i) f)). rewrite homotweqinvweq in q. apply q. 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.