In my example $f$ is a principal bundle because it becomes trivial (an isomorphism) after pulling back along a cover, namely $f$ itself.

Are you interested in "real" examples, or contrived ones? e.g. if $f : A \to B$ is any noninvertible mono that we declare to be a singleton covering family, then $f$ is also a map of principal bundles on $B$ for the trivial group that does not have an inverse. (But after sheafififcation, it will have an inverse.)

It's not exactly what you asked for for several reasons, but the HoTT book does start from basic type theory, and constructs a universe of ZF-style sets in section 10.5.

What about $C = \partial \Delta^1$, $D = \Delta^1$, $p$ the inclusion. Do I understand your question right?

What I meant is that, for fixed X, your equation holds for all Y if and only if the counit |Sing X| -> X is a homeomorphism. And both |Sing X| and (by assumption) X are "nice" spaces, so if (as usual) they are different, we should be able to see the difference using maps into another "nice" space Y.