Escusado será dizer que a construção padrão em 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 

é incrível e extremamente útil.

Tentando definir uma coisa semelhante em Agda (vou colocá-lo apenas por causa da integralidade)

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

falha porquef não é necessariamente estritamente positivo. Isso faz sentido - eu poderia facilmente obter uma contradição a partir desta construção escolhendo apropriadamente.

Minha pergunta é: existe alguma esperança de codificar esquemas de recursão em Agda? Já foi feito? O que seria necessário?