proposition: Lemma inv_folds_iso_prop : folds_iso_prop inv_folds_iso_data.
proof: 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.
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.Folds.folds_precat UniMath.Folds.from_precats_to_folds_and_back