Question about Theory of the observational type .
Consider this parameter:
data level : Set where
We have a stratified hierarchy of universes: Prop : Type 0 : Type 1 : ... (where Prop is impractical), codes for Σ- and Π types and one additional πᵤ code for "polymorphic Π types of the universe." As in Agda ∀ α -> Set α has the [hidden] type Setω , π nat univ has the 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 (kx)) -> Univ ω _‵πᵤ‵_ = πᵤ
we can define many functions using constructions of the target language, for example
_≟ₚ_ : ⟦ nat ⇒ nat ⇒ prop ⟧ zero ≟ₚ zero = top suc n ≟ₚ suc m = n ≟ₚ m _ ≟ₚ _ = bot
In an imaginary language, we can identify codes and corresponding types, forming a closed reflexive universe (we also need some representation of first-order data types, but that's a different story). But consider the usual type equality:
Eq : ∀ {α β} -> Univ α -> Univ β -> Prop
How to paste this into the target language? We can write
EqEmb : ⟦ (nat ‵πᵤ‵ λ α → nat ‵πᵤ‵ λ β → univ α ⇒ univ β ⇒ prop) ⟧
but note that the target language does not contain anything about ω . In Eq we can match the pattern with the following arguments:
Eq (πᵤ A₁ B₁) (πᵤ A₂ B₂) = ...
α and β both become ω , and everything is in order. But in EqEmb we cannot match the pattern in this way, because in univ α α there is a number and cannot be ω , therefore ⟦ univ α ⟧ never Univ ω .
Say we can map a pattern to simple Agda types. Then we could write a function that determines whether some value is a function:
isFunction : ∀ {α} {A : Set α} -> A -> Bool isFunction {A = Π AB} _ = true isFunction _ = false
But what if B is “universe dependent” and has, say, this type: ∀ α -> Set α ? Then Π AB is of type Setω , and α unified with ω . But if we could create 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
This is impractical (although I don’t know if this particular form of unpredictability leads to inconsistency.)? //
Thus, we cannot add ω as the legal level to the target language, and we cannot match the correspondence in Set α in the presence of functions that depend on the “universe”. Thus, "reflexive" equality
EqEmb : ⟦ (nat ‵πᵤ‵ λ α → nat ‵πᵤ‵ λ β → univ α ⇒ univ β ⇒ prop) ⟧
not defined for all polymorphic functions of the universe (not "unit dependent"). For instance. type of map type
map : ∀ {α β} {A : Set α} {B : Set β} -> (A -> B) -> List A -> List B
is Setω , and we cannot ask if there is Eq (typeOf emb-map) (typeOf emb-map) , because in Eq AB type A has ⟦ univ α ⟧ , which is a “finite” universe (the same is true for B )
. Is it possible to embed OTT in a well-typed way? If not, can we somehow cheat? Can we match the coincidence on Set α in the presence of “all-dependent” functions, such as everything is normal?