Skip to content

Instantly share code, notes, and snippets.

@msakai

msakai/JMeq.agda

Created September 26, 2011 11:32
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 msakai/1242059 to your computer and use it in GitHub Desktop.
Save msakai/1242059 to your computer and use it in GitHub Desktop.
Download ZIP
John Major's equality in Agda2
Raw
JMeq.agda
-- John Major's equality is definable in Agda2!
module JMeq where
data JMeq {A : Set} (a : A) : {B : Set} → B → Set where
refl : JMeq a a
JMeq-elim
: {A : Set} → (a a' : A) → (e : JMeq a a')
→ (P : (a' : A) → JMeq a a' → Set)
→ P a refl → P a' e
JMeq-elim a .a refl P P-prf = P-prf
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment