3 inductive datatype encodings with self

ind.md

Scott encoding (λP λct0 λct1 λct2 ... (ctN f0 f1 f2 ...)):

Bool
: *
= $self
  ∀(P: ∀(x: Bool) *)
  ∀(t: (P Bool.true))
  ∀(f: (P Bool.false))
  (P self)

Bool.true  : Bool = ~λP λt λf t
Bool.false : Bool = ~λP λt λf f

Bool.match
: ∀(b: Bool)
  ∀(P: ∀(x: Bool) *)
  ∀(t: (P Bool.true))
  ∀(f: (P Bool.false))
  (P b)
= λb λP λt λf
  (~b P t f)

Tagged Tuple encoding ((#tag, f0, f1, f2, ...)):

QBool.true  : QBool = ~λP (#0, λx x)
QBool.false : QBool = ~λP (#1, λx x)

QBool : * =
  $self
  ∀(P: ∀(x: QBool) *) 
  Σ(t: #U60)
  ∀(x: match t {
    0: (P QBool.true) // <- fields would be Σ's
    1: (P QBool.false)
    +: ∀(x: Empty) *
  })
  (P self)

QBool.match
: ∀(a: QBool)
  ∀(P: ∀(x: QBool) *)
  ∀(t: (P QBool.true))
  ∀(f: (P QBool.false))
  (P a)
= λa λP λt λf
  let (tag, val) = (~a P)
  #match tag = tag {
    #0: (val t)
    #1: (val f)
    #+: (val λe (Empty.absurd e *))
  }

Tagged Lam-Tuple encoding (λP λt (t #tag f0 f1 f2 ...)):

QBool2.true  : QBool2 = ~λP λnew (new #0)
QBool2.false : QBool2 = ~λP λnew (new #1)
QBool2.bad   : QBool2 = ~λP λnew (new #2 ?impossible)

QBool2 : * =
  $self
  ∀(P: ∀(x: QBool2) *)
  ∀(new: ∀(tag: #U60) #match tag = tag {
    #0: (P QBool2.true)  // <- fields would be ∀'s
    #1: (P QBool2.false)
    #+: ∀(e: Empty) *
  }: *)
  (P self)

QBool2.match
: ∀(a: QBool2)
  ∀(P: ∀(x: QBool2) *)
  ∀(t: (P QBool2.true))
  ∀(f: (P QBool2.false))
  (P a)
= λa λP λt λf
  (~a P λtag #match tag = tag {
    #0: t
    #1: f
    #+: λe (~e λx(*))
  })