Slider comments on Set-like mathematics in type theory

[Slider]

Practising expressing old interests in a new language:

$S=S_{form}/{\le }_{Sf}$

$S_{bucket}=P\left(S\right)$

$S_{form}=a:S_{bucket},b:S_{bucket}|numeri{c}_S(a,b)$

$pair\left(a\right):S_{form}\to S_{bucket}\times S_{bucket}$

$numeri{c}_S(a,b)=\forall x(x\in a(\forall y{\le }_{Sb}\left(pair\right(x),pair(y\left)\right)\left)\right):S_{bucket}\times S_{bucket}\to \Omega$

$firstborn\left(a\right):S\to S_{form}$

${\le }_{Sf}(a,b)={\le }_{Sb}\left(pair\right(a),pair(b\left)\right):S_{form}\times S_{form}\to \Omega$${\le }_{Sb}(a,b,c,d)=\neg \exists x(x\in a\wedge {\le }_{Sn}(c,d,x\left)\right)\wedge \neg \exists y(y\in d\wedge {\ge }_{Sn}(a,b,y\left)\right):S_{bucket}\times S_{bucket}\times S_{bucket}\times S_{bucket}\to \Omega$

${\le }_{Sn}(c,d,x)={\le }_{Sb}(c,d,pair(firstborn\left(x\right)\left)\right):S_{bucket}\times S_{bucket}\times S\to \Omega$

${\ge }_{Sn}(a,b,y)={\le }_{Sb}\left(pair\right(firstborn\left(y\right)),a,b):S_{bucket}\times S_{bucket}\times S\to \Omega$

It is a known system and a terribly recursive one. One can get going by the fact that $\varnothing \in P\left(A\right),A\in U$