Forcing $\pi_1(\tilde f(a))=f(a)$ for an object of a sigma type

Question

Suppose I have an object $f$ of type $\Pi x:A.B(x)$, and consider a new type $\Pi (x:A).\Sigma (t:B(x)).C(t)$. If $\tilde f$ is an object of the second type and $a:A$, then $\pi_1(\tilde f (a)):B(x)$, where $\pi_1(x,y)=x$. Is there a way to force that $\pi_1(\tilde f(a))=f(a)$?

A few words on where this question is coming from: suppose we want to model sentences like "John walked" and "John walked (for some time) and then stopped". Say $walk$ has type $\Pi x:AnimateEntity.Evt(x)$, so $walk(john)$ has type $Evt(john)$, the type of events with participant "John". Now consider another version of the verb "walk", one in which it is encoded that the action of walking took place and then stopped (in some languages there is such a word form). Let's call this version $walk'$. Then it would be natural to assume that $walk'(john):\Sigma (x:Evt(j)).Stop(x)$, where $\pi_1(walk'(john)) = walk(john)$ -- which says that there was the original walking event (which we denoted $walk$ without a prime) and $\pi_2(walk'(john))$ is a proof that that original walking event stopped. So if I want $walk'(john)$ to have that type, I should make $walk'$ have type $\Pi (x:AnimateEntity).\Sigma(t:Evt(x)).Stop(t)$. But now I'm not sure how to force $\pi_1(walk'(john)) = walk(john)$, and hence the original question.

Answer 1

Before I answer (the purely mathematical part of) your question, we have to get around a minor, but confusing, notational ambiguity.

It's not entirely clear what role you intend $C$ to play. Is it some bona fide function of type $C: \Pi x:A.B(x) \rightarrow \mathrm{Type}$? If so, why do you elide the $x$ and not denote its value at least $C(x)(t)$? If not, does it just abbreviate whatever expression, with free variable $t$, comes after the $\Sigma$ binder? Then why not just denote it $C$ instead of $C(t)$? I'm going to assume $C$ is the former.

1. In general, when $A: \mathrm{Type}$, $B: A \rightarrow \mathrm{Type}$, $f: \Pi x:A.B(x)$ and $C: \Pi x:A.B(x) \rightarrow \mathrm{Type}$ are arbitrary, there is no way to force this. Consider e.g. the situation where $C(x)(t)$ stands for $f(x) \neq t$.

2. When $A: \mathrm{Type}$, $B: A \rightarrow \mathrm{Type}$, $f: \Pi x:A.B(x)$, but you have full control over $C$, you can achieve what you want trivially: just make sure that $C(x)(t)$ has the form $(t = f(x)) \times C'(x)(t)$ for some $C': \Pi x:A. B(x) \rightarrow \mathrm{Type}$.

3. Inbetween the two extreme scenarios above, when you know some things about $C$, but don't have full control over it, you might be able to ensure this, depending on the properties of $C$. Unfortunately, I cannot answer your question in the context of Corfield-style HoTT linguistics, concerning $\mathrm{Stop}$ in particular; and I'll be surprised if anyone apart from perhaps David Corfield can.