tweak quantities in eta.from-false
This commit is contained in:
parent
115fbce43c
commit
9c3fbf93fd
|
@ -18,8 +18,8 @@ def0 pair : (A : ★) → (B : A → ★) → (P : Σ A B → ★) → (e : Σ A
|
||||||
λ A B P e p ⇒ p
|
λ A B P e p ⇒ p
|
||||||
|
|
||||||
-- not exactly η, but kinda related
|
-- not exactly η, but kinda related
|
||||||
def0 from-false : (A : ★) → (P : (False → A) → ★) → (f : False → A) →
|
def0 from-false : (A : ★) → (P : (0.False → A) → ★) → (f : 0.False → A) →
|
||||||
P (λ x ⇒ void A x) → P f =
|
P (void A) → P f =
|
||||||
λ A P f p ⇒ p
|
λ A P f p ⇒ p
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in New Issue