[Agda] Re: elements of recursive records

[Nils Anders Danielsson]

On 2011-03-28 16:59, Thorsten Altenkirch wrote:
> 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?

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

reflω : ∀ {A} (a : A) → El (♭ (hom (Idω A) a a))
reflω a = ♭ (reflω′ a)

-- 
/NAD