Do dependent product functors always reflect terminal objects? Let $X$ be an object of a cartesian closed category $C$ with pullbacks (and hence finite limits).

Does the dependent product functor $\Pi_X:C/X \to C$ always reflect terminal objects? In other words, if $f$ is a morphism with codomain $X$ for which the "object of sections" of $f$ is terminal, must $f$ be an isomorphism?

It is easy to see that $f$ must at least be a split epimorphism with a unique section. Also, the above question is a generalization of the fact that the cartesian product of a family of sets is a singleton only when all of the sets in the family are themselves singletons.

$
\newcommand{\base}{\mathsf{base}}
\newcommand{\loop}{\mathsf{loop}}
\newcommand{\transport}{\mathsf{transport}}
\newcommand{\0}{\mathsf{[0]}}
\newcommand{\1}{\mathsf{[1]}}
\newcommand{\2}{\mathsf{[2]}}
\newcommand{\3}{\mathsf{[3]}}
\newcommand{\Switch}{\mathsf{Switch}}
\newcommand{\fst}{\mathsf{fst}}
$
Okay, after conferring with someone who knows the homotopy angle better than I do, and some fiddling around, I've constructed this Agda development which shows how dependent products may not reflect the terminal type.
The idea is to construct a family over the type $S^1$, which is the homotopy type of the circle with base point $\base : S^1$ and path $\loop : \base \equiv \base$. A family over this type can be given by a type $T$ and a path $P : T \equiv T$.
The key idea is that the type of sections $\prod_{c:S^1} F\ c$ is equivalent to $\sum_{t : T} \transport\ P \ t \equiv t$ (presuming that the family $F$ is equivalent to $(T, P)$ as above). That is, a section of $F$ is an element of $T$ that is fixed by $P$.
So, we can define a set $\3$ with three values, and define a path $\Switch :\3 \equiv \3$ that rotates two of the elements but leaves one fixed. This makes for a family whose sections are contractible (equivalent to the terminal object), but there are fibers of the family that are not contractible.
I'm not an expert on the categorical semantics of this stuff. The slice category presentation of this family is $\fst : (\sum_{c:S^1} F\ c) \to S^1$. The "non-boolean presheaf (pre)topos" in question is, I think, that of cubical sets (pretopos becauase Agda is predicative, and doesn't have a subobject classifier). $\fst$ is not injective because it sends $(\base, \0)$, $(\base, \1)$ and $(\base, \2)$ all to $\base$. But every section must send $\base$ to $(\base, \0)$ for the reasons discussed above.
