False.agda

{-# OPTIONS --prop --type-in-type #-}
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
module False (extensionality : ∀ (A B : Prop) → A ≡ B) where

⊥ : Prop
⊥ = ∀ (p : Prop) → p

⊤ : Prop
⊤ = ⊥ → ⊥

cast : ∀ (A B : Prop) → A ≡ B → A → B
cast _ _ refl x = x

false : ⊥
false P = cast ⊤ P (extensionality ⊤ P) (λ z → z ⊤ z)