QW Type

Idea

A QW type combines W types with a system of equivalence relations.

Definitions

System of Equations over a Container

Definition

Let $\Sigma =S◁P$ be a container. A system of containers over $\Sigma$ is specified by:

• A type $E:\mathcal{U}$
• A function $V:E\to \mathcal{U}$
• For each $e:E$, two elements $le,re:T_{\Sigma }(Ve)$

These represent the following notions.

• $E$ indexes the equations.
• $Ve$ indexes variables for each equation.
• $le,re$ represent AST’s in variables for the the left and right side of the equation.

Here $T_{\Sigma }(V)$ is the free $S_{\Sigma }$-algebra¹ on $V$. Specifically, it is the least type that consists of:

• $\eta :V\to T_{\Sigma }V$
• $\sigma :S_{\Sigma }(T_{\Sigma }V)\to T_{\Sigma }V$

Link to original

Plump Order

Definition

Let $W=(\mu X.S◃P)$ be a W type for the container $S◃P$. We define the relations $\le$ and $<:{\mathrm{Rel}}_2(W)$ via an inductive-inductive definition:

$$\begin{array}{rlrl}& \frac{\forall (i:Ps).fi<t}{(s,f)\le t}& & \text{(Bounded by strict predecessors)}\\ & & & \\ & \frac{\exists (i:Ps).t\le fi}{t<(s,f)}& & \text{(Dominated by a predecessor)}\end{array}$$ Link to original

WISC

Definition

A weakly initial set of covers over $Y$ is just a weakly initial set in the category of covers $\mathbf{Cov}(Y)$.

That is:

$$\begin{array}{rl}& \text{Suppose }(I,\bar{X}):\prod _{i:I}\mathrm{Cov}(Y).\\ & \text{Say }(I,\bar{X})\text{ is WISC for Y iff}\\ & \forall q:Z\twoheadrightarrow Y\\ & \exists i:I;f:X_i\to Z\\ & \text{s.t. }q\circ f\text{ is a surjection}\end{array}$$ Link to original

Remarks

Why WISC is needed

Suppose WISC doesn’t hold. Pick $\{c_i:C_i\to A\}$ weakly initial. Construct fibration $\pi :WA\twoheadrightarrow A$. with fibres containing all well-founded trees labeled by $A$. If all ordinals have cofinality $\omega$ then the trees have unbounded height.

Examples

A (finite) multiset can be defined as:

data Bag (A : Type) : Type where
	[] : Bag A
	_::_ : A -> Bag A -> Bag A
	x :: y :: xs == y :: x :: xs

References

Defined in fiore2022-quotient-inductive.