24 lines
719 B
Plaintext
24 lines
719 B
Plaintext
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)) ?)))
|
||
-}
|