Skip to content

Instantly share code, notes, and snippets.

@phadej

phadej/Exi.agda Secret

Created September 23, 2020 22:04
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 phadej/828a8e8daf3ec4d90f694f5bafa79356 to your computer and use it in GitHub Desktop.
Save phadej/828a8e8daf3ec4d90f694f5bafa79356 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Exi.agda
module Exi where
open import Data.Product
open import Data.Bool
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
exists : Set _
exists = Σ Set λ a → a
val1 : exists
val1 = Bool , true
val2 : exists
val2 = Bool , false
val1/=val2 : val1 ≡ val2 → ⊥
val1/=val2 ()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment