Então esse é o problema que tenho em uma tarefa de casa, tenho que provar que bool não é igual a top, também tenho um sinal de igual redefinido que devo usar.
module TranspEq where
open import Agda.Primitive
open import Agda.Builtin.Equality renaming (_≡_ to _≡ᵣ_ ; refl to reflᵣ)
open import Agda.Builtin.Nat renaming (Nat to ℕ)
_≡_ : ∀{ℓ}{A : Set ℓ} → A → A → Setω
_≡_ {A = A} a b = ∀{κ}(P : A → Set κ) → P a → P b
infix 4 _≡_
-- define conversion between the two 'equals'
transp : ∀{ℓ}{A : Set ℓ}(a b : A) → a ≡ b → a ≡ᵣ b
transp a b x = x (_≡ᵣ_ a) reflᵣ
untransp : ∀{ℓ}{A : Set ℓ}(a b : A) → a ≡ᵣ b → a ≡ b
untransp a .a reflᵣ P y = y
-- prove properties of ≡
refl : ∀{ℓ}{A : Set ℓ}{a : A} → a ≡ a
refl P a = a
sym : ∀{ℓ}{A : Set ℓ}{a b : A} → a ≡ b → b ≡ a
sym {l} {A} {a} {b} = λ z P → z (λ z₁ → (x : P z₁) → P a) (λ x → x)
trans : ∀{ℓ}{A : Set ℓ}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans = λ a b P c → b P (a P c)
cong : ∀{ℓ κ}{A : Set ℓ}{B : Set κ}(f : A → B){a b : A} → a ≡ b → f a ≡ f b
cong = λ f a P → a (λ b → P (f b))
-- types
record ⊤ : Set where
instance constructor tt
data Bool : Set where
true : Bool
false : Bool
data ⊥ : Set where
_≢_ : ∀{ℓ}{A : Set ℓ} → A → A → Setω
a ≢ b = a ≡ b → ⊥
Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ = {!!}
Eu tentei algo assim, mas sim, não consegui:/não consigo criar um predicado que seja Set -> Set
⊤≠⊥ : ⊤ ≢ ⊥
⊤≠⊥ x = x (λ x → x) tt
Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ x = ⊤≠⊥ λ P y → {! !}
--Bool≠⊤ : Bool ≢ ⊤
--Bool≠⊤ x = x (λ y → y tt) p
-- where
-- p : {Set : (Bool ≡ ⊤)}→ ⊥
-- p (true ≡ tt) = ⊥
-- p (false ≡ tt) = ⊥