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 是非谓语），Σ- 和 Π-类型的代码和一个附加代码 πᵤ "universe polymorphic Π-types"。就像在 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 是 "universe dependent" 并且具有，比方说，这种类型：∀ α -> Set α 怎么办？那么 Π A B 的类型是 Setω 并且 α 与 ω 统一。但是如果我们可以用 ω 实例化级别变量，那么我们可以写成

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

id : Id
id α A x = x

id ω Id id ~> id

这是非谓语（尽管我不知道这种特殊形式的非谓语是否会导致不一致。是吗？）。

因此我们无法将 ω 作为目标语言的合法级别添加，并且我们无法在存在 "universe dependent" 函数的情况下对 Set α 进行模式匹配。因此 "reflexive" 相等

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

没有为所有 Universe 多态函数定义（不是 "universe dependent"）。例如。 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 α ⟧，这是一个"finite"宇宙（B也是如此）。

那么是否可以将OTT以一种良好类型的方式嵌入到自身中呢？如果没有，我们能以某种方式作弊吗？我们可以在 "universe dependent" 函数的情况下对 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 ω₁

关键是现在可以在 π₀ 上进行模式匹配，从而允许定义全域多态函数的相等性，但不可能在 π₁ 上进行模式匹配（与 π₀ 被称为 πᵤ)，我们可以接受它。

等式有这些"reflexive"类型：

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

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

OTT 中的自我表示和宇宙

Self-representation and universes in OTT

agda

dependent-type

type-theory

observational-type-theory