Skip to content

Instantly share code, notes, and snippets.

@aljce

aljce/False.agda

Created November 22, 2019 02:58
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save aljce/b8981c618fb020fce048ec5fdd1d90d1 to your computer and use it in GitHub Desktop.
Save aljce/b8981c618fb020fce048ec5fdd1d90d1 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment