agda - OTT 中的 self 表示和宇宙

Question

问题是关于Observational Type Theory的.

考虑这个设置:

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 是非谓语)，Σ- 和 Π 的代码-types 和一个附加代码 πᵤ 用于“宇宙多态 π-types”。就像在 Agda 中 ∀ α -> Set α 具有 [the hidden] 类型 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 ω₀的代码来能够定义全域多态函数的相等性，类型 ω₁ 的代码用处不大。

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

σ₀ π₀   : {α : 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) ⟧

密码是here .然而，看起来我需要再次扩展层次结构才能证明一致性。我会问一个问题。