In recent years in the bx literature, attention has turned to incorporating intensional information about edits (based on monoid actions [HPW12,AU14, for example]), or more generally, deltas (based on categories [DXC11a, DXC+11b]), describing model updates. This talk sketches a dependently-typed approach to consistency maintenance, a la Meertens/Stevens [Mee98, Ste10], building on a propositions-astypes account of consistency [McK16]. The resulting de nition of dependently-typed bx (dtbx) has identities and is closed under composition; examples include the above instances of delta-based bx. The definition is \pre-categorical", relying on no ambient assumptions about categorical structure on model spaces. We reconcile the dependentlytyped approach to deltas with the categorical by examining analogues of the hippocraticness and overwriteability properties, and discuss this relationship in the context of recent developments in type theory.
[AU14] [DXC11a] [HPW12] [McK16] [Mee98] [Ste10]
J. McKinna. Complements witness consistency. In these proceedings, 2016.
L. Meertens. Designing constraint maintainers for user interaction. Unpublished manuscript, available from http://www.kestrel.edu/home/people/meertens/, June 1998.