ConTy

Idea

This is a simplification of type theory syntax used as a ‘difficult enough’ QIIT to test constructions while keeping constuctors to a minimum.

Definition

Given sorts $\mathrm{Con}:\mathrm{Set}$ and $\mathrm{Ty}:\mathrm{Con}\to \mathrm{Set}$, we define a quotient inductive-inductive type with the following constructors:

$$\begin{array}{rl}\epsilon & :\mathrm{Con}\\ \mathrm{ext}& :(\Gamma :\mathrm{Con})\to \mathrm{Ty}(\Gamma )\to \mathrm{Con}\\ \iota & :(\Gamma :\mathrm{Con})\to \mathrm{Ty}(\Gamma )\\ \sigma & :(\Gamma :\mathrm{Con})\to (A:\mathrm{Ty}(\Gamma ))\to \mathrm{Ty}(\mathrm{ext}\Gamma A)\to \mathrm{Ty}(\Gamma )\\ {\sigma }_{\mathrm{eq}}& :\forall \Gamma AB\to \mathrm{ext}(\mathrm{ext}\Gamma A)B=\mathrm{ext}\Gamma (\sigma \Gamma AB)\end{array}$$

References

altenkirch2016-qiit