cicada-lang / cicada-solo Goto Github PK

datatype Bool {
  true: Bool
  false: Bool
}

datatype Nat {
  zero: Bool
  suc(pred: Nat): Bool
}

check! Nat.zero : Bool

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)
}

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

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

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

I infer the type to be:
  (_: [x1: induction (car(car(xInΔ))) { (_) => Type case set(x1, _) => x1 } | Equal(Set, car(car(xInΔ)), induction (car(car(xInΔ))) { (s1) => (_: induction (s1) { (_) => Type case set(x2, _) => x2 }) -> Set case set(_, y, _1) => y(_1) }(x1))]) -> Absurd
But the expected type is:
  (_: [x1: induction (x) { (_) => Type case set(x1, _) => x1 } | Equal(Set, x, induction (x) { (s1) => (_: induction (s1) { (_) => Type case set(x2, _) => x2 }) -> Set case set(_, y, _1) => y(_1) }(x1))]) -> Absurd

Paradox.cic:
 39 |
 40 |// For every x ∈ Δ, x ∉ x. (By definition of Δ.)
 41 |function xInΔ_xNotInx(x: Set, xInΔ: In(x, Δ)): NotIn(x,x) {
 42 |  return cdr(car(xInΔ))
 43 |}
 44 |