Indexed QPF

Stream: Type theory

[Palalansoukî]

QPF.Fix provides a fixed point of functor F. Can we extend this to obtain (potentially infinite) fixed points, indexed by some type? That is, by assuming appropriate conditions for F, can we properly define a constructor and destructor as follows?

variable {ι : Type u} {F : (ι → Type v) → (ι → Type v)} [IndexedQPF F]

def Fix (F : (ι → Type v) → (ι → Type v)) : ι → Type v := sorry

def Fix.mk : (i : ι) → F (Fix F) i → Fix F i := sorry

def Fix.dest : (i : ι) → Fix F i → F (Fix F) i := sorry