Skip to content

Instantly share code, notes, and snippets.

@caotic123

caotic123/gist:019696f91d15e593c353a00ad4641d89

Last active November 9, 2019 16:39
Show Gist options
  • Save caotic123/019696f91d15e593c353a00ad4641d89 to your computer and use it in GitHub Desktop.
Save caotic123/019696f91d15e593c353a00ad4641d89 to your computer and use it in GitHub Desktop.
Download ZIP
Axiom K in Key
Raw
gistfile1.txt
In Agda :
{-# OPTIONS --with-K #-} -- This is optional just be aware that overrides the option --without-K
data _≡_ {w : Set} (_x : w) : w -> Set where
refl : _x ≡ _x
axiom_k : ∀ {A : Set} {a : A} (P : ∀ (H : a ≡ a) -> Set) (H : P refl) (E : a ≡ a) -> (P E)
axiom_k p H refl = H
In Kei :
Rule A : Type.
Rule ≡ : (forall (n : A) (n' : A) -> Type).
Rule refl : (forall (n : A) -> (≡ n n)).
axiom_k = (\(forall (a : A) (T : (forall (H : (≡ a a)) -> Type)) (p : (T (refl a))) (e : (≡ a a)) -> (T e)) | _ P y H =>
[H of (P H)
|{x}(refl x) => y
]
).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment