2024-05-12 14:29:09 -04:00
|
|
|
|
-- inspired by https://github.com/agda/agda/issues/2556
|
|
|
|
|
|
|
|
|
|
|
|
postulate0 A : ★
|
|
|
|
|
|
|
|
|
|
|
|
def0 ZZ : ★ = 0 ≡ 0 : ℕ
|
|
|
|
|
|
|
|
|
|
|
|
def reflZ : ZZ = δ _ ⇒ 0
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
namespace erased {
|
|
|
|
|
|
def0 ZZA : ★ = 0.ZZ → A
|
|
|
|
|
|
|
|
|
|
|
|
def propeq : (x : ZZA) → x ≡ (λ _ ⇒ x reflZ) : ZZA =
|
|
|
|
|
|
λ x ⇒ δ _ ⇒ x
|
|
|
|
|
|
|
|
|
|
|
|
def defeq : 0.(P : ZZA → ★) → 0.(x : ZZA) → P (λ _ ⇒ x reflZ) → P x =
|
|
|
|
|
|
λ P x p ⇒ p
|
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
namespace unrestricted {
|
|
|
|
|
|
def0 ZZA : ★ = ω.ZZ → A
|
|
|
|
|
|
|
|
|
|
|
|
def defeq : 0.(P : ZZA → ★) → 0.(x : ZZA) → P (λ _ ⇒ x reflZ) → P x =
|
|
|
|
|
|
λ P x p ⇒ p
|
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
namespace linear {
|
|
|
|
|
|
def0 ZZA : ★ = 1.ZZ → A
|
|
|
|
|
|
|
2024-05-12 14:32:32 -04:00
|
|
|
|
#[fail "λ _ ⇒ x reflZ is not equal to x"]
|
2024-05-12 14:29:09 -04:00
|
|
|
|
def defeq : 0.(P : ZZA → ★) → 0.(x : ZZA) → P (λ _ ⇒ x reflZ) → P x =
|
|
|
|
|
|
λ P x p ⇒ p
|
|
|
|
|
|
}
|
