Philipp Joram @phijor@types.pl

Amazing, I noticed today that weak excluded middle ¬¬𝑃 ∨ ¬𝑃 is true! One just has to use the familiar properties of the field of real numbers.

I know this looks suspicious, so I formalized the proof in Agda, and included an informal explanation.

This is huge, we can do so much more now in constructive analysis.

https://gist.github.com/andrejbauer/689b17b10a4e80ea409d03ec030c98b3

Prompted by recent discussions, I got the boundary scavenging prototype back to roughly where it used to be. Demo attached!

If you want the details:

• Boundary information is not associated with clauses, but with interaction points

• This information is collected during unification, by looking at equations which are headed by a metavariable and "in the pattern fragment, modulo endpoints" (i.e.: all arguments are variables, which must be distinct, or i0/i1)

• A problem like this doesn't give a unique solution, but it does give a partial solution: it's a face of a partial element which the meta must extend (internally I don't represent these as Partials... yet). A spine like this can still be inverted [1], by skipping over endpoints, so the RHS can be put in the meta's context

• When printing, we can show the user this information

• Bonus: Unsolved boundary constraints aren't shown to the user (strictly speaking they shouldn't be highlighted, either, but it's a WIP). Might be too much, but I decided to suppress any unsolved constraint that's headed by an interaction meta

• Bonus: Since the equations we recover are in the meta's context, we can print the value of the term at each face, too! This closes a very old feature request: https://github.com/agda/agda/issues/3690

[1]: One of the many reasons trying to extend the pattern fragment sucks is that now there's ambiguity over how to abstract over the RHS:

?0 A x y p i0 = p i0

should this invert to

?0 := λ A x y p i (i = i0) → p i0

or

?0 := λ A x y p i (i = i0) → p i

but happily in this case it doesn't matter (I use the former). Now to test the hell out of the fancy substitutions I'm inventing...

"stop replacing wikis with discord servers!" sorry, misheard you and now the manpages are a discord server. oops

Once again bottlenecked by just how slow pretty-printing Agda terms is.. this is somehow a very absurd and very reasonable problem to have. Ugh

If you want a version of "gaslight gatekeep girlboss" which is gender neutral and appropriate for local cartesian closure appreciators try "sum substitute sections" (\Sigma_f -| f^* -| \Pi_f)

Every vector space is free on some set. That's one reason linear algebra is so nice. Amazingly, Steven Givant was able to classify the totally free algebraic gadgets! There aren't many, and I talked about them here earlier.

Now I've explained this more carefully on the n-Category Café:

https://golem.ph.utexas.edu/category/2023/01/freedom.html

and raised a puzzle. Suppose we define our gadgets not to be *sets* with extra bells and whistles, but objects of some *other* category with extra bells and whistles. What then?

Trying to nerd-snipe HoTTists because I've reached the point where I'm getting very disillusioned with a theorem. We'll work in HoTT + excluded middle¹.

Yes this is the eighth time I've posted this. So What. I don't have a post preview. Leave me alone.

This is sometimes called "Freyd's theorem": If a category \(\mathcal{C}\) admits products indexed by \(\mathrm{Arr}(\mathcal{C})\), then it is a preorder. There's a super thorough explanation of the proof by @andrejbauer here in MO: https://mathoverflow.net/questions/336607/can-there-be-a-small-complete-category-in-zf

The gist of the argument is as follows, but please refer to Andrej's post for the full details:

Given \( f, g : \mathrm{Hom}(a, b) \), we'll show it's not the case that \( f \ne g \); By EM, we have \( f = g \). Start by computing the really wide product \( z = \prod_{\mathrm{Arr}(\mathcal{C})} b \), satisfying \( \mathrm{Hom}(a, z) \cong \prod_{\mathrm{Arr}(\mathcal{C})} \mathrm{Hom}(a, b) \).

Define \( r : 2 \to \mathrm{Hom}(a, b) \) so it sends 0 to \( f \) and 1 to \( g \). Note: This really is the type of booleans, not the type of propositions under excluded middle. Define a map \( a : 2^{\mathrm{Arr}(\mathcal{C})} \to \mathrm{Hom}(a, z) \) which sends \( c \) to \( \langle r(c(i))\rangle_i \). Andrej's computation shows that this map is an injection, so since it's a map between sets, an embedding.

But therein lies the problem with this argument: What we really want is an embedding \( a' : 2^{\mathrm{Arr}(\mathcal{C})} \hookrightarrow \mathrm{Arr}(\mathcal{C}) \), since LEM implies this embedding splits with a surjective inverse \(X \to 2^X\), which contradicts... whatever you call that theorem. Cantor's theorem?

But unless \( \mathcal{C} \) is assumed to be a strict category, making \( \mathrm{Arr}(\mathcal{C}) \) into a set, we can't naïvely extend \( a' \) into an embedding with this larger codomain, essentially because concluding \( f = f' \) from \( (x, y, f) = (x, y, f') : \mathrm{Arr}(\mathcal{C}) \) is an illegal move: it fails pretty hard on univalent categories, where the best you can conclude is that \( f \) is equal to \( g \) adjusted by isomorphisms induced by the identifications \(x = x\) and \(y = y\).

