Does this really use advanced features of Homotopic Type Theory? Does it really require the Univalence Axiom? (Caveat: I don't yet properly understand either of those two things.)
It seems to me that the representation of cardinalities as "Univalent Types" could just as easily be done using Decidable Setoids (eg the number 3 is represented by a Setoid with a decidable equivalence relationship that divides its members into 3 equivalence classes).
There are only four things in this system that require a notion of equality and/or equivalence: tuples, cardinalities, relations (as functions from tuples to cardinalities) and queries (as functions from relations to relations).
I think this could all be done with in ordinary plain dependent type theory, without any HOTT or Univalence Axiom (for example, in Idris, which is apparently incompatible with the Univalence Axiom). Each of the four notions of equivalence would be represented by a corresponding type function.
It seems to me that the representation of cardinalities as "Univalent Types" could just as easily be done using Decidable Setoids (eg the number 3 is represented by a Setoid with a decidable equivalence relationship that divides its members into 3 equivalence classes).
There are only four things in this system that require a notion of equality and/or equivalence: tuples, cardinalities, relations (as functions from tuples to cardinalities) and queries (as functions from relations to relations).
I think this could all be done with in ordinary plain dependent type theory, without any HOTT or Univalence Axiom (for example, in Idris, which is apparently incompatible with the Univalence Axiom). Each of the four notions of equivalence would be represented by a corresponding type function.
Have I missed something?