How to formalize dependent setoid morphisms?

In fact, how to constructive mathematics a la Bishop.
I haven't got to the bottom of it, it turns out to be
a long term project in itself, for both theoretical and
technical reasons, but here are few notes and mainly the
references that I have managed to collect.
"How to formalize dependent setoid morphisms?"
<https://discourse.rocq-prover.org/t/2759>
To be continued...
-Julio