Definition folds_ax_I (C : folds_id_T) := (∏ a : C, ∥ ∑ f : a ⇒ a, I f ∥ ) × ((∏ (a b : C) (f : a ⇒ b)(i : b ⇒ b), I i → T f i f) × (∏ (a b : C) (f : a ⇒ b)(i : a ⇒ a), I i → T i f f)).
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.