As a concrete failure case, consider e.g. the arrows \(\mathrm{id}\) and \(\mathrm{not}\), which are identified in \(\mathrm{Arr}(\mathbf{Sets})\) since we can modify either the domain or codomain by \(\mathrm{not}\).

My question/challenge/source of despair is threefold, but really, it's various degrees of giving up:

1. Can the argument above be patched: am I missing something really obvious that allows us to derive \(\neg (f \ne g)\) and conclude \(\mathcal{C}\) is a preorder?

2. If the argument can't be patched, is there some other way of proving \(\mathcal{C}\) is a preorder? I tried for a little while but none of my ideas really panned out.

3. If you're feeling adversarial, can you come up with a complete univalent category which admits limits the size of its arrow category?

¹: If you're asking why I'm trying to prove a classical theorem, it's just so that I have somewhere to point to, on the 1Lab, for why e.g. the AFT for categories needs to be so complicated.

@gallais @jonmsterling What fun!

EDIT: we did this drawing on Sunday, 15 January

https://mathstodon.xyz/@nilesjohnson/109695494574553537

Thanks everyone; I only wish I had more to give away!

--

I have an extra copy of my 2-categories book, and it seems silly to leave it on my shelf. Does anyone want it? I'll hold a raffle to give it away in a week or so! If you want to be entered:

1. reply below and
2. boost this post for visibility.

Note that this is for a *physical copy*. If you just want an electronic copy, it's on the arxiv!

https://arxiv.org/abs/2002.06055

air🅱️

another day volunteering at the MLTT museum. everyone keeps asking me if they can fuck the identity type. buddy, they won't even let me fuck it

My kid is so hipster they don’t listen to Joy Division, they listen to a Russian band that sounds like Joy Division instead. https://youtu.be/HR5zpFs7YpY

I didn't expect we would ever see a replacement of #Agda's oldest components, but here it is: https://github.com/agda/agda/pull/6410

Nervous about giving a talk? Your thesis defence? Here's why, even though you're standing at the edge of human knowledge, you shouldn't fear falling. https://scientistseessquirrel.wordpress.com/2022/12/20/dont-fear-falling-at-the-edge-of-knowledge-2/

good morning

I've finally had time to upload my Agda talk sources about "Dimension analysis and graded algebras" to github: https://github.com/DSLsofMath/dimensionanalysis

(This includes my first real use of @wen 's setup-Agda continuous integration scripts: https://github.com/wenkokke/setup-agda.)

Earlier blog post:
https://patrikja.owlstown.net/posts/1127-first-and-31-st-agda-meetings

The talks were recorded https://www.youtube.com/playlist?list=PL_DwsquKqQhKR-KuBmRxsfIWEVHV1itou
by O. Melkonian https://omelkonian.github.io/

Using #vim is easy once you learn a few basic keybindings.

h and l - move left and right
j and k - move down and up
η and λ - move backwards and forwards through time
ξ and κ - translation through additional temporal dimension (if applicable)
ᚻ, ᛄ, ᚳ and ᛚ - moving left, down, up, and right through celestial spheres
𐤄 and 𐤋 - switch deity to pantheon member to left or right
ᛄ - supplicate to chosen deity
ᚳ - challenge chosen deity (dangerous)
:q - exit

This week the #HoTTEST seminar has talks by junior researchers Astra Kolomatskaia and Philipp Joram on topics in homotopy type theory #HoTT:

Astra Kolomatskaia: Why are semi-simplicial types hard?

Philipp Joram: Final coalgebras of analytic functors in homotopy type theory

The talks start at 11:30am EST (UTC-5) on Thursday, Dec 15 and are followed by Gather Town. See https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html for the Zoom link, abstracts, and calendar of all upcoming talks.