The question is about Observational Type Theory.
Consider this setting:
data level : Set where
# : ℕ -> level
ω : level
_⊔_ : level -> level -> level
# α ⊔ # β = # (α ⊔ℕ β)
_ ⊔ _ = ω
_⊔ᵢ_ : level -> level -> level
α ⊔ᵢ # 0 = # 0
α ⊔ᵢ β = α ⊔ β
mutual
Prop = Univ (# 0)
Type = Univ ∘ # ∘ suc
data Univ : level -> Set where
bot : Prop
top : Prop
nat : Type 0
univ : ∀ α -> Type α
σ≡ : ∀ {α β γ} -> α ⊔ β ≡ γ -> (A : Univ α) -> (⟦ A ⟧ -> Univ β) -> Univ γ
π≡ : ∀ {α β γ} -> α ⊔ᵢ β ≡ γ -> (A : Univ α) -> (⟦ A ⟧ -> Univ β) -> Univ γ
πᵤ : ∀ {α} -> (A : Univ α) {k : ⟦ A ⟧ -> level} -> (∀ x -> Univ (k x)) -> Univ ω
⟦_⟧ : ∀ {α} -> Univ α -> Set
⟦ bot ⟧ = ⊥
⟦ top ⟧ = ⊤
⟦ nat ⟧ = ℕ
⟦ univ α ⟧ = Univ (# α)
⟦ σ≡ _ A B ⟧ = Σ ⟦ A ⟧ λ x -> ⟦ B x ⟧
⟦ π≡ _ A B ⟧ = (x : ⟦ A ⟧) -> ⟦ B x ⟧
⟦ πᵤ A B ⟧ = (x : ⟦ A ⟧) -> ⟦ B x ⟧
prop = univ 0
type = univ ∘ suc
We have a stratified hierarchy of universes: Prop : Type 0 : Type 1 : ... (where Prop is impredicative), the codes for Σ- and Π-types and one additional code πᵤ for "universe polymorphic Π-types". Just like in Agda ∀ α -> Set α has [the hidden] type Setω, π nat univ has type Univ ω.
With some shortcuts
_&_ : ∀ {α β} -> Univ α -> Univ β -> Univ (α ⊔ β)
A & B = σ A λ _ -> B
_⇒_ : ∀ {α β} -> Univ α -> Univ β -> Univ (α ⊔ᵢ β)
A ⇒ B = π A λ _ -> B
_‵π‵_ : ∀ {α β} -> (A : Univ α) -> (⟦ A ⟧ -> Univ β) -> Univ (α ⊔ᵢ β)
_‵π‵_ = π
_‵πᵤ‵_ : ∀ {α} -> (A : Univ α) {k : ⟦ A ⟧ -> level} -> (∀ x -> Univ (k x)) -> Univ ω
_‵πᵤ‵_ = πᵤ
we can define many functions using the target language constructs, e.g.
_≟ₚ_ : ⟦ nat ⇒ nat ⇒ prop ⟧
zero ≟ₚ zero = top
suc n ≟ₚ suc m = n ≟ₚ m
_ ≟ₚ _ = bot
In an imaginary language we can identify codes and the corresponding types, thus forming a closed reflexive universe (we also need some first-order representation of data types, but that's another story). But consider the usual equality of types:
Eq : ∀ {α β} -> Univ α -> Univ β -> Prop
How to embed this in the target language? We can write
EqEmb : ⟦ (nat ‵πᵤ‵ λ α → nat ‵πᵤ‵ λ β → univ α ⇒ univ β ⇒ prop) ⟧
but notice that the target language doesn't contain anything about ω. In Eq we can pattern match on the arguments like this:
Eq (πᵤ A₁ B₁) (πᵤ A₂ B₂) = ...
α and β both become ω and everything is fine. But in EqEmb we can't pattern-match like this, because in univ α α is a number and cannot be ω, so ⟦ univ α ⟧ is never Univ ω.
Let's say we can pattern match on plain Agda types. Then we could write a function that determines whether some value is a function:
isFunction : ∀ {α} {A : Set α} -> A -> Bool
isFunction {A = Π A B} _ = true
isFunction _ = false
But what if B is "universe dependent" and has, say, this type: ∀ α -> Set α? Then Π A B has type Setω and α is unified with ω. But if we could instantiate level variables with ω, then we could write things like
Id : Set ω
Id = ∀ α -> (A : Set α) -> A -> A
id : Id
id α A x = x
id ω Id id ~> id
That's impredicative (Although I don't know whether this particular form of impredicativity leads to inconsistency. Does it?).
So we can't add ω as a legal level to the target language and we can't pattern match on Set α in the presence of "universe dependent" functions. Thus the "reflexive" equality
EqEmb : ⟦ (nat ‵πᵤ‵ λ α → nat ‵πᵤ‵ λ β → univ α ⇒ univ β ⇒ prop) ⟧
is not defined for all universe polymorphic functions (not "universe dependent"). E.g. the type of type of map
map : ∀ {α β} {A : Set α} {B : Set β} -> (A -> B) -> List A -> List B
is Setω and we can't ask whether Eq (typeOf emb-map) (typeOf emb-map), because in Eq A B the type of A is ⟦ univ α ⟧, which is a "finite" universe (the same holds for B).
So is it possible to embed OTT in itself in a well-typed way? If not, can we cheat somehow? Can we pattern match on Set α in the presense of "universe dependent" functions like everything is fine?
