Chain of functions and their sequential application

Stream: Is there code for X?

[nrs]

I encountered the following structure and thought that it's probably already defined somewhere:

structure seqFunc where
  finIndex : Nat
  func : Fin finIndex -> (t t' : Type) ×' (t -> t')
  isSeq : (n : Nat) -> (p : n.succ < finIndex) -> (func ⟨n, by linarith⟩).2.1 = (func ⟨n.succ, by linarith⟩).1

So e.g. given (fstruct : seqFunc), (fstruct.func 0).2.2 : A -> B, (fstruct.func 1).2.2 : B -> C, (fstrict.func 2).2.2 : C -> D, and so on. I'm trying to define the function for folding fstruct.func, and I was wondering if maybe some of the work was done somewhere

[nrs]

here is a small API for application-remembering folds with an analogous type to seqFunc in case someone else looks up the topic

set_option autoImplicit true

inductive FuncChain (α : Type) : Type -> Type 1
| intro {β : Type} : (α -> β) -> FuncChain α β
| extend : FuncChain α β -> (β -> γ) -> FuncChain α γ

inductive FuncChainOn {α : Type} (a : α) : (β : Type) -> (b : β) -> Type 1
| intro {β : Type} : (f : α -> β) -> (s : Σ' b, b = f a) -> FuncChainOn a β s.1
| extend : FuncChainOn a β b -> (g : β -> γ) -> (s : Σ' c, c = g b) -> FuncChainOn a γ s.1

def FuncChain.toFunc : FuncChain α β -> α -> β
| .intro f => f
| .extend fs g => g ∘ (toFunc fs)

def FuncChainOn.ofFuncChain (fs : FuncChain α τ) : (a : α) -> (v : τ) × FuncChainOn a τ v :=
  fun a => match fs with
  | .intro f => ⟨f a, .intro f ⟨f a, rfl⟩⟩
  | .extend fs' g =>
    let prev := ofFuncChain fs' a
    ⟨g prev.fst, .extend prev.2 g ⟨g prev.fst, rfl⟩⟩

def FuncChainOn.onList (fs : FuncChain α τ) (l : List α) : List <| (a : α) × (v : τ) × FuncChainOn a τ v :=
  List.map (fun a => ⟨a, ofFuncChain fs a⟩) l