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:
- It is easy to see that
W A Bis isomorphic toΣ A (λ x → B x → W A B). - Using this isomorphism and extensionality we can prove that, for any
x,y : A,f : B x → W A B, andg : B y → W A B, there is a surjection fromΣ (x ≡ y) (λ p → (i : B x) → f i ≡ g (subst B p i))
to
sup x f ≡ sup y g.
(The
substfunction is sometimes called transport.) - 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 whichs = sup x fandt = sup y g. From the inductive hypothesis we getH-level n (f i ≡ g j)
for any
i,j. In particular, if we assumep : x ≡ y, then we haveH-level n (f i ≡ g (subst B p i)).
All h-levels are closed under
(B x)(assuming extensionality), so we getH-level n ((i : B x) → f i ≡ g (subst B p i)).
Every h-level is also closed under
Σ, so by the assumption thatAhas h-level1 + nwe getH-level n (Σ (x ≡ y) (λ p → (i : B x) → f i ≡ g (subst B p i))).
Finally
H-level nrespects surjections, so by step 2 above we getH-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.)
Homotopy Type Theory 
Thanks Nils — that certainly answers my question!
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”?
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.
With Egbert Rijke, we proved that if all surjections are split, then we have excluded middle, following the usual Diaconescu Theorem.
So maybe it would better not to use “surjection” to mean “split surjection”? (That is, at least if we want to avoid assuming PEM.)
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. 🙂
Try “split epi”.
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.
it’s not the same as “epimorphism”, because an epi is an arrow that cancels on the right:
. These are the surjections in Sets, but that’s a rather special case.
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
-groupoids, they are the “essentially surjective functors”, those that are surjective on 
. 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.
I would prefer to keep “surjection” and “split surjection” separate. If the surjection (epi) is split, just say so.
(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.
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
as 
, 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]](https://s0.wp.com/latex.php?latex=%5CPi+%5B%5CSigma%5Cldots%5D&bg=ffffff&fg=333333&s=0&c=20201002)
, 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.
I guess this is really the Diaconescu argument I am refering to above, isn’t it? In fact, the Diaconescu Theorem seems to be an old observation, already in Problem 2 on page 58 in Bishop ’67.
That’s one direction. The other is given e.g. here:
Click to access ac.pdf
Nice!
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).
You don’t need univalence. I just added a proof (with the enlightening name W-≡,≡≈≡) to http://www.cse.chalmers.se/~nad/listings/equality/Weak-equivalence.html.
Cool! I didn’t mean to imply that you *needed* univalence—indeed, if the computational conjecture is true, you essentially have to be able to prove this without univalence. What I was trying to point out is that univalence is a nice way to think about what’s going on, because it immediately tells you that equivalent types will have equivalent identity types.