OTT中的自我表示与宇宙

Question

问题是关于观察型理论的。

考虑一下这一背景：

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

我们有一个分层的宇宙层次：Prop : Type 0 : Type 1 : ... ( Prop是非谓词的)，Σ-和Π-类型的代码，以及“宇宙多态Π-类型”的附加代码πᵤ。就像在Agda中，∀ α -> Set α有隐藏类型Setω，π nat univ有类型Univ ω。

用一些捷径

_&_ : ∀ {α β} -> 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 ω
_‵πᵤ‵_ = πᵤ

我们可以使用目标语言构造来定义许多函数。

_≟ₚ_ : ⟦ nat ⇒ nat ⇒ prop ⟧
zero  ≟ₚ zero  = top
suc n ≟ₚ suc m = n ≟ₚ m
_     ≟ₚ _     = bot

在一种假想的语言中，我们可以识别代码和相应的类型，从而形成一个封闭的自反宇宙(我们还需要一些数据类型的一阶表示，但这是另一个故事)。但是，考虑到通常的类型相等：

Eq : ∀ {α β} -> Univ α -> Univ β -> Prop

如何将其嵌入到目标语言中？我们可以写

EqEmb : ⟦ (nat ‵πᵤ‵ λ α → nat ‵πᵤ‵ λ β → univ α ⇒ univ β ⇒ prop) ⟧

但是请注意，目标语言不包含任何关于ω的内容。在Eq中，我们可以对如下参数进行模式匹配：

Eq (πᵤ A₁ B₁) (πᵤ A₂ B₂) = ...

α和β都变成了ω，一切都很好。但在EqEmb中，我们不能像这样进行模式匹配，因为在univ α中，α是一个数字，不能是ω，所以⟦ univ α ⟧永远不是Univ ω。

假设我们可以在普通Agda类型上进行模式匹配。然后，我们可以编写一个函数来确定某个值是否是一个函数：

isFunction : ∀ {α} {A : Set α} -> A -> Bool
isFunction {A = Π A B} _ = true
isFunction             _ = false

但是，如果B是“宇宙依赖的”，并且有，比方说，这种类型：∀ α -> Set α？然后Π A B具有Setω类型，α与ω统一。但是，如果我们可以用ω实例化级别变量，那么我们就可以编写如下

Id : Set ω
Id = ∀ α -> (A : Set α) -> A -> A

id : Id
id α A x = x

id ω Id id ~> id

这是不可预测的(虽然我不知道这种特殊形式的非预测性是否会导致不一致。是吗？)。

因此，我们不能将ω作为合法级别添加到目标语言中，也不能在存在“宇宙依赖”函数的情况下在Set α上进行模式匹配。因此，“自反”平等

EqEmb : ⟦ (nat ‵πᵤ‵ λ α → nat ‵πᵤ‵ λ β → univ α ⇒ univ β ⇒ prop) ⟧

不是为所有宇宙多态函数(不是“宇宙依赖的”)定义的。例如，map的类型

map : ∀ {α β} {A : Set α} {B : Set β} -> (A -> B) -> List A -> List B

是Setω，我们不能问Eq (typeOf emb-map) (typeOf emb-map)是否是，因为在Eq A B中，A的类型是⟦ univ α ⟧，这是一个“有限”的宇宙(B也是如此)。

那么，是否有可能以一种类型良好的方式嵌入OTT本身呢？如果没有，我们能以某种方式欺骗吗？我们能不能在Set α上匹配“宇宙依赖的”函数，就像一切正常一样？

Answer 1

最后我得到了以下层次结构：

Prop : Type 0 : Type 1 : ...
(∀ α -> Type α) : Type ω₀ : Type ω₁

没有Type ω₁的代码，因为以前没有Type ω₀的代码，但是我们需要一个Type ω₀的代码来定义宇宙多态函数的相等，而Type ω₁的代码就不那么有用了。

现在我们有四个宇宙相关的量词

σ₀ π₀   : {α : Lev false}
        -> (A : Univ α) {k : ⟦ A ⟧ -> Lev false} -> (∀ x -> Univ (k x)) -> Univ {false} ω₀
σ₁ π₁   : ∀ {a} {α : Lev a}
        -> (A : Univ α) {b : ⟦ A ⟧ -> Bool} {k : ∀ x -> Lev (b x)}
        -> (∀ x -> Univ (k x))
        -> Univ ω₁

关键是，现在可以在π₀上进行模式匹配，从而允许定义宇宙多态函数的相等，但是在π₁上进行模式匹配是不可能的(就像π₀ (称为πᵤ)一样)，我们可以接受这一点。

平等有以下这些“自反”类型：

mutual
  Eq : ⟦ (π₁ lev λ α -> π₁ lev λ β -> univ⁺ α ⇒ univ⁺ β ⇒ prop) ⟧
  eq : ⟦ (π₁ lev λ α -> π₁ lev λ β -> π (univ⁺ α) λ A -> π (univ⁺ β) λ B -> A ⇒ B ⇒ prop) ⟧

代码是这里。然而，看起来我需要再一次扩展层次结构，以证明一致性。我会问你一个问题。