[Agda] elements of recursive records

[Thorsten Altenkirch]

Hi,

I am trying to define an element of a recursive record but seem to run in trouble with the fact that # is generative. Do you know a good workaround?

I define globular sets:

record Glob : Set₁ where
  field
    obj : Set₀
    hom : obj → obj → ∞ Glob
open Glob

and elements of globular sets:

record El (G : Glob) : Set where
  field
    obj→ : obj G
    hom→ : ∞ (El (♭ (hom G obj→ obj→)))

Now the iterated identity type is an example:

Idω : Set → Glob
Idω A = record { obj = A; hom = λ a b → ♯ Idω (a ≡ b) } 

And iterated reflexivity should be an an element

reflω : ∀ {A} (a : A) → El (♭ (hom (Idω A) a a))
reflω a = record { obj→ = refl; hom→ = ♯ reflω refl  } 

but Agda doesn't like this - i suspect it has to do with # appearing in a type. But I don't see how to avoid this - do you?

Cheers,
Thorsten