Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade

Blaisorblade/foo.agda

Created July 2, 2019 18:14
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 Blaisorblade/6bb4e6b71f9d13dc50311315906018b6 to your computer and use it in GitHub Desktop.
Save Blaisorblade/6bb4e6b71f9d13dc50311315906018b6 to your computer and use it in GitHub Desktop.
Download ZIP
Level coercions in Agda
Raw
foo.agda
module foo where
open import Data.Nat
open import Agda.Primitive
open import Level
foo = λ (T : (∀ (X : Set (lsuc lzero)) → X → X)) (X : Set lzero) → T (Lift _ X)
@mietek
Copy link

mietek commented Jul 2, 2019 •
edited

In slightly more readable Agda:

foo : (∀ (X : Set₁) → X → X) → (∀ (Y : Set₀) → Lift _ Y → Lift _ Y)
foo = λ (T : (∀ (X : Set₁) → X → X)) → (λ (Y : Set₀) → (T (Lift _ Y)))

I think what I would like to write is something like:

py : Pretype
py = all 1 (tyvar 0 ⊃ tyvar 0) ⊃ all 0 (tyvar 0 ⊃ tyvar 0)

pm : Preterm
pm = lam (all 1 (tyvar 0 ⊃ tyvar 0)) (tylam 0 (var 0 ty∙ tyvar 0))

ty : Type [] py
ty = all (tyvar 0 ⊃ tyvar 0) ⊃ all (tyvar 0 ⊃ tyvar 0)

tm : Term [] [] pm ty
tm = lam (all (tyvar 0 ⊃ tyvar 0)) (tylam (var 0 ty∙ var 0))

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment