在Agda中构建一个依赖类型系统

Question

如何在Agda中制定一个依赖类型的逻辑，而不是通过重新使用Agda类型系统来“欺骗”？

我可以很容易地定义一个独立类型的逻辑：

infixr 5 _⇒_
data Type : Set where
    _⇒_ : Type → Type → Type

infix 4 _⊢_
data _⊢_ : List Type → Type → Set where
    var : {a : Type} → [ a ] ⊢ a
    λ'  : {a b : Type} {γ : _} → a ∷ γ ⊢ b → γ ⊢ a ⇒ b
    ply : {a b : Type} {γ δ : _} → γ ⊢ a ⇒ b → δ ⊢ a → γ ++ δ ⊢ b
    weak : {a b : Type} {γ : _} → γ ⊢ b → a ∷ γ ⊢ b
    cntr : {a b : Type} {γ : _} → a ∷ a ∷ γ ⊢ b → a ∷ γ ⊢ b
    xchg : {a : Type} {γ δ : _} → γ ↭ δ → γ ⊢ a → δ ⊢ a

我也可以粗略地遵循Haskell中依赖类型的λ演算的LambdaPi教程实现。但它与我的Agda代码不同，它是隐含式的，我不知道在哪里开始修改我的代码，因为到目前为止我想到的路径导致了无限的回归：

data _⊢_ : List (? ⊢ ?) → (? ⊢ ?) → Set where ...

谷歌搜索“在Agda中嵌入依赖类型”等仅仅返回Agda中依赖类型编程的命中...

Answer 1

我们在关于类型理论中的类型理论的论文中做到了这一点，该论文实际上是在Agda中形式化的。基本思想是将上下文，类型，术语和替换定义为互感定义。我们只定义类型化对象，因此我们永远不必定义无类型的东西或打字判断。键入是通过依赖来定义的，例如类型取决于类型和上下文的上下文和术语。为了形成定义平等，我们使用来自同伦类型理论的思想并允许等式构造函数。这意味着我们必须对更高电感类型的实例进行公理化，或者是精确的归一归电感应类型。这应该很快就可以在立方体Agda中开箱即用。

http://www.cs.nott.ac.uk/~psztxa/publ/tt-in-tt.pdf

@article{altenkirch2016type,
  title={Type theory in type theory using quotient inductive types},
  author={Altenkirch, Thorsten and Kaposi, Ambrus},
  journal={ACM SIGPLAN Notices},
  volume={51},
  number={1},
  pages={18--29},
  year={2016},
  publisher={ACM}
}