在Coq或Agda中键入层次结构定义

Question

我想构建一种类型层次结构:

B is of type A  ( B::A )

C and D are of type of B   (C,D ::B) 

E and F are of type of C     (E,F ::C)

我在这里询问是否可以直接在Isabelle中实现,但是你看到的答案是否可以直接在Agda或Coq中编码？

PS:假设A..F都是抽象的,并且在每种类型上定义了一些函数)

谢谢

Answer 1

如果我正确理解你的问题,你想要的东西看起来像身份类型.当我们声明类型构造函数时_isOfType_,我们提到两个Sets(参数A和索引B),但构造函数indeed确保构造这种类型的元素的唯一方法是强制它们确实相等(并且这a是这种类型) ):

data _isOfType_ {?} {A : Set ?} (a : A) : (B : Set ?) ? Set where
  indeed : a isOfType A

我们现在可以将函数作为参数证明事物是正确的类型.在这里,我翻译了您的要求,并假设我有一个f能够将两个Cs 组合成一个的功能.在适当的假设上进行模式匹配表明E和F确实在类型上C,因此可以用它f来实现目标:

example : ? (A : Set?) (B : Set?) (C D : Set?) (E F : Set) ?
    B isOfType A
  ? C isOfType B ? D isOfType B
  ? E isOfType C ? F isOfType C
  ? (f : C ? C ? C) ? C
example A B .Set D E F _ _ _ indeed indeed f = f E F

对于这种模式,您是否考虑过特定​​的用例,或者您是否正在使用其他编程语言遇到的想法来访问Agda？可能有更惯用的方式来制定您的问题.