Another application of HIITs (or QIITs)

[Altenkirch Thorsten]

I just noticed that there is another interesting application of Higher Inductive-Inductive definitions (however, at least in the moment I am thinking of 1st order HIIts, I.e. a HIIT defining a set which I call QIITs = Quotient inductive inductive definitions).

When internalizing type theory, we are tempted to use an inductive-inductive definition inductively defining

[I am writing Set intentionally, since these are all 0-types].

Con : Set

Type : Con -> Set

Term : Pi (G : Con) Type(A) -> Set

Subst : Con -> Con -> Set

I spare you the details. However, we also need to define equivalence relations on each of them. This is additionally complicated by the fact that the types depend on each other. It may look something like this:

~Con : Con -> Con -> Prop

~Type : Pi (G,G' : Con)(G ~Con G') -> Type(G) -> Type(G') -> Prop

~Term : Pi(G,G':Con)(p : G ~Con G')(A : Type(G))(A' : Type(G')) (A ~Type(G,G',p) A') 

-> Term(G,A) -> Term(G',A') -> Prop

~Subst : Pi(G,G':Con)(p : G ~Con G')(D,D':Con)(D ~Con D') Subst(G,D) -> Subst(G',D') -> Prop

While this is already quite disgusting it is getting worse: for each constructor above we have to add a congruence rule for the equalities. And we need transport maps, e.g. if we have p : G ~Con G' we need a map 

transport : Type(G) -> Type(G') which appears as an additional constructor for Type. Moreover we need to state that the transport maps are functorial which show up as additional constructors for the ~ relation.

My former student James Chapman had quite a go at something like this in his paper "Type Theory should eat itself" but the result invariably gets so complicated that you can't actually do anything with it and in particular we weren't even sure wether we got it right. He also had to cope with the fact that we don't have Prop in Agda and hence proof-irrelvance has to be built into the definitions.

However, in the presence of HIITs (or QIITs) it all becomes very straightforward: all we need to do apart from stating the constructors for contexts, etc is to state the rules for conversion as equality constructors (and force everything to be 0-truncated). An application of this is for example Guillaume's weak omega groupoids with explicit substitutions (which I think is preferable to defining substitutions recursively which already isn't completely straightforward).

Thorsten