So this is the problem I have in a homework task, I have to prove that bool is not equal with top, also I have a redefined equalsign that I have to use.
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≠⊤ = {!!}
I tried something like this, but yeah I couldn't succeed :/ can't create a predicate that is 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) = ⊥
In case of Bool
and ⊤
this is particularly handy to exploit, because every element of ⊤
is equal to every other element of it, which isn't true for Bool
(true
isn't equal to false
). Hence all you need is
Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ x with sym x (λ A -> (x y : A) -> x ≡ᵣ y) (λ _ _ -> reflᵣ) true false
... | ()