This was great! Bringing some formality to the social sciences is a topic that is near and dear to me. I hope that the presentations given at the Mathematics for Governance Design event will be made available to the public. In the meantime I have some papers to read. :) Well done, and totally fascinating.
Extremely interesting video especially in researching my "autobiography" from the FORTRAN and punch card days in the 1970's to exploration of Haskell and Lean in the 2020's
11:40 2 Introductory resources used; 12:30 Insights from wiring diagrams; 15:06 3 more in-depth resources used (includes "7 sketches of ACT" by Brendan Fong & David Spivak I am also using.) I would recommend adding the lens based ideas in "Categorical Systems Theory" used by David Jaz Myers, since the presenter was interested in expanding the compositionality of wiring diagrams. In particular, to define new composition operators for nesting at 22:26 and then explaining a use case for safety and security at 25:24 as the right modularity (or getting modularity right) to operate within the safe parameters set by an outer diagram; a potential use case for lens composition. David also has an intro lecture into lens composition on youtube at ru-vid.com/video/%D0%B2%D0%B8%D0%B4%D0%B5%D0%BE-qywgbGrtJSo.html.
The beauty of category theory(!) is that $5 * $3 CAN make sense: - In fact, I came up with a way of multiplying in the dollar category A: $5 by $3 exactly the same way as you would in the quantity category B: 5 boxes by 20 widgets. These can be seen as isomorphic transformations, each resulting in a categorical product. How? First, they both have the SAME kind of constraint: You need to know how one quantity translates into the other. Moreover, there IS a functor between the two transformations going from B to A. In category B, you would get 5 boxes x 20 widgets = 100 ONLY if EACH box is the same size and a full box contains 20 widgets. However, the real result is actually a product (5 boxes, 100 widgets) not a just a number or scalar. The same way, for US$ 5 x CAN$ 3 to work in category A, you need to know how much Canadian dollar goes into 1 US dollar. But you can get US$5 x CAN$3 even if US$1 is worth more or less than CAN$ 3. That's the beauty of this categorical product. Similarly, if one full box contains less or more than 20 widgets, 5 boxes x 20 widgets no longer equals 100. But as a product it still makes sense. Suppose now that we set the constraint for category B that each box must go to a different address and 1 box fits 25 widgets, meaning with 20 a box will be 0.2 empty and only 0.8 full. Then, if you set the same rule of equal distribution into each box as you have equal exchange into each unit for currencies, you get 5 boxes x 20 widgets = (5x0.8b, 100w) as a product. You can translate this to (4b, 100w) ONLY of you are happy to leave 1 box empty, ship only 4 boxes and make one of the 5 recipients unhappy because they receive nothing of the widgets. More generally and thinking categorically, the T: $ x $ product is a discreet matrix or continuous field (consider a fractional exchange rate) of monetary assets along two different dimensions. They can be two arbitrary but convertible currencies, or two different persons using the same currency, etc. Thus a Category where objects are $^2 can describe a series of valuations, exchanges and transactions not just by adding or multiplying like 3 x $5 or $3 = $5 as in the accounting books referred by David at 10:00, but along two different dimensions describing a network of transactions that may even include loops or other basins as in some regularly occurring circular exchange, for example.
after watching the polynomial morphisms section like 10 times over several days and thinking about it in between I think I understood it! if we interpret elements of the polynomial as functions, then the downwards arrows are just the domain morphisms, which maps a function to its domain. the pullback is defined by the family of *Q'_{f_0(a)}* which will point to `a` in `P_0`. Each function `g_f : a -> r` in *Q'_f* is defined by a corresponding `g : f_0(a) -> r` in *Q'*. The rightward morphism in the pullback is just applying this definition. the main confusion that remains is what category the commuting diagram is in, where both sets of arrows and sets of dots are objects? How can both `P_0` and `P'` be objects in the same category?
This is great; thanks Spencer! I just wanted to mention a typo at 25:06, where the combinatorial should say 12-->4, because there was a slight mistake in the computation on the right.
Interesting. There is a common intuition that a UI provides a specific language, a visual language. I wonder if a similar approach to categories and polynomials might serve to characterize other visual languages, and reductively some spoken or written languages or notations. In particular, I am thinking about sign language, where there are a number of parallel carriers of information (Dominant and Nondominant handshapes, their movement, a signing space, and a collection of distinctive facial expressions that play a syntactic or phonemic role (other facial expressions are more prosodic, like intonation rather than like phonemes or morphemes). I am thinking that individual lexical signs are polynomials, carrying some kind of lexical content. Functional morphemes may be functors on signs.
thank you for clarifying the question about how paths that end up in the same place could still not commute - I've always had a litle trouble keeping track of what the "objects" are in a category, I keep forgetting that an object can be a set of things etc. this one diagram that you drew cleared up a LOT of confusion!
I thought the point about new users not knowing how to search matched my experience as a new user of F* and Liquid Haskell very well. There is a lot of things in the standard library, and also some things that are just not there, and it was hard to tell the difference or figure out if I really was looking in the right place. (I think the problem is a bit different in Lean which has a more mature standard library, though.)
11:07 "the trade-off between memory versus perception" ... :"humans have really bad memories": Another way to look at things is that humans are really efficient at pruning what they don't find relevant. Forgetting is a major principle of structuring cognition and memory, as much as the countervailing principle of retaining. We can also look beyond the percept to the external world which gives structure to the percept. We can even consider a theory of extended mind, that incorporates the world into cognitive states. I wouldn't necessarily go that far, but I do think an individual mind instantiates some social type context of shared lexicalized concepts. What structures that schema of lexicalized concepts (or in math, notationalized concepts) is sometimes the objective world, but sometimes also social institutions and culture. This is something that LLM-based AI doesn't have, making its outputs and hallucinations opaque to conceptual inquiry or ethical accountability.
Great Talk! Will is a great teacher/communicator, and clearly very skilled! I read his paper, "A new era of systems programming with Rust" at least once per month to recenter my thinking. Thank you for this paper Will.
The transcript provided is a conversation between David Berlekamp, Michael Francis and Daniel Calegari discussing the concepts of algebraic theories in type theory for mathematics. 1) **David** starts by introducing an analogy with categories to explain why they are important. He says that categorical structures like topologies (where points can be assigned types from a set T into another category S, typically called SetCat or TopoCats), and finite limits of these cat subcategories under filtered colimits in CSubs make up the mathematical language for algebraic theories. 2) **David** then introduces "types" as an abstraction that captures essential properties like identity types (a pair with two elements: one being equal to another). The type theory he describes is very much dependent on context, allowing structures and formulas only valid within specific contexts. This distinction between pure syntax vs semantics helps clarify the limitations of algebraic theories. 3) **David** explains how these categories can be constructed using a technique called "conversion" from category notation (where objects are labeled with types in one direction followed by morphisms that relate those two labels and so forth, similar to ordinary programming languages like Java or Python)) into type-theoretical context-sensitive language. 4) **David** uses an example of the CategoryTheory toolbox for TypeScript's syntax tree representation as a way how he constructs categories. He also mentions some advanced features such "recursive pattern matching" and basic functionalities, all within this specific setting to demonstrate its applicability in constructing category-like structures out-of-the-box. 5) **David** closes by comparing the type theory of algebraic theories with other formal languages that use types but differ significantly: he discusses how TypeScript's syntax can be interpreted as a framework for dependent typed functional programming, which includes terms and substitutions within contexts. He concludes his talk saying there is more work to do on this topic. 6) **Michael** comments about the simplicity of algebraic theories in general (a single type theory with no arbitrary structure at all), but emphasizes that categorical structures like TopoCats are quite useful when one wants a formal framework for mathematics or computer science. He also refers back briefly to David's analogy between categories and topologies, showing how mathematical concepts can be naturally encoded using category-theoretic language. The conversation is rich with examples of type theory constructs (types as abstract sets/morphisms in certain context) being used within this particular setting like constructing the CategoryCats toolbox or interpreting a TypeScript syntax tree. The discussion touches on various aspects such linguistic nuances, mathematical properties and how these concepts can be formalized using programming languages that encapsulate type theory. Overall it demonstrates why category-theoretic language has found its place in modern mathematics as an expressive yet powerful system for describing abstract structures like topologies or algebra models.
hey nice talk! one way to view the failure of topological spaces to be algebraic is as a problem of variance: the *opposite* of the category of topological spaces is a quasivariety, and thus locally finitely presentable
@@cbaberle not much more. I can point you to this paper arXiv:2404.05017 which gives a survey of some similar results for other topologically-flavored categories. a quasivariety is a full subcategory of a variety (variety = category monadic over Set) closed under subobjects and products, or equivalently, a quasivariety is the category of models of a conditional equations (aka Horn clauses with equations).
Oh hey, that's me! One quick correction to something I said in the talk: if you view the theory of elementary topoi equipped with a topological space as a category fibred over (the category given by the theory of) elementary topoi, the fibre of the topos Set isn't quite the usual category of topological spaces and continuous maps - instead, it's the category of topological spaces and *open* maps. So you need to do a little more work to get out the category of topological spaces and continuous maps, although it is still possible. This is closely related to Owen's point later in the talk about getting the 2-category of topoi and geometric morphisms out of this sort of setup (inasmuch as geometric morphisms are the topos-theoretic analogue of continuous maps).
@@KevinCarlson-k7d I still need to work out the example of topological spaces a bit more carefully, but here's one that definitely does work - the Grothendieck construction of the fibration T : topos |-> cocomplete distributive lattices (aka frames) in T *is* locally finitely presentable, and the fibrewise opposite of this fibration is T : topos |-> locales in T, into which T : topos |-> spaces in T embeds as the full subcategory of spatial locales.
@@cbaberle somewhat, but there's this issue about lfp fibrations not necessarily having lfp fibers too. OK, well, that begs [us to ask] the question: is the category of topological spaces in Set and open maps itself lfp? I'd guess not but I have no idea off the top of my head.
She’s one of the clearest explainers in category theory I know of. I’ll have to come back to this to watch more. I’m right at the level where I can sort of get an idea about Lawvere theories from a video like this. They’re very related to some questions I’ve had.
The progression of models thru grade levels seems quasi exponential. Which begs questions of how long before there is an AI better than the best human subject matter experts. Can an LLM produce greater than x level students performance given a training corpus of x-1 level students knowledge? My intuition here is we hit a point soon where LLMS can reason slightly above the highest human level at which point knew knowledge enters a shared corpus. AI makes new knowledge, which makes both experts and subsequent AIs better. I'm new to category theory, but in some sense I think this is a mapping of categories into another. Is there a functor that moves from categories of smaller knowledge to those of greater knowledge? Clearly there is a way from less knowledge to more. The question then becomes at what level do really large LLMs diverge from max_existing(x) level students knowledge. Also at one point does the energy consumption to train one of these models exceed the cost of training, for example, a class of students measured in currency C.
I'm working thru "An Invitation to Applied Category Theory", and I would certainly try to read the "The Universal Librarian" if it existed. Because I am not a professional mathematician that speaks the many languages of math, studying the linguistics of those languages feels like a shortcut to learning more than one at a time.
At about 24:50 he shows four different queries, but they aren't doing the same thing. In the file system example we take one pass over all files, extract calculator and system, and create a list of simulators for each (calculator, system) pairs. If there are two matching simulations, they each appear in the list once. This seems the closest to what was asked for -- we partitioned the simulations by calculator and cell. In all the other examples we're returning a set of pairs that have equal calculator and cell, but if (a,b) match then in the Python and SQL versions we return both (b,a) and (a,b). I think the Algebraic Julia code will do this as well. If there's an arrow s1->a and s2->b then there should also be an arrow s1->b and s2->a. Monic just ensures we don't get a=b. To me this looks like we have two different sets of semantics at work, and the three on the right all seem buggy? Why do I want every pair returned twice? Isn't the left-hand much more useful because the matching experiments are grouped by the key, instead of just a list of matching pairs?
it's also a shame that a lot of the formalization work is split across other projects and programming languages. Having to build the library from scratch is tedious... There should be some common format/standard that all other projects can use and re-use.
