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?
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With