20251203-wisc

WISC: Weakly Initial Sets of Covers

Overview

It explains the motivation, internal formulation, and role of WISC within the Fiore–Pitts–Steenkamp (2022) construction of quotient W-types.

Covers and Their Category

Fix a universe $U$. For any type $Y:U$, a cover of $Y$ is a surjective map $q:X\twoheadrightarrow Y$ with

$$\mathrm{isSurj}(q):=\prod _{y:Y}\parallel \sum _{x:X}q(x)=y\parallel .$$

The category of covers $\mathbf{Cov}(Y)$ has:

• objects: pairs $(X,q)$ with $q:X\twoheadrightarrow Y$
• morphisms $f:(X,p)\to (Z,q)$ satisfying $q\circ f=p$

This captures surjections as structure-preserving bundles with explicit fibres.

Weakly Initial Sets of Covers

A family of covers $\{p_c:E(c)\twoheadrightarrow Y{\}}_{c:C}$ is weakly initial if every cover $q:Z\to Y$ admits a morphism from some $(E(c),p_c)$:

$$\exists c:C.\exists f:E(c)\to Z.q\circ f=p_c.$$

This means every surjection onto $Y$ factors through one of a small, fixed family of surjections. It is a strictly weaker form of the Axiom of Choice: it does not choose points in fibres, only a universal domain through which each cover can be reached.

Internal Formulation Used by Fiore–Pitts–Steenkamp

Inside type theory it is often preferable not to store the maps $E(c)\to Y$ explicitly. Instead one requires:

A family $(C,E)$ is a wisc for $Y$ if for every cover $q:Z\twoheadrightarrow Y$ there exist $c:C$ and $f:E(c)\to Z$ such that $q\circ f$ is surjective.

This induces a weakly initial family of covers, but the maps to $Y$ are derived on demand as $q\circ f$. This avoids additional structure and aligns with the internal dependent-type-theoretic treatment of surjectivity.

Indexed WISC (IWISC)

For a family $(A,B)$ with $B:A\to U$, a single $(C,E)$ is a wisc for $(A,B)$ if it is a wisc for each $B(a)$. The same family of domains uniformly dominates all covers of all fibres $B(a)$.

This uniformity is essential: quotient W-types require a single size object and a single cover base to control all constructor arities simultaneously. Separate WISC families for each $B(a)$ are not sufficient.

WISC as a Minimal Choice Principle

WISC stands strictly between:

• no choice (surjections need not split and covers may have no sections)
• the Axiom of Choice (every surjection splits)

It provides exactly the amount of choice required to replace AC in the theory of W-types: instead of choosing points in fibres, WISC chooses standard shapes of covers.

Notably:

• WISC does not imply countable or dependent choice
• WISC is strictly weaker than full AC
• WISC holds in many constructive models (sheaf toposes, realisability)
• WISC fails in some models of ZF

Role of WISC in the Size Construction

The Fiore–Pitts–Steenkamp construction introduces a well-founded type Size, analogous to ordinals under suprema, used to index a transfinite colimit.

WISC is used to:

1. produce a small family of canonical cover shapes for each $B(a)$
2. build a W-type over this family
3. ensure this W-type is closed under the required colimit operations
4. ensure polynomial functors preserve the Size-colimit

Without WISC, Size cannot be constructed uniformly for all $B(a)$.

Polynomial Functors and WISC

Given a signature with arities $B(a)$, the associated polynomial functor

$$S_{\Sigma }(X)=\sum _{a:A}{X}^{B(a)}$$

must preserve the Size-colimit. The proof requires surjective comparison maps between power objects to be surjective and injective. Both directions rely on invoking WISC to factor arbitrary covers of $B(a)$ through the canonical family $E(c)$.

Thus WISC ensures $S_{\Sigma }$ is cocontinuous with respect to the Size-indexed diagram.

Construction of QW/QWI-Types

With Size and cocontinuity established:

• one forms a transfinite sequence of approximations to the desired inductive object
• each stage applies the polynomial functor and quotienting operations
• Size-indexed colimits yield the final carrier
• algebraic structure transfers along the colimit

WISC’s uniform cover base is required at each stage for replacing arbitrary covers with canonical ones. This supports both the induction and quotienting components of QWI-types.

Consequences

Under IWISC, Fiore–Pitts–Steenkamp (2022) derive:

• existence of general quotient W-types internally
• support for uncountable and infinitary constructors
• compatibility with sheaf and realisability semantics
• elimination of the need for classical choice

WISC is therefore the precise constructive choice principle necessary for QWI-types: weak enough to hold in important models, but strong enough to supply the uniform cover bases needed for Size and cocontinuity.