Skip to content

Instantly share code, notes, and snippets.

@xekoukou

xekoukou/.agda

Created December 27, 2019 17:08
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/75558eaa315b74b875cabab6be8056c3 to your computer and use it in GitHub Desktop.
Save xekoukou/75558eaa315b74b875cabab6be8056c3 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
.agda
module HL5 where
open import Agda.Builtin.Unit
import Level as L
postulate
World : Set
HSet : ∀{α} → Set (L.suc α)
HSet {α} = {〈w〉 : World} → Set α
↓ : ∀{α} → ∀{HA : HSet {α}} → ⊤
↓ = {!!}
↓¡_¡ : ∀{α} → ∀{HA : HSet {α}} → ⊤
↓¡_¡ = {!↓!} --ctrl - u u .
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment