Generalize Elements, 2 level terms.

GenEl.agda

record Univ : Set₁ where
  field
    U : Set
    El : U → Set
open Univ

record GeneralizedElement : Set₁ where
   constructor _∋_∋_
   field
    𝒰 : Univ
    ty : 𝒰 .U
    elem : (𝒰 .El) ty


open import Data.Nat
open import Data.String
open import Data.Bool
open import Function hiding (_∋_)




data Types₁ : Set where 𝕓 𝕟 : Types₁
data Types₂ : Set where
  𝕤 : Types₂
  _⇒_ : Types₂ → Types₂ → Types₂

U₁ : Univ
U₁ .U = Types₁
U₁ .El 𝕓 = Bool
U₁ .El 𝕟 = ℕ

U₂ : Univ
U₂ .U = Types₂
U₂ .El = El'
  where 
    El' : Types₂ → Set
    El' 𝕤 = String
    El' (x ⇒ y) = El' x → El' y


ex : GeneralizedElement
ex = U₂ ∋ (𝕤 ⇒ 𝕤) ∋ (λ s → s ++ "foo")


ex2 : GeneralizedElement
ex2 = U₁ ∋ 𝕓 ∋ false