Lambda-calculus stuff

Emdedding universe polymorphism

{-# OPTIONS --no-positivity-check #-}

open import Level as Le
open import Function
open import Data.Maybe renaming (map to _<$>_)

infixl 4 _<*>_
_<*>_ : ∀ {α β} {A : Set α} {B : Set β} -> Maybe (A -> B) -> Maybe A -> Maybe B
just f <*> just x = just (f x)
_      <*> _      = nothing

infixr 2 _‵ℓΠ‵_ _‵Π‵_ _⟶_
infixl 4 _ℓ·_ _·_

record Tag {α β : Level} {A : Set α} (B : (x : A) -> Set β) (x : A) : Set (α ⊔ β) where
  constructor tag
  field detag : B x
open Tag

mutual
  data Type : Maybe Level -> Set where
    ‵Level : Type (just zero)
    ‵Type : ∀ α -> Type (just (suc α))
    _‵ℓΠ‵_ : ∀ {mα} (A : Type mα) {k : ‵⟦ A ⟧ -> Maybe Level}
           -> (∀ x -> Type (k x)) -> Type nothing
    _‵Π‵_ : ∀ {mα mβ} -> (A : Type mα) -> (B : ‵⟦ A ⟧ -> Type mβ) -> Type (_⊔_ <$> mα <*> mβ)
    ‵Lift : ∀ {β α} -> Type (just α) -> Type (just (α ⊔ β))

  ‵⟦_⟧ : ∀ {mα} -> Type mα -> Set
  ‵⟦ ‵Level   ⟧ = Level
  ‵⟦ ‵Type α  ⟧ = Type (just α)
  ‵⟦ A ‵ℓΠ‵ B ⟧ = (x : ‵⟦ A ⟧) -> ‵⟦ B x ⟧
  ‵⟦ A ‵Π‵ B  ⟧ = (x : ‵⟦ A ⟧) -> ‵⟦ B x ⟧
  ‵⟦ ‵Lift A  ⟧ = ‵⟦ A ⟧

_⟶_ : ∀ {mα mβ} -> Type mα -> Type mβ -> Type (_⊔_ <$> mα <*> mβ)
A ⟶ B = A ‵Π‵ λ _ -> B

‵⟦_⟧ᵂ : ∀ {mα} -> Type mα -> Set
‵⟦_⟧ᵂ = Tag ‵⟦_⟧

_<t>_ : ∀ {α β} {A : Type α} {B : ‵⟦ A ⟧ -> Type β}
      -> ((x : ‵⟦ A ⟧) -> ‵⟦ B x ⟧) -> (xᵂ : ‵⟦ A ⟧ᵂ) -> ‵⟦ B (detag xᵂ) ⟧ᵂ
f <t> xᵂ = tag (f (detag xᵂ))

mutual
  data Term : ∀ {mα} -> Type mα -> Set where
    ↑ : ∀ {mα} {A : Type mα} -> ‵⟦ A ⟧ᵂ -> Term A
    ℓ⇧ : ∀ {mα} {A : Type mα} {k : ‵⟦ A ⟧ -> Maybe Level} {B : (x : ‵⟦ A ⟧) -> Type (k x)}
       -> ((t : ‵⟦ A ⟧ᵂ) -> Term (B (detag t))) -> Term (A ‵ℓΠ‵ B)
    ⇧ : ∀ {mα mβ} {A : Type mα} {B : ‵⟦ A ⟧ -> Type mβ}
      -> ((t : ‵⟦ A ⟧ᵂ) -> Term (B (detag t))) -> Term (A ‵Π‵ B)
    _ℓ·_ : ∀ {mα} {A : Type mα} {k : ‵⟦ A ⟧ -> Maybe Level} {B : (x : ‵⟦ A ⟧) -> Type (k x)}
         -> Term (A ‵ℓΠ‵ B) -> (e : Term A) -> Term (B ⟦ e ⟧)
    _·_ : ∀ {mα mβ} {A : Type mα} {B : ‵⟦ A ⟧ -> Type mβ}
        -> Term (A ‵Π‵ B) -> (e : Term A) -> Term (B ⟦ e ⟧)
    ′lift : ∀ {β α} {A : Type (just α)} -> Term A -> Term (‵Lift {β} A)
    ′lower : ∀ {β α} {A : Type (just α)} -> Term (‵Lift {β} A) -> Term A

  ⟦_⟧ : ∀ {mα} {A : Type mα} -> Term A -> ‵⟦ A ⟧
  ⟦ ↑ t      ⟧ = detag t
  ⟦ ℓ⇧ f     ⟧ = λ x -> ⟦ f (tag x) ⟧
  ⟦ ⇧ f      ⟧ = λ x -> ⟦ f (tag x) ⟧
  ⟦ f ℓ· x   ⟧ = ⟦ f ⟧ ⟦ x ⟧
  ⟦ f · x    ⟧ = ⟦ f ⟧ ⟦ x ⟧
  ⟦ ′lift t  ⟧ = ⟦ t ⟧
  ⟦ ′lower t ⟧ = ⟦ t ⟧

plain-↑ : ∀ {mα} {A : Type mα} -> ‵⟦ A ⟧ -> Term A
plain-↑ = ↑ ∘ tag

type-↑ : ∀ {mα} {A : Type mα} -> ‵⟦ A ⟧ -> Term A
type-↑ = ↑ ∘ tag



test-1 : Type (just (suc (suc (suc zero))))
test-1 = ‵Lift (‵Type zero)

test-2 : Term (‵Type zero
            ‵Π‵ λ A -> ‵Type zero
            ‵Π‵ λ B -> (A ⟶ B)
            ‵Π‵ λ f -> (‵Type (suc zero) ‵Π‵ id)
            ⟶ B)
test-2 = ⇧ λ A -> ⇧ λ B -> ⇧ λ f -> ⇧ λ g -> ↑ f · ′lower (↑ g · ↑ (‵Lift <t> A))



open import Relation.Binary.PropositionalEquality

z : Term ((‵Level ⟶ ‵Level) ‵ℓΠ‵ λ k -> ‵Type (suc (k zero)))
z = ℓ⇧ λ k -> plain-↑ (‵Type (detag k zero))

s : Term (((‵Level ⟶ ‵Level) ⟶ ‵Level)
         ‵ℓΠ‵ λ j -> ((‵Level ⟶ ‵Level) ‵ℓΠ‵ λ k -> ‵Type (suc (j k)))
         ⟶ (‵Level ⟶ ‵Level)
         ‵ℓΠ‵ λ k -> ‵Type (suc (k zero ⊔ j (k ∘ suc))))
s = ℓ⇧ λ j -> ⇧ λ r -> ℓ⇧ λ k ->
   plain-↑ (‵Type (detag k zero) ⟶ ⟦ ↑ r ℓ· (⇧ λ α -> ↑ k · (plain-↑ suc · ↑ α)) ⟧)

crescendo : Term (((‵Level ⟶ ‵Level) ⟶ ‵Level)
                 ‵ℓΠ‵ λ j -> ((‵Level ⟶ ‵Level) ‵ℓΠ‵ λ k -> ‵Type (j k))
                 ⟶ ‵Type (j id))
crescendo = ℓ⇧ λ j -> ⇧ λ r -> ↑ r ℓ· plain-↑ id

test-3 : ⟦ crescendo ℓ· ↑ _
             · (s ℓ· ↑ _
             · (s ℓ· ↑ _
             · (s ℓ· ↑ _
             · z))) ⟧ ≡ (‵Type zero
                      ⟶ ‵Type (suc zero)
                      ⟶ ‵Type (suc (suc zero))
                      ⟶ ‵Type (suc (suc (suc zero))))
test-3 = refl



I : ∀ α -> (A : Set α) -> A -> A
I _ _ x = x

Iᵀ : Term (‵Level ‵ℓΠ‵ λ α -> ‵Type α ‵Π‵ λ A -> A ⟶ A)
Iᵀ = ℓ⇧ λ α -> ⇧ λ A -> ⇧ λ x -> ↑ x

open import Data.List

data Listᵀ {mα : _} (A : Type mα) : Set where
  []ᵀ : Listᵀ A
  _∷ᵀ_ : Term A -> Listᵀ A -> Listᵀ A

{-Setω-error : ?
Setω-error = I _ _ I-}

{-Type-nothing-error : ?
Type-nothing-error = Iᵀ ℓ· _ · _ · Iᵀ-}

{-Setω-error : ?
Setω-error = I ∷ []-}

ok-1 : Listᵀ _
ok-1 = Iᵀ ∷ᵀ []ᵀ

{-Setω-error : ?
Setω-error = (∀ α -> Set α) ∷ []-}

ok-2 : List (Type nothing)
ok-2 = (‵Level ‵ℓΠ‵ ‵Type) ∷ []