fact: Definition folds_iso_prop {a b : C} (i : folds_iso_data a b) : UU := ((((∏ (x y : C) (f : x ⇒ y) (g : y ⇒ a) (h : x ⇒ a), T f g h ≃ T f ((ϕ₁ i) g) ((ϕ₁ i) h)) × (∏ (x z : C) (f : x ⇒ a) (g : a ⇒ z) (h : x ⇒ z), T f g h ≃ T ((ϕ₁ i) f) ((ϕ₂ i) g) h)) × (∏ (z w : C) (f : a ⇒ z) (g : z ⇒ w) (h : a ⇒ w), T f g h ≃ T ((ϕ₂ i) f) g ((ϕ₂ i) h))) × (((∏ (x : C) (f : x ⇒ a) (g : a ⇒ a) (h : x ⇒ a), T f g h ≃ T ((ϕ₁ i) f) ((ϕo i) g) ((ϕ₁ i) h)) × (∏ (x : C) (f : a ⇒ x) (g : x ⇒ a) (h : a ⇒ a), T f g h ≃ T ((ϕ₂ i) f) ((ϕ₁ i) g) ((ϕ∙ i) h))) × ((∏ (x : C) (f : a ⇒ a) (g h : a ⇒ x), T f g h ≃ T ((ϕ∙ i) f) ((ϕ₂ i) g) ((ϕ₂ i) h)) × (∏ f g h : a ⇒ a, T f g h ≃ T ((ϕ∙ i) f) ((ϕ∙ i) g) ((ϕ∙ i) h))))) × (∏ f : a ⇒ a, I f ≃ I ((ϕ∙ i) f)).
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