Evan Cavallo

Postdoc at Göteborgs universitet. Types + Cubes

Last Notes

2026-05-04 08:48:12 UTC

Something new on the arXiv from Jonas Höfer (@nprofile…jpwq) and I today: "Univalence without function extensionality" https://arxiv.org/abs/2605.00812
We look at a definition of "equivalence" where instead of asking for homotopies---i.e., pointwise equalities---between the inverses, we ask for equalities of functions. We call this a "categorical equivalence", because its the definition you arrive at if you think of the universe as a wild category. If you define univalence using categorical equivalence, i.e. if you ask for the universe to be a univalent wild category, it turns out you get an axiom that doesn't imply function extensionality! This has long been suspected (https://mathoverflow.net/questions/134449/equivalent-form-of-the-univalence-axiom), but we prove it with a countermodel based on Von Glehn's polynomial construction. This is a construction on models whose outputs always refute function extensionality, but it turns out it carries through some amount of univalence from the base model.
We also show that the canonical map from categorical equivalences to equivalences is a equivalence if and only if function extensionality holds. This is a sharpening of Voevodsky's classic result that univalence implies function extensionality in the universe, and the proof uses the same ideas. To me this is a kind of answer to the old question of what is really going on in Voevodsky's proof, and whether the implication from univalence to funext is really fundamental or just an "accident".
(1/2)

2025-11-27 13:27:37 UTC

- reply

@nprofile…dand They have been at this for a while, scroll for example through https://arxiv.org/search/cs?searchtype=author&query=de+Oliveira,+A+G. I read through one of them many years ago and recall not being convinced, but I don't remember anything specific now.

2025-10-21 05:45:42 UTC

- reply

@nprofile…dand I see, thanks!

2025-10-21 01:29:39 UTC

- reply

@nprofile…dand What model is this? It may be relevant to me 🙃

2025-10-20 08:59:08 UTC

Type theory is weird

2025-09-30 12:23:38 UTC

- reply

@nprofile…6kk0 @nprofile…2pts The counterexample does apply. But the counterexample also applies to cartesian cubes, and as I wrote in https://mathstodon.xyz/@ecavallo/112262872461992336 I'm optimistic that an equivariance condition can also save reversals.
Unfortunately it doesn't pay too well to write this up; one would rather take some time to figure out the right general setting under which these equivariant model constructions give the right answer, instead of doing one more special case. But at least some of the necessary components could now be taken off the shelf from the equivariant cartesian paper, so maybe once I clear my plate a little (🙃) I should sit down and bang it out...

2025-08-25 11:40:38 UTC

My paper with Christian Sattler on cubes with one connection has been accepted to the Canadian Journal of Mathematics: https://doi.org/10.4153/S0008414X25101466
The title buries the lede (oops), but it's about a constructive model of homotopy/cubical type theory and a (classical) proof that its associated homotopy theory agrees with the homotopy theory of topological spaces. The first such model to be found with this property was https://arxiv.org/abs/2406.18497; this one is in some ways simpler, in other ways more complicated. The main technical work is in generalizing some combinatorial techniques from homotopy theory (Reedy category theory) to deal with a more exotic cube category (cartesian cubes with one connection) that came out of constructive semantics of homotopy type theory.
It's in copy-editing now, so this is your last chance to find us some typos ;)

2025-08-16 09:55:23 UTC

The usual proof of \((\lvert x\rvert_{n+1} = \lvert y \rvert_{n+1}) \simeq \lVert x = y\rVert_n\) uses a univalent universe. Anybody know a (non-univalent) model where it fails?

2025-08-10 16:13:45 UTC

(-1)-types (modest proposals)

2025-08-01 15:35:08 UTC

