Skip to content

Instantly share code, notes, and snippets.

@xekoukou

xekoukou/ss.agda

Created October 23, 2019 16:48
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/59912544487c04fa5131b77a15a50697 to your computer and use it in GitHub Desktop.
Save xekoukou/59912544487c04fa5131b77a15a50697 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
ss.agda
data K : Set where
WSet : Set₁
WSet = K → Set
variable
HW HQ : WSet
⊢ : WSet → Set
⊢ ha = ∀ {n} → ha n
postulate
foo : ⊢ HW
goo : ⊢ HQ
goo = foo
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment