Type: Type can lead to Russell's paradox about cicada-solo HOT 3 OPEN

datatype Set {
  set(X: Type, y: (X) -> Set): Set
}

function carrier(s: Set): Type {
  return induction(s) {
    (_) => Type
    case set(x, _) => x
  }
}

function index(s: Set): (carrier(s)) -> Set {
  return induction(s) {
    (s) => (carrier(s)) -> Set
    case set(_, y) => y
  }
}

function In(a: Set, b: Set): Type {
  return [ x : carrier(b) | Equal(Set,a,index(b)(x)) ]
}

function NotIn(a: Set, b: Set): Type {
  return (In(a, b)) -> Absurd
}

let Δ = Set.set([s: Set| NotIn(s,s)], (pair) => car(pair))
// check! Δ: Set

// For every x ∉ x, x ∈ Δ. (By definition of Δ.)
function xNotInx_xInΔ(x: Set, xNotInx: NotIn(x, x)): In(x, Δ) {
  return cons(cons(x, xNotInx), refl)
}

function equal_swap
  ( implicit A: Type
  , implicit x: A
  , implicit y: A
  , xy_equal: Equal(A, x, y)
  ):Equal(A, y, x) {
  return replace
    ( xy_equal
    , (w) => Equal(A, w, x)
    , refl
    )
}

// For every x ∈ Δ, x ∉ x. (By definition of Δ.)
function xInΔ_xNotInx(x: Set, xInΔ: In(x, Δ)): NotIn(x,x) {
  return replace
    ( equal_swap(cdr(xInΔ))
    , (s) => NotIn(s,s)
    , cdr(car(xInΔ))
    )
}

// Hence, Δ ∉ Δ.
let ΔNotInΔ: NotIn(Δ, Δ) = (ΔInΔ) => { return xInΔ_xNotInx(Δ, ΔInΔ)(ΔInΔ) }

// However, that means Δ ∈ Δ, which is absurd.
let falso: Absurd = ΔNotInΔ(xNotInx_xInΔ(Δ, ΔNotInΔ))

RangeError: Maximum call stack size exceeded
    at ImplicitApCore.evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/exps/implicit-pi/implicit-ap-core.js:37:13)
    at evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/core/evaluate.js:7:16)
    at ImplicitApCore.evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/exps/implicit-pi/implicit-ap-core.js:38:57)
    at evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/core/evaluate.js:7:16)
    at ImplicitApCore.evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/exps/implicit-pi/implicit-ap-core.js:38:57)
    at evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/core/evaluate.js:7:16)
    at ApCore.evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/exps/pi/ap-core.js:36:49)
    at evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/core/evaluate.js:7:16)
    at ApCore.evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/exps/pi/ap-core.js:36:49)
    at evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/core/evaluate.js:7:16)

datatype WTF {
  wtf: Absurd
}
check! WTF.wtf: Absurd