# David Corfield Chapter 2 Dependent types

• Some propositions treated in this chapter have event structures as discussed later on. So the construction of ‘leaving off’ or stopping, might be characterised via a map $stop: Activity \to Achievement$.