具有不同类型索引的互感描述？

Question

我正在使用描述，就像它们被描述的那样 here，作为对归纳数据类型的形状进行编码的一种方式。但是，我坚持如何表示归纳类型：

互感
有不同的指数

例如，假设我们有这样的东西，我们要订购不同的类型：

data Foo : Set where
  N : ℕ -> Foo 
  P : (Foo × Foo) -> Foo

data <N : ℕ -> ℕ -> Set where
  <0 : (n : ℕ) -> <N zero n
  <suc : (m n : ℕ) -> <N m n -> <N (suc m) (suc n)

data <P : (Foo × Foo) -> (Foo × Foo) -> Set 
data <F : Foo -> Foo -> Set 

data <P where
  <Pair : (x1 x2 y1 y2 : Foo) -> <F x1 y1 -> <F x2 y2 -> <P (x1 , x2) (y1 , y2)

data <F where
  <FN : ∀ (a b : ℕ) -> <N a b -> <F (N a) (N b)
  <FP : ∀ (p1 p2 : (Foo × Foo) ) -> <P p1 p2 -> <F (P p1) (P p2)

也就是说，我们得到了一种在叶子上有 nats 的二叉树。我们在树之间有一个偏序，我们以通常的方式比较 nats，我们通过比较它们各自的子树来比较节点对。

注意 <F 和 <P 是如何相互依赖的。当然，我们可以内联它以使 <F 和 <P 成为一种类型，我试图避免这种情况，对于 <P 的情况更复杂。

我想知道的是：上面的部分订单类型可以用Descriptions来表达吗？

我什至试图将上述类型描述为索引函子的定点时也卡住了。通常我们有一个索引类型 (I : Set) 而仿函数的类型为 (X : I -> Set) -> I -> Set。但是我们不能同时让 "Foo" 和 "Foo × Foo" 成为我们的 I 值。有没有什么技巧可以让我们使用 I = Foo ⊎ (Foo × Foo)?

Answer 1

对所有指数求和：

Ix = ((Foo × Foo) × (Foo × Foo)) ⊎ (Foo × Foo)

data <P : Ix -> Set
data <F : Ix -> Set

data <P where
  <Pair : (x1 x2 y1 y2 : Foo) -> <F (inj₂(x1 , y1)) -> <F (inj₂(x2 , y2))
                              -> <P (inj₁((x1 , x2), (y1 , y2)))

data <F where
  <FN : ∀ (a b : ℕ) -> <N a b -> <F (inj₂(N a , N b))
  <FP : ∀ (p1 p2 : (Foo × Foo) ) -> <P (inj₁(p1 , p2)) -> <F (inj₂(P p1 , P p2))

我们可以稍微整理一下索引，并以索引函子更容易描述的形式编写内容：

data Ix : Set where
  <P : Foo × Foo → Foo × Foo → Ix
  <F : Foo → Foo → Ix

data T : Ix → Set where
  <Pair : ∀ x1 x2 y1 y2  → T (<F x1 y1) → T (<F x2 y2)
                         → T (<P (x1 , x2) (y1 , y2))
  <FN : ∀ (a b : ℕ) → <N a b → T (<F (N a) (N b))
  <FP : ∀ p1 p2 → T (<P p1 p2) → T (<F (P p1) (P p2))

我注意到 <P 和 <F 可以递归定义，所以归纳在这里不是必需的。

<F : Foo → Foo → Set
<F (N n) (N n')              = <N n n'
<F (P (x , y)) (P (x' , y')) = <F x x' × <F y y'
<F (N _) (P _) = ⊥
<F (P _) (N _) = ⊥

具有不同类型索引的互感描述？

Mutually Inductive Descriptions with different type indices?

type-theory

functional-programming

theorem-proving

agda

dependent-type