I am using the usual coinductive definition of the M-type, defined below.
record M (S : Set) (Q : S → Set) : Set where
coinductive
constructor sup-M
field
shape : S
pos : Q shape → M S Q
open M
I define a family Pos over M, which has specified target types (namely the target types use sup-M and aren't generic for any m : M).
data Pos : M S Q → Set where
here : {s : S} {f : Q s → M S Q} → Pos (sup-M s f)
below : {s : S} {f : Q s → M S Q} → (q : Q s) → Pos (f q) → Pos (sup-M s f)
Say that for fixed S : Set, Q : S → Set, X Y : Set, s : S, h : Q s → Y, g : Y → X, I define the function below going into M.
β₁ : Y → M S Q
shape (β₁ y) = s
pos (β₁ y) = β₁ ∘ h
Then if I want to define a function β₂ : (y : Y) → Pos (β₁ y) → X, I'm not able to pattern-match on the second argument because it's not of the form Pos (sup-M s f). I can get around this in a few ways, one of which is by noting that in Cubical Agda we have (propositional) eta-equality for M:
M-eta-eq : {S : Set} {Q : S → Set} (m : M S Q) → sup-M (shape m) (pos m) ≡ m
shape (M-eta-eq m i) = shape m
pos (M-eta-eq m i) = pos m
So I can define a helper function β₂' : (y : Y) → Pos (sup-M s (β₁ ∘ h)) → X which allows pattern matching, and then define β₂ in terms of β₂' using the fact that M-eta-eq (β₁ y) : sup-M s (β₁ ∘ h) ≡ β₁ y.
β₂' : (y : Y) → Pos (sup-M s (β₁ ∘ h)) → X
β₂' y here = g y
β₂' y (below q p) = β₂' (h q) (subst Pos (sym (M-eta-eq (β₁ (h q)))) p)
β₂ : (y : Y) → Pos (β₁ y) → X
β₂ y p = β₂' y (subst Pos (sym (M-eta-eq (β₁ y))) p)
The problem with this is that it raises a non-terminating error, presumably because Agda can't tell that subst Pos (sym (M-eta-eq (β₁ (h q)))) p is structurally smaller than below q p. So my question is:
Can I prove to Agda that
β₂'terminates? Perhaps something making use ofsubst-filler?
P.S. I have tried other approaches, like defining β₂ using the eliminator of Pos, or adding an equality of the form m ≡ sup-M s f to the constructors of Pos, and then having the target types be of type Pos m. While I was able to define β₂ successfully in both cases, both approaches introduced many substs and transports to proofs of equality involving β₂ that I have to do later on. I am wondering if there is a better way to define Pos, especially since I know inductive families are still not fully supported in Cubical Agda.
Many thanks for any help!
You should generally try to avoid green slime both in function arguments and in constructor return types: indices that yield difficult unification problems (in this case, M doesn't have definitional eta equality, so even sup-M is difficult).
Things go smoothly if you use variables instead:
data Pos : M S Q → Set where
here : {m : M S Q} → Pos m
below : {m : M S Q} → (q : Q (shape m)) → Pos (pos m q) → Pos m
β₁ : M S Q
shape β₁ = s
pos β₁ _ = β₁
β₂ : (y : Y) → Pos β₁ → X
β₂ y here = g y
β₂ y (below q p) = β₂ (h q) p
_ : {y : Y} → β₂ y here ≡ g y
_ = refl