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)).
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.