Skip to content

Instantly share code, notes, and snippets.

@pnlph

pnlph/sort.agda

Last active May 6, 2020 14:02
Show Gist options
  • Save pnlph/c0b034cfecb7cab9285bd4bc0aefe785 to your computer and use it in GitHub Desktop.
Save pnlph/c0b034cfecb7cab9285bd4bc0aefe785 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
sort.agda
module sort where
-- Polymorphic types
-- Not the framework of pure type systems!
-- Reference https://jesper.sikanda.be/posts/agdas-new-sorts.html
------------------------------------------------------------
-- id₁ : id-sort₁ : Setω
-- with Level, Setω
------------------------------------------------------------
module polymorphic-ω where
-- polymorphic identity function
-- we need the Level type
open import Agda.Primitive using (Level)
id₁ : (l : Level) (A : Set l) (x : A) → A
id₁ l _ a = a
-- Now, we need to import Setω
open import Agda.Primitive using (Setω)
id-sort₁ : Setω
id-sort₁ = (l : Level) (A : Set l) (x : A) → A
-- id₁ : id-sort₁ : Setω
_ : id-sort₁
_ = id₁
_ : Setω
_ = id-sort₁
------------------------------------------------------------
-- ∀ {l} → id₂ : id-sort₂ : Set (lsuc l)
-- with lsuc
------------------------------------------------------------
module polymorphic-lsuc where
-- polymorphic identity function
id₂ : ∀ {l} (A : Set l) → A → A
id₂ _ a = a
-- We need to import lsuc
open import Agda.Primitive using (lsuc)
id-sort₂ : ∀ {a} → Set (lsuc a)
id-sort₂ {l} = (A : Set l) → A → A
-- id₁ : id-sort₁ : Setω
_ : ∀ {l} → id-sort₂ {l}
_ = id₂
_ : ∀ {l} → Set (lsuc l)
_ = id-sort₂
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment