Computable fixpoint functors

Stream: lean4

[ohhaimark]

I would like to write an inductive type

inductive Tm (tm: Nat -> Type) : Nat -> Type  := ...

with functor instance (Assuming Nat is a discrete category).

Since I can't write a terminating instance for fixpoints generally, could you specialize it to just initial algebras. Would it be computable assuming the functor is computable? If not, what conditions do I need for it to be computable?