Quotient Inductive Type

Definition

A quotient inductive type is a type of the form $W (S ◁ P) / \sim$ .

Quotient-inductive types for mobiles work constructively because the only identifications are local leaf permutations.
These identifications can be handled using setoids without needing choice.
Mobiles have local symmetric identification that is treatable with setoid-level constructions.
Their index order is a plump ordinal with definable suprema, ensuring cocontinuity of the quotient-polynomial functor.

Richer QITs, especially those involving recursive equations between constructors and paths, generally require some form of choice or WISC.
Choice enters when an element of a quotient in the base of a fibration must be represented by a specific representative.
This is essential when defining structural recursion or elimination on quotient structures.
General QITs involve global coherence, higher-dimensional identifications, or recursive quotienting, which require choice or WISC.

Fiore 2022 constructs QW-types, a restricted class of QITs, and requires WISC to do so constructively.
Fiore–Pitts–Steenkamp’s QWI types use very general signatures and require WISC to guarantee the existence of a suitable size for any signature.
Key difference from mobiles: general QITs are non-local and require global coherence, unlike mobiles.

QITs can be constructed constructively using a restricted system of sizes rather than full ordinals.
Each QIT signature should carry its own explicit size: a plump, well-founded order with locality information.
Sizes require only well-foundedness, transitivity, directedness, and the property that recursive calls strictly decrease.
Full ordinal structure is unnecessary; ordinal embeddings are not required.
A size can be generated automatically from constructor syntax; the user or library provides a rank function and the checker verifies decrease.
Classical ordinal comparison is optional and external.
“Ordinal diameter” is not relevant; what matters is rank or height of the plump order, obtained via a decreasing measure.

Permutation trees show that rank can grow as ω, ω², ω^ω depending on branching, arising from recursive measures rather than graph diameter.
Fully automatic inference of ordinal ranks is impossible in general due to undecidability.
Practical systems use syntactic checks and annotations.
Main barriers: complexity of size inference, ensuring equations are locality-compatible, universe levels, and conservativity.

Goal: understand when QITs can be constructed fully constructively without choice principles such as WISC.
Problem cases arise when quotient relations are non-local: require unbounded-depth reasoning, transitive closure, or global extensionality (e.g. ordinals).
Locality means the quotient depends only on bounded-depth structure.
Non-local QITs inspect unbounded structure and typically need choice or WISC.