let bottomat : ℕ → ℕ → Type
  ≔ ℕ-ind (λ_. ℕ → Type)
          (λ_. ⊥)
          (λn.λban. ℕ-ind (λ_. Type) ⊤ (λm.λ_. ban m))

let fin : ℕ → Type
  ≔ λn. Σ (m : ℕ) bottomat n m

let bool : Type
  ≔ fin 2

let false : bool
  ≔ ⟨0, ★⟩

let true : bool
  ≔ ⟨1, ★⟩

{-
let boolind : Π (C : bool → Type) C false → C true → Π (b : bool) C b
  ≔ λC.λCf.λCt. Σ-ind ℕ (bottomat 2) C (λn.λu. ℕ-ind (λm. Id ℕ m n → C (n, u))
                                                     (λp. ?)
                                                     (λn.λ_.λp. ℕ-ind (λm. Id ℕ m n → C (n, u)) (λp. ?) (λm.λ_.λp. ⊥-ind (λ_. C (n, u)) ?)))
-}