A morphism in a category has a domain and codomain: $f:A\to B$
In dependent type theory, we can have functions with a "dependent type", meaning that the codomain depends on the input. This can be written as: $f:(a:A)\to B_a$, where $B_a$ is a type (or set ...) that is parameterized by elements of $A$.
Can we formalize such "dependently typed morphisms" in the context of category theory? Is this a done?