Cubical Sets Axiomatised in the Internal Type Theory of a Topos
We take up a suggestion of Coquand to axiomatize within the internal logic of an elementary topos the constructions involved in the cubical sets model of Homotopy Type Theory of Cohen-Coquand-Huber-Mortberg (CCHM). We take the internal logic to be a form of extensional dependent type theory extending intuitionistic higher-order logic.
Working in this internal type theory we consider (1) an interval object equipped with a simple form of path connection structure (rather than a full de Morgan algebra structure) and (2) a collection of "cofibrant" monomorphisms classified by a distinguished subobject of propositions. We investigate what properties of (1) and (2) are needed to develop notions of fibrations, path/identity types, "glueing" and a form of univalence. The axioms we obtain are quite weak and can be satisfied in a number of ways, one of which is the motivating presheaf CCHM model.