[Agda] induction recursion - normalisation

[Ondrej Rypacek]

Hi,
I have a fairly simple inductive-recursive definition (see below).
The hole roughly in the middle, 4th case of the def. of src, has type

?0 : src fzero z ≡ tgt fzero (comp fzero x y xy)

where the right-hand side normalises to tgt fzero y by the definition
of tgt so the normalised environment is

Goal: src fzero z ≡ tgt fzero y
————————————————————————————————————————————————————————————
xy : src fzero y ≡ tgt fzero x
yz : src fzero z ≡ tgt fzero y
z  : Freeω (suc .n)
y  : Freeω (suc .n)
x  : Freeω (suc .n)
.n : ℕ
G  : GlobularSet

But yz fits only until I recompile. Then I'm getting

"y != (comp fzero x y xy) of type (Freeω (suc .n))
when checking that the expression yz has type
src fzero z ≡ tgt fzero (comp fzero x y xy)"

Strangely, the symmetrical case below, in the definition of tgt, i.e.

tgt fzero (alpha x y z yz xy) = comp fzero x (comp fzero y z yz) xy

works fine. Why? What's the difference ?
Any ideas what's wrong and how to fix it ?


Cheers,
Ondrej

-------

{-# OPTIONS --no-termination-check #-}

module globSetCat where

open import Data.Nat
open import Data.Fin hiding (#_;_<_) renaming (suc to fsuc;zero to fzero)
open import Data.Product
open import Data.Empty
open import Data.Unit hiding (tt ; _≤_ )
open import Relation.Binary.PropositionalEquality


-- a category structure on a set
record GlobularSet : Set₁ where
  field
    #_ : ℕ → Set
    src : ∀ {n} → # (suc n) → # n
    tgt : ∀ {n} → # (suc n) → # n

    ss-st : ∀ {n x} → src {suc (suc n)} (src x) ≡ src (tgt x)
    ts-tt : ∀ {n x} → tgt {suc (suc n)} (src x) ≡ tgt (tgt x)


module Freeω (G : GlobularSet) where
  open GlobularSet G renaming (src to |src|;tgt to |tgt|)

  mutual
    data Freeω : ℕ → Set where
      emb : ∀ {n} → # n → Freeω n
      comp : ∀ {n} → (m : Fin (suc n)) → (α β : Freeω (suc n)) → src m
β ≡ tgt m α → Freeω (suc n)
      id : ∀ {n} → Freeω n → Freeω (suc n)
      alpha : ∀ {n} → (x y z : Freeω (suc n)) → src fzero z ≡ tgt
fzero y → src fzero y ≡ tgt fzero x → Freeω (suc (suc n))

    src : ∀ {n} → (m : Fin (suc n)) → Freeω (suc n) → Freeω (n ℕ-ℕ m)
    src fzero (emb y) = emb (|src| y)
    src fzero (comp _ f g _) = src fzero f
    src fzero (id y) = y
    src fzero (alpha x y z yz xy) = comp fzero (comp fzero x y xy) z {!!}
    src {zero} (fsuc ()) x
    src {suc n} (fsuc i) x = src i (src fzero x)

    tgt : ∀ {n} → (m : Fin (suc n)) → Freeω (suc n) → Freeω (n ℕ-ℕ m)
    tgt fzero (emb y) = emb (|tgt| y)
    tgt fzero (comp _ f g _) = tgt fzero g
    tgt fzero (id y) = y
    tgt fzero (alpha x y z yz xy) = comp fzero x (comp fzero y z yz) xy
    tgt {zero} (fsuc ()) x
    tgt {suc n} (fsuc i) x = tgt i (tgt fzero x)