Skip to content

Instantly share code, notes, and snippets.

@xekoukou

xekoukou/aa.agda

Created October 23, 2019 19:26
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 xekoukou/55dc1344d8d08bb55fac1723ea336de4 to your computer and use it in GitHub Desktop.
Save xekoukou/55dc1344d8d08bb55fac1723ea336de4 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
aa.agda
data Bool : Set where
true : Bool
false : Bool
data D : Set where
d : D
data E : Set where
e : E
HSet : Set₁
HSet = {b : Bool} → Set
⊨ : HSet → Set
⊨ HA = HA {true}
G : HSet
G {true} = E
G {false} = D
boo : ⊨ (G {false})
boo = d
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment