Just to make sure I understand the notation in the excerpt below (from Corfield's "Modal Homotopy Type Theory") correctly, is the "sum" over $x:Activity, y:Achievement$" the same as
$$ \Sigma_{x:Activity} [\Sigma_{y: Achievement}.Culminate(x,y)], $$
i.e., an object of type $Accomplishment$ has the form $(a,(b,c))$ where $a:Activity, b:Achievement, c:Culminate(a,b)$?
And then if $w:Accomplishment$, say $w=(a,(b,c))$, then $q(w)= (b,c)$?
If that's right, I'm also confused about the type of $q(w)$. It should be something like $\Sigma_{y:Achievement}Culminate(x,y)$, but can a type contain a free variable (like $x$ in this case)?
Consider a sigma type $\displaystyle \sum_{x:T} \varphi(x)$ and its inhabitant $\displaystyle w : \sum_{x:T} \varphi(x)$. We will denote the left projection by $p(w)$ and the right projection by $q(w)$. Then, we can make the following judgments:
Notice that the bound variable $x$ does not occur free in the type of $q(w)$; instead, we substituted it with $p(w)$. This allows $q(w)$ to appear in the exact same typing context as $w$ itself.
Indeed, in this case we could give the "eliminator" $q$ the function type (dependent product type) $$q:\prod_{w:(\Sigma_{x:T} \varphi(x))} \varphi(p(w))$$
Everything works the same way when we deal with an iterated sum type. If we have
$$w: \sum_{x:\mathrm{Activity}} \sum_{y:\mathrm{Achievement}} \mathrm{Culminate}(x,y) $$
then we simply have $p(w): \mathrm{Activity}$ on one hand, and $$q(w): \sum_{y:\mathrm{Achievement}} \mathrm{Culminate}(p(w),y)$$ on the other. Furthermore, if we know that $w=(a,(b,c))$, then the equalities $p(w) = a$ and $q(w) = (b,c)$ hold, and accordingly, by substituting these into the judgment above, we have $$(b,c): \sum_{y:\mathrm{Achievement}} \mathrm{Culminate}(a,y).$$
Repeating this process one more time would let us conclude $q(q(w)) : \mathrm{Culminate}(p(w),p(q(w)))$, or using the equalities above, $c: \mathrm{Culminate}(a,b)$ as expected.