 |
Posts by [email protected] |
 |
Post #AXUCoGUqrMv2cbBjw8 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
Enter leftover typing! Instead of using context splits, we can have our morphis… |
|
|
|
Post #AXUCoHWJ3Rg1nOsPqK by [email protected] |
|
0 likes, 0 repeats |
|
|
|
Unfortunately, these type-theoretic methods aren't totally free, and we pay… |
|
|
|
Post #AfSfa0ZlSXf1B58Tbc by [email protected] |
|
0 likes, 0 repeats |
|
|
|
Shit I’m going to have to actually learn commutative algebra aren’t I |
|
|
|
Post #AfSfa1Uq2LJY25q3ZA by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@boarders Turns out polynomial functors should be handled like polynomials, who… |
|
|
|
Post #AfSoMMiDGA4tMiemRs by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@johncarlosbaez @boarders The structure is quite lovely, but the proofs are les… |
|
|
|
Post #AfTqe4ghPHgJk6Ts6y by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@boarders @johncarlosbaez Uses of choice also are a bit scary WRT categorificat… |
|
|
|
Post #Afge7w2nKpx3H0Cf2W by [email protected] |
|
0 likes, 0 repeats |
|
|
|
I think that nix has to be the most *actively* user-hostile software I've e… |
|
|
|
Post #Afge7w7351M1UCC3fc by [email protected] |
|
0 likes, 0 repeats |
|
|
|
Every command tells me to run another command, and the command it told me to ru… |
|
|
|
Post #An6FT8gPjx0GZk2i7k by [email protected] |
|
0 likes, 0 repeats |
|
|
|
Inspired by discussions with @ToucanIan, I’ve come up with what I think is a … |
|
|
|
Post #An6FT8pdBgNN2KM4US by [email protected] |
|
0 likes, 0 repeats |
|
|
|
First, some observations: Knaster-Tarski isn’t really a theorem about fixpoin… |
|
|
|
Post #An6FT8wilK2zOJfjXc by [email protected] |
|
0 likes, 0 repeats |
|
|
|
The naive generalization is to turn this meet into a limit over the category of… |
|
|
|
Post #An6FT97096GpuCTwZ6 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
Now for the proof! Let C be a kappa-complete category, F an endofunctor, and as… |
|
|
|
Post #An6FT9Nf99b8jsHFXE by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@zanzi It's a size thing: you have all kappa-small limits. In type-theoreti… |
|
|
|
Post #AnsTUEBdUL0msc8Vfs by [email protected] |
|
0 likes, 0 repeats |
|
|
|
Omg why |
|
|
|
Post #AnsTUELCukfTMIc9aq by [email protected] |
|
0 likes, 0 repeats |
|
|
|
This is from “Mal’cev, Protomodular, Homological and Semi-Abelian Categorie… |
|
|
|
Post #AnsTfLt3CQ8BwmkPVA by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@johncarlosbaez Have we not learned our lesson from rings?!? |
|
|
|
Post #AnsTiu0mmT2SeU3h6O by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@johncarlosbaez Other than this the book is really lovely though; very lucid, a… |
|
|
|
Post #AvLnLSAnicVO2HuqEy by [email protected] |
|
0 likes, 0 repeats |
|
|
|
No matter what you think the performance bottleneck of your proof assistant is,… |
|
|
|
Post #AvLnLSOctDZ2jANsn2 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@pigworker Unfortunately, the floor is low enough that one UNPACK pragma is abl… |
|
|
|
Post #AvLnLUCIC2t2JUd3qK by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@ToucanIan @MartinEscardo @andrejbauer The unifier might have some opinions on … |
