Selbstverständlich die Standardkonstruktion in Haskell

newtype Fix f = Fix { getFix :: f (Fix f) }

cata :: (Functor f) => (f a -> a) -> Fix f -> a
cata f = f . fmap (cata f) . getFix 

ist fantastisch und äußerst nützlich.

Versuch, eine ähnliche Sache in Agda zu definieren (ich werde es der Vollständigkeit halber sagen)

data Fix (f : Set -> Set) : Set where
    mkFix : f (Fix f) -> Fix f

scheitert daranf ist nicht unbedingt streng positiv. Das macht Sinn - ich könnte leicht einen Widerspruch aus dieser Konstruktion ziehen, wenn ich sie richtig auswähle.

Meine Frage ist: Gibt es irgendeine Hoffnung, Rekursionsschemata in Agda zu kodieren? Wurde es getan? Was wäre erforderlich?