我可以在 Cubical Agda 中使用归纳类型系列吗？

Question

我注意到 Cubical 标准库定义Fin为依赖对而不是索引归纳类型。原因是 Cubical Agda 不完全支持索引归纳类型：https : //github.com/agda/cubical/pull/104#discussion_r268476220

一个链接问题指出模式匹配不适用于归纳家庭，因为hcomp并且transp尚未对其进行定义：https : //github.com/agda/cubical/pull/57#issuecomment-461174095

我定义Fin并Vec编写了一个模式匹配函数，它似乎工作正常：

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat using (?; zero; suc)

private
  variable
    ? : Level
    A : Type ?
    n : ?

data Fin : ? ? Type? where
  fzero : Fin (suc n)
  fsuc : Fin n ? Fin (suc n)

data Vec (A : Type ?) : ? ? Type ? where
  [] : Vec A zero
  _?_ : A ? Vec A n ? Vec A (suc n)

_[_] : Vec A n ? Fin n ? A
(x ? _) [ fzero ] = x
(_ ? xs) [ fsuc n ] = xs [ n ]

p : (1 ? (2 ? [])) [ fzero ] ? 1
p = refl

然而这个问题仍然存在：https : //github.com/agda/agda/issues/3733

我想使用 Cubical Agda 以防万一我需要更高的归纳类型或函数扩展性，但我不想放弃Vec或Fin. 我不熟悉立方类型理论的细节，所以我不知道在哪里hcomp和transp会被调用。Cubical Agda 中归纳家庭的现状如何？如果我避免某些操作，我还可以使用它们吗？

Answer 1

将归纳族与立方 agda 一起使用是很好的，模式匹配定义的工作原理是它们确实为族的声明构造函数进行计算。

https://github.com/agda/agda/issues/3733将解决的限制如下：

像这样的术语subst Fin refl fzero不会计算fzero或任何其他构造函数，这也意味着

(x ? _) [ subst Fin refl fzero ]

也不会计算x。

我们仍然可以证明subst Fin refl fzero ? fzero通过substRefl从库中，所以我们也可以证明(x ? _) [ subst Fin refl fzero ] ? x。

因此，目前可以选择使用归纳族并处理它们subst并transport陷入困境，或者以其他方式使用路径对所有内容进行编码并失去良好的模式匹配。