+nrecord nAx : Type[2] ≝ {
+ nS:> setoid; (*Type[0];*)
+ nI: nS → Type[0];
+ nD: ∀a:nS. nI a → Type[0];
+ nd: ∀a:nS. ∀i:nI a. nD a i → nS
+}.
+
+notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
+notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
+
+notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
+notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
+
+interpretation "D" 'D a i = (nD ? a i).
+interpretation "d" 'd a i j = (nd ? a i j).
+
+ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
+
+notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
+notation "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
+
+interpretation "image" 'Im a i = (image ? a i).
+
+ndefinition Ax_of_nAx : nAx → Ax.
+#A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
+nqed.
+
+ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝
+ sig_intro : ∀x:A.P x → sigma A P.
+
+interpretation "sigma" 'sigma \eta.p = (sigma ? p).
+
+ndefinition nAx_of_Ax : Ax → nAx.
+#A; @ A (I ?);
+##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
+##| #a; #i; *; #x; #_; napply x;
+##]
+nqed.
+
+ninductive ord (A : nAx) : Type[0] ≝
+ | oO : ord A
+ | oS : ord A → ord A
+ | oL : ∀a:A.∀i.∀f:𝐃 a i → ord A. ord A.
+
+nlet rec famU (A : nAx) (U : Ω^A) (x : ord A) on x : Ω^A ≝
+ match x with
+ [ oO ⇒ U
+ | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.∀j:𝐃 x i.𝐝 x i j ∈ Un}
+ | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
+
+ndefinition ord_coverage ≝ λA,U.{ y | ∃x:ord A. y ∈ famU ? U x }.