Towards an Override in Topoi

Models of software systems are built in Z and VDM using partial functions between sets and certain operations on these partial functions : extension (⊔), restriction (◃), removal and override (†). Can these operations be given a categorial semantics? Doing so will show the 'nature' of the operations. The operation of override is found to depend on the 'shape' on X, the poset PX. The operations are developed in an elementary topos E. This is achieved by constructing each operation in the topos Set, of sets and total functions, and then using these constructions as the definition of the operations in an elementary topos. Each of the operations is thus given a categorical semantics. As an example the operation of override is considered in the topos Set↓, of total functions and commuting diagrams. Can models of software systems be built in topoi other than Set?