Type theoretical databases
Journal article, Peer reviewed
MetadataShow full item record
Original versionJournal of Logic and Computation. 2020, 30 (1), 217–238. 10.1093/logcom/exaa009
We show how the display-map category of finite (symmetric) simplicial complexes can be seen as representing the totality of database schemas and instances in a single mathematical structure. We give a sound interpretation of a certain dependent type theory in this model and show how it allows for the syntactic specification of schemas and instances and the manipulation of the same with the usual type-theoretic operations.