Toots for ecavallo@mathstodon.xyz account

Written by Evan Cavallo on 2024-12-30 at 14:58

I finally started making all the pent-up edits I've been meaning to make to the nLab articles on cubes, which means I need to issue a formal apology to everyone for annihilating this gem:

=> View attached media

=> More informations about this toot | View the thread

Written by Evan Cavallo on 2024-12-26 at 13:06

In a retract diagram, one object is called the "retract". What would you call the other object?

=> More informations about this toot | View the thread

Written by Evan Cavallo on 2024-11-11 at 13:15

Now let's see a cool application of 6-for-2 in HoTT

=> More informations about this toot | View the thread

Written by Evan Cavallo on 2024-10-21 at 11:27

Christian Sattler is looking to hire a postdoc in the areas of higher category theory, homotopy type theory, and/or constructive mathematics at Chalmers here in Gothenburg, with application deadline November 3: https://www.chalmers.se/en/about-chalmers/work-with-us/vacancies/?rmpage=job&rmjob=13267&rmlang=UK.

=> More informations about this toot | View the thread

Written by Evan Cavallo on 2024-10-07 at 18:29

Given ( A, B : U_i ), we have plenty of equivalent definitions of the type ( A \simeq B ) of equivalences. Among these, there is the definition from Exercise 4.2 of the HoTT Book:

[ \sum_{R: A \to B \to U_i} \left(\prod_{a:A} \mathsf{isContr}\left(\sum_{b:B} R(a,b)\right)\right) \times \left(\prod_{b:B} \mathsf{isContr}\left(\sum_{a:A} R(a,b) \right)\right) ]

which, unlike the other definitions I know of, has the nice property that ( A \simeq B ) is definitionally isomorphic to ( B \simeq A ) (if we assume the standard definitional (\eta)-equality for (\Sigma)- and (\Pi)-types), in the sense that we have back-and-forth maps which are inverse up to definitional equality. But it also has the less nice property that ( A \simeq B : U_{i+1} ), that is, that the type of equivalences lives one universe higher than ( A ) and ( B ) do.

Is there an equivalent definition of ( A \simeq B ) that both (1) is symmetric up to definitional isomorphism and (2) lives in the same universe as ( A ) and ( B )? Or can we prove that no such thing is definable in (some flavor of) HoTT?

=> More informations about this toot | View the thread

Written by Evan Cavallo on 2024-08-28 at 12:30

👀

=> View attached media

=> More informations about this toot | View the thread

Written by Evan Cavallo on 2024-08-22 at 09:16

They're not really related, but reading Tom de Jong's nice note (just boosted) sparked a memory of this interesting paper of Orton and Pitts from 2017, which breaks down the univalence axiom into a few special cases: https://arxiv.org/abs/1712.04890

This strategy for checking univalence in models didn't really catch on to my knowledge, but maybe it's worth revisiting!

(The conjecture discussed in §6, that naive univalence implies full univalence, is resolved in the negative by the cardinal model, see Théo Winterhalter's PhD thesis: https://theowinterhalter.github.io/#phd)

=> More informations about this toot | View the thread

=> This profile with reblog | Go to ecavallo@mathstodon.xyz account