26 lines
820 B
Plaintext
26 lines
820 B
Plaintext
load "misc.quox"
|
||
|
||
namespace eta {
|
||
|
||
def0 Π : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) → B x
|
||
def0 Σ : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) × B x
|
||
|
||
def0 function : (A : ★) → (B : A → Type) → (P : Π A B → ★) → (f : Π A B) →
|
||
P (λ x ⇒ f x) → P f =
|
||
λ A B P f p ⇒ p
|
||
|
||
def0 box : (A : ★) → (P : [ω.A] → ★) → (e : [ω.A]) →
|
||
P [case1 e return A of {[x] ⇒ x}] → P e =
|
||
λ A P e p ⇒ p
|
||
|
||
def0 pair : (A : ★) → (B : A → ★) → (P : Σ A B → ★) → (e : Σ A B) →
|
||
P (fst e, snd e) → P e =
|
||
λ A B P e p ⇒ p
|
||
|
||
-- not exactly η, but kinda related
|
||
def0 from-false : (A : ★) → (P : (0.False → A) → ★) → (f : 0.False → A) →
|
||
P (void A) → P f =
|
||
λ A P f p ⇒ p
|
||
|
||
}
|