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...
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:
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?
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.
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.
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!
@mhoye Well, there is a political solution: in France, a law from 2016 allows (public) researchers to open-access their own articles. Almost all science from France ends up as PDF on https://hal.archives-ouvertes.fr/
Some French universities even **require** their staff to open-access everything.
The only thing an editor can ask is an embargo of max. 6 months (12 months for social sciences)
This was not easy, but there is a big "open science" movement in France.
More info: https://www.ouvrirlascience.fr/home/
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/
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
On the \(\infty\)-topos semantics of homotopy type theory
http://arxiv.org/abs/2212.06937
#arXiv_2212_06937
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.
PhD Student at Tallinn University of Technology.
Learning about type theory. Chasing the diagrams.
{love, marry, debug} ≃ {Agda, Rust, Nix}.