Positive h-levels are closed under W

I was asked about my proof showing that positive h-levels are closed under W (assuming extensionality), so I decided to write a short note about it.

W-types are defined inductively as follows (using Agda notation):

data W (A : Set) (B : A → Set) : Set where
  sup : (x : A) → (B x → W A B) → W A B

The result can then be stated as follows:

(A : Set) (B : A → Set) →

((x : A) (C : B x → Set) (f g : (y : B x) → C y) →
   ((y : B x) → f y ≡ g y) → f ≡ g) →

(n : ℕ) → H-level (1 + n) A → H-level (1 + n) (W A B)

Here _≡_ is the identity type, and H-level n A means that A has h-level n. Note that B, which is only used negatively in W, can have any h-level. Note also that h-level 0 is not closed under W: the type W ⊤ (λ _ → ⊤) is empty (where is the unit type).

Sketch of the proof:

  1. It is easy to see that W A B is isomorphic to Σ A (λ x → B x → W A B).
  2. Using this isomorphism and extensionality we can prove that, for any x, y : A, f : B x → W A B, and g : B y → W A B, there is a surjection from
    Σ (x ≡ y) (λ p → (i : B x) → f i ≡ g (subst B p i))


    sup x f ≡ sup y g.

    (The subst function is sometimes called transport.)

  3. We can wrap up by proving
    (s t : W A B) → H-level n (s ≡ t)

    by induction on the structure of s. There is one case to consider, in which s = sup x f and t = sup y g. From the inductive hypothesis we get

    H-level n (f i ≡ g j)

    for any i, j. In particular, if we assume p : x ≡ y, then we have

    H-level n (f i ≡ g (subst B p i)).

    All h-levels are closed under \Pi (B x) (assuming extensionality), so we get

    H-level n ((i : B x) → f i ≡ g (subst B p i)).

    Every h-level is also closed under Σ, so by the assumption that A has h-level 1 + n we get

    H-level n (Σ (x ≡ y) (λ p → (i : B x) → f i ≡ g (subst B p i))).

    Finally H-level n respects surjections, so by step 2 above we get

    H-level n (sup x f ≡ sup y g).

See the code listing for the full proof, which is stated in a universe-polymorphic way. (Search for “W-types”, and note that identifiers are hyperlinked to their definition.)

This entry was posted in Code. Bookmark the permalink.

18 Responses to Positive h-levels are closed under W

  1. Steve Awodey says:

    Thanks Nils — that certainly answers my question!

  2. Mike Shulman says:

    I still have a bit of trouble parsing Agda code mentally. I see that by “extensionality” you mean “function extensionality”. By “surjection” do you mean “split surjection”?

    • Nils Anders Danielsson says:

      By “surjection from A to B” I mean a triple containing f : A → B,
      g : B → A, and a proof of (x : B) → f (g x) ≡ x.

      • Bas Spitters says:

        With Egbert Rijke, we proved that if all surjections are split, then we have excluded middle, following the usual Diaconescu Theorem.

        • Mike Shulman says:

          So maybe it would better not to use “surjection” to mean “split surjection”? (That is, at least if we want to avoid assuming PEM.)

          • Nils Anders Danielsson says:

            I’m not familiar with the term “split surjection”. In fact, I used a well-known search engine to search for “split surjection”, and this very blog post was one of the first twenty hits, so I imagine that the term isn’t very common. 🙂

          • Mike Shulman says:

            Try “split epi”.

            • Nils Anders Danielsson says:

              With this terminology I guess that “surjection” stands for epimorphism.

              There are several ways to turn the set-theoretic concept of surjection into a type-theoretic one. The one I’ve used is a very naive one: just map ∀, ∃, → and = to Π, Σ, → and ≡. However, if there is an established terminology, then I should of course use it.

              • Steve Awodey says:

                it’s not the same as “epimorphism”, because an epi is an arrow that cancels on the right:
                f\circ e = g\circ e \Rightarrow f = g. These are the surjections in Sets, but that’s a rather special case.

              • Mike Shulman says:

                The epis are also the “internal” surjections in any topos, or more generally any pretopos. But when we move to higher h-levels, then the concepts and terminology get more murky. It seems that probably instead of the usual definition of “epimorphism” what one cares about is the “effective epimorphisms”, those that are the “quotient of their kernel” in a suitable higher-categorical sense. It’s also true in 1-category theory that it’s really the effective epis that are more important — e.g. in a regular category that isn’t balanced, it’s the effective (= regular) epis that are the “internal surjections”, not the plain epis. However, in a 1-category, it’s at least true that every morphism that is the quotient of its kernel is an epimorphism, so it makes sense to name them with an adjective in front of “epimorphism”. But this seems to no longer be true in a higher category.

                When speaking internally (as we do when doing type theory), I think it still makes sense to call these “surjections” (and add the word “split” when it applies). In the standard model of \infty-groupoids, they are the “essentially surjective functors”, those that are surjective on \pi_0. And when talking about higher-categorical semantics, I think most people still just say “effective epi” and rely on the red herring principle. It’s a little unfortunate, but no one has come up with a better name.

          • Bas Spitters says:

            I would prefer to keep “surjection” and “split surjection” separate. If the surjection (epi) is split, just say so.

    • Mike Shulman says:

      (Jumping back down a few comment nesting levels to maintain a reasonable text width.)

      Yes, it all depends on whether you use propositions-as-types logic or propositions-as-squashed-types logic. Personally, I am in favor of propositions-as-squashed-types logic, since it is strictly more expressive and matches categorical semantics better. Plus, I think one of the whole points of h-levels is that the h-props are a good notion of (proof-irrelevant) proposition, and that entails propositions-as-squashed-types.

      • Steve Awodey says:

        The question is how to translate conventional first-order logical properties — in this case of functions between types/sets — into type theory. As Mike says, if we use PaT, we get one thing, and if we use Pa[T] we (often) get something different. This is of course a good thing — our type-theoretic language is more expressive — but one therefore needs to be careful — and explicit — about such renderings.

        In this example of surjections, the issue is whether or not the existence of a preimage is “squashed”. If not, and one renders the condition \forall\exists \ldots as \Pi \Sigma\ldots, then obviously (by the type-theoretic axiom of choice) there will be a section of the map — i.e. a “splitting”. If one squashes the sigma down to an existential quantifier as in \Pi [\Sigma\ldots], then the condition is weaker. Perhaps this condition should be called a “surjection”, and the stronger condition a “split surjection” — or these could be called “weak” and “strong” surjections — it’s just a question of terminology, but it’s important to decide it to avoid this kind of confusion.

        By the way, an old paper of mine shows that the two conditions coincide if and only if (the PaT version of) the LEM holds.

  3. Dan Licata says:


    BTW, using univalence, it’s easy to see that step 2 is really an isomorphism, not just a surjection, and that it really follows from general principles (I didn’t type this in to check it, but I’m pretty sure.):

    * Since Wx:A.B == Σx:A.B x -> Wx:A.B, using univalence to transport at the corresponding identity types shows that Id{Wx:A.B} (sup(x,f)) (sup(y,g)) is isomorphic to Id{Σx:A.B x -> Wx:A.B} (x,f) (y,g). I.e., because the W-type is isomorphic to its unrolling, paths at W are isomorphic to paths at the unrolling (coerced by sup).

    * From there, you just apply the standard “definitions” of Id for Σ and -> (Id at Σ is a pair of Ids; Id at -> is function extensionality) to show that this is isomorphic to the type you gave in 2).

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s