Agda proving Bool ≢ ⊤

Question

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) = ⊥

Answer 1

The only way to prove that two sets are different in Agda is to exploit their differences in terms of cardinality.

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
... | ()

Answer 2

The first step is to think of a predicate P : Set → Set such that P Bool is inhabited and P ⊤ is refutable, or vice versa. Agda won't give you much assistance in picking a good one because Set → Set is a very vague type, with lots of inhabitants (most of them useless to you). I'll leave this choice of P mostly as an exercise, but give some hints, given that I guess finding such a P is the main point of this homework question.

I actually found it easier to do the vice versa thing – pick a P with P ⊤ but P Bool → ⊥. In producing such a P, you'll typically take a T : Set using a λ-abstraction. This T will be instantiated to ⊤ and Bool by the definition of _≡_. With such a T, you can universally quantify over elements using (x : T) → .... If you've been introduced to Σ-types (dependent pairs), you can use them for existential quantification, though I ultimately found a property that needed only universal quantification. You can't use _≡_ to produce the required Set because of size issues, but you can use _≡ᵣ_ in its place. You can't pattern-match on T or its inhabitants, because they are not of data or record type.

I needed a lemma true≢ᵣfalse : true ≡ᵣ false → ⊥. I proved it via absurd pattern-matching (()), but it should also be provable by untransp and defining a property of Booleans that's true of true and false of false. This property is easier to define, in the sense that it's of type Bool → Set, so you can pattern-match on the Bool argument.

The resulting proof should look something like the following. I would recommend starting with just true≢ᵣfalse ? and filling in P and p, which will then tell you how many arguments sym q P p should take.

Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ q = true≢ᵣfalse (sym q P p {- instantiation of universal quantifiers -})
  where
  P : Set → Set
  P T = ?

  p : P ⊤
  p = ?