Definition folds_iso {C: folds_pre_3_cat} {a b : C} (f g : a ⇒ b) : UU := (((∏ (x : C) (u : x ⇒ a) (v : x ⇒ b), T u f v ≃ T u g v) × (∏ (x : C) (u : a ⇒ x) (v : x ⇒ b), T u v f ≃ T u v g)) × (∏ (x : C) (u : b ⇒ x) (v : a ⇒ x), T f u v ≃ T g u v)) × ((((∏ (u : a ⇒ b) (p : b = a), T p ## f f u ≃ T p ## g g u) × (∏ (u : b ⇒ b) (p : a = a), T (transportf (λ a, a ⇒ b) p f) u f ≃ T (transportf (λ a, a ⇒ b) p g) u g)) × ((∏ (u : a ⇒ a) (p : b = b), T u p ## f f ≃ T u p ## g g) × (∏ (p : a = a) (q : b = a) (r : b = b), T (folds_double_transport p q f) r ## f f ≃ T (folds_double_transport p q g) r ## g g))) × (((∏ p : b = a, I p ## f ≃ I p ## g) × (∏ u : a ⇒ b, E f u ≃ E g u)) × ((∏ u : a ⇒ b, E u f ≃ E u g) × (∏ (p : a = a) (q : b = b), E (folds_double_transport p q f) f ≃ E (folds_double_transport p q g) g)))).
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.