From objects to families of objects

Stream: new members

[Mathias Stout]

My question is essentially the following: given existing theorems for a certain Type α, is there a standard/best procedure to work with and derive properties of objects of type β → α and their corresponding fiberwise morphisms?

Context: I am setting up some basics for multisorted first order logic, based on the existing libraries for the one-sorted case and suggestions in the work of Sky Wilshaw.
In the one-sorted setting a Structure is some built on some object M : Type u. A natural multisorted analogue is M : Sorts \to Type u (where Sorts are the sorts of some multisorted language and unrelated to Lean's Sort). Similarly for sets of variable names, morphisms between structures, ...

Many basic theorems and definitions are easy to transfer and a good exercise to familiarize oneself with the model theory library. However, I was wondering if there is a general principled way to go about this. E.g. any existing modules on "fiberwise" maps that I should be aware of?