pi/tests/fin.pi

24 lines
711 B
Plaintext
Raw Normal View History

2022-07-26 07:57:44 +02:00
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)) ?)))
-}