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₂