granule_dup.gr

data Bool =
  Bool (exists {n : Nat} . exists {m : Nat} .
    (forall {a : Type} . a [n] -> a [m] -> a))

true : Bool
true = 
  let true_ex_m = 
    pack <0, (/\(a : Type) -> \([x] : a [1]) -> \([y] : a [0]) -> x)>
      as exists {m : Nat} .
        (forall {a : Type} . a [1] -> a [m] -> a) in
  let true_ex_n = 
    pack <1, true_ex_m>
      as exists {n : Nat} . exists {m : Nat} .
        (forall {a : Type} . a [n] -> a [m] -> a) in
  Bool true_ex_n

false : Bool
false = 
  let false_ex_m = 
    pack <1, (/\(a : Type) -> \([x] : a [0]) -> \([y] : a [1]) -> y)>
      as exists {m : Nat} .
        (forall {a : Type} . a [0] -> a [m] -> a) in
  let false_ex_n = 
    pack <0, false_ex_m>
      as exists {n : Nat} . exists {m : Nat} .
        (forall {a : Type} . a [n] -> a [m] -> a) in
  Bool false_ex_n

dup : Bool [1] -> Bool
dup [Bool ex_n] =
  unpack <n, ex_m> = ex_n in
  unpack <m, raw> = ex_m in
  raw @ Bool [true] [false]