Can I use inductive type families in Cubical Agda?

Question

I noticed that the Cubical standard library defines Fin as a dependent pair instead of an indexed inductive type. The reason why is that Cubical Agda does not fully support indexed inductive types: https://github.com/agda/cubical/pull/104#discussion_r268476220

A linked issue states that pattern matching doesn't work on inductive families because hcomp and transp haven't been defined on them: https://github.com/agda/cubical/pull/57#issuecomment-461174095

I defined Fin and Vec and wrote a pattern-matching function, and it seems to work fine:

{-# 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

Yet this issue is still open: https://github.com/agda/agda/issues/3733

I want to use Cubical Agda just in case I need higher inductive types or function extensionality, but I don't want to give up Vec or the indexed definition of Fin. I am unfamiliar with the details of Cubical Type Theory, so I don't know where hcomp and transp would be invoked. What is the current status of inductive families in Cubical Agda? Can I still use them if I avoid certain operations?

Saizan Saizan · Accepted Answer · 2020-01-29T09:03:10

It is fine to use inductive families with cubical agda, and pattern matching definitions work in the sense that they do compute for the declared constructors of the family.

The limitation that will be addressed by https://github.com/agda/agda/issues/3733 is the following:

A term like subst Fin refl fzero will not compute to fzero or any other constructor, which also means that

(x ∷ _) [ subst Fin refl fzero ]

will not compute to x either.

We can still prove subst Fin refl fzero ≡ fzero by substRefl from the library, so we can also prove (x ∷ _) [ subst Fin refl fzero ] ≡ x.

So currently it is a choice between using inductive families and dealing with subst and transport getting stuck on them, or otherwise encoding everything with paths and lose the nice pattern matching.

Can I use inductive type families in Cubical Agda?

1 Answers