David Corfield elements

The type of elements, $\widehat{Type}$, is such that it contains as elements $(A, a)$ where $A$ is a type and $a: A$. Say we want to distinguish between a kind of activity and instances of that kind – running and occasions/instances of running.

Running: Activity, El(Running).

$X:Achievement, x: X \vdash t(x): Time, l(x): Location$

$u: Time, v: location \vdash Rain(u, v): Prop$

$x: Person, y: Object \vdash x\; lit\, y: Achievement$

$John\; lit\; a\; cigarette: Achievement$

$z: John\; lit\; a\; cigarette \vdash t(z): Time; l(z): Location$

$\prod_{z: John\; lit\; a\; cigarette} Rain(t(z), l(z))$