Here's a puzzle (don't know an answer) that came up while I was thinking about @nprofile…9vc2's "type-theoretic axiom of replacement".
Let's say we're in intensional MLTT with funext and a univalent universe U (but you can drop funext and univalence and I'm still interested in the answer).
Q: Are there any closed examples of a surjection f : A → B where A is U-small and B is locally U-small, but B cannot be proven to be U-small?
Here a type is U-small when it's equivalent to a type in U, and a type is locally U-small when its identity types are U-small. Since I'm not assuming a propositional truncation, f being surjective means that for any B-indexed family of h-propositions P, precomposition (-) ∘ f : (Πb:B.P(b)) → (Πa:A.P(fa)) is an equivalence.

2025-07-26 13:45:22 UTC

- reply

@nprofile…v2av For one thing I made a mistake, that should be S² → Type (corrected now). Thanks!
The universal property of S² as encoded in type theory is that a map S² → A is determined by a point a : A and a two-dimensional loop at a : A, i.e. an inhabitant of the interated identity type \(\mathsf{refl}_a =_{a =_A a} \mathsf{refl}_a\).
In this case, we build a map H into a universe, which I called "Type"; to do so we choose a type in Type and a two-dimensional loop at that type.
The type will be S¹.
For the two-dimensional loop, we use the univalence axiom for Type, which says that identities in it correspond to homotopy equivalences, and the reflexive identity corresponds to the identity equivalence.
It also implies that identities between equivalences correspond to homotopies between the underlying functions.
So giving an element of \(\mathsf{refl}_{S^1} =_{S^1 =_{\mathsf{Type}} S^1} \mathsf{refl}_{S^1}\) means giving an element of \(\mathsf{id}_{S^1} =_{S^1 ≃ S^1} \mathsf{id}_{S^1}\) means giving a family of identities \(x =_{S^1} x\) for all x : S¹.
The Hopf fibration H : S² → Type is what we get when for each x : S¹ we take the loop \(x =_{S^1} x\) that goes around the circle once.

2025-07-26 12:16:20 UTC

Doing synthetic homotopy theory in univalent type theory, we usually assume that we have a suspension type constructor from which we can define all the n-spheres. But a funny consequence of the Hopf fibration is that in univalent type theory with just a 1-sphere and a 2-sphere (but no other HITs assumed), we can already define a 3-sphere type, namely the Σ-type Σ(x:S²).H(x) with the Hopf fibration H : S¹ → Type definable by elimination into our univalent universe. Likewise, if we have 3- and 4-spheres we should be able to build the 7-sphere, and if we have 7- and 8-spheres the 15-sphere.
That exhausts the applications of this particular construction, by Adams' theorem. Are there any other ways to get new spheres from existing spheres by standard type-theoretic operations? (I don't know and I'm not the right person to ask. I also don't have any reason to ask; just wondering.)

2025-07-02 13:29:49 UTC

- reply

@nprofile…6kk0 @nprofile…tphs @nprofile…9vrk Re the EDIT: the Smith paper that afaik introduces large elimination (https://www.cse.chalmers.se/~smith/Rek.pdf) has the natural numbers as its main example, so imo it's not unclear what one needs to do; one just doesn't want to do it!

2025-06-20 21:21:59 UTC

Does anyone know of a model of intensional MLTT that satisfies LEM but not function extensionality? Preferably the strong version of LEM that says A or ¬A for all types A, not only h-propositions.

2025-06-09 10:35:09 UTC

- reply

@nprofile…hszg I think Bourke and Garner's paper https://arxiv.org/abs/1412.6559 contains a related result. I will not try to unfold everything here, but in Section 4.4 they show that for certain classes of monics M, there is an algebraic weak factorization system (L,R) where the L-coalgebras are the maps in M. They observe there that R sends a map to its partial map classifier. Then in Proposition 20 they prove that for general a.w.f.s, the R-algebras are maps with "coherent" lifting structure against a certain double category formed by the L-coalgebras. In this case, the two coherence conditions (in 5.1 and 6.1) are the pullback naturality and associativity you are looking at.

2025-06-04 04:13:41 UTC

https://arxiv.org/abs/2506.02759
Something on the arXiv from Christian Sattler and I today!
This paper is about small object arguments, which are used in homotopy theory to construct various factorizations of maps. A little more specifically, it's about Garner's *algebraic* small object argument, which is a more recent, more general, more frequently constructive variant of the original argument (due to Quillen). We start from a certain useful characterization of factorizations coming with Quillen's argument and hunt down an analogue of sorts for the algebraic case.
I hope the paper will be interesting to people who are interested in these things in general, but of course for me the motivation is in semantics of homotopy type theory. The algebraic small object argument is used in particular in the cubical model constructions, and the reason we ended up writing this paper is because we needed the result somewhere deep in an argument about these models. Someday you'll hear more about that :)
I talked about this work at HoTT/UF a month and a half ago, so you can check out some slides and video at https://hott-uf.github.io/2025/

2025-03-31 22:02:33 UTC

Today's rediscovery of literature I should be citing more often: Raffael Stenzel's thesis https://etheses.whiterose.ac.uk/24342/

2025-03-24 14:26:54 UTC

I see the contributed talks are now listed for HoTT/UF (https://hott-uf.github.io/2025/) and the WG6 meeting (https://europroofnet.github.io/wg6-genoa/)!