在Agda中键入Hierarchy

Question

我试图找出类型层次结构如何在Agda中工作.

假设我定义了一个集合类型X:

X : Set 

然后继续构建归纳型

data Y : X -> Set where

是什么类型的X -> Set？是设置还是类型？

谢谢!

Answer 1

好吧,为什么不问阿格达呢？我将为Emacs使用出色的Agda模式.我们从:

module Hierarchy where

postulate
  X : Set

data Y : X ? Set where
  -- empty

我们必须使用加载文件C-c C-l; 这样可以检查文件,将?s转换为空洞,进行语法高亮等操作.

现在,有一个命令"推断(演绎)类型"可用C-c C-d,所以让我们使用:

> C-c C-d
Expression:
> Y
X ? Set

对,这是有道理的.我们定义了Y : X ? Set,所以它应该不足为奇.我们再问一遍:

> C-c C-d
Expression:
> X ? Set
Set?

所以,你有它:Y : X ? Set : Set?.

虽然第一部分回答了问题,并向您展示了如何自己检查这些东西,但每次这样做都会变得乏味,至少.以下是它的工作原理:

为避免悖论,我们要求

Set i : Set (i + 1)

它给你Sets 的(无限)层次结构.如果你有Set : Set(其中阿格达通过允许--type-in-type标志),可以推导出矛盾,比如这一个.

这也为我们提供了一个简单的函数规则:

A : Set i
B : A ? Set j

(a : A) ? B a : Set (max i j)

将此应用于您的示例:

X   : Set
Set : Set?

X ? Set : Set (max 0 1)
X ? Set : Set?