Category Theory May Actually be a Disease

I was just listening to people talking about how much time people spend communicating in text and how little people read, then I started looking again at Categories within the Foundation of Mathematics by Benjamin Horowitz and I realised that although he admits to leaving the idea of a collection undefined, he also leaves the idea of a map undefined, but then he is happy to make assertions about this undefined notion of a map, for example he says "It is important to note that a diagram doesn’t necessarily have to commute unless forced to by the properties of a category (as with the associativity and identity diagrams)." What on earth does he expect that to mean to someone? Then I remembered Steve Awodey's lectures being an unusually comprehensible introduction, so I went back to look at them again and I noticed this comment "Math joke: What do you call a category theorist who reads a paper? A co-author."


See Another Excellent Talk on HoTT by Steve Awodey.

In 2009 Steve Awodey and Andrej Bauer wrote some notes for a course on categorical logic that are still available. If you compare their definition of a category with Horowitz's one above, you see there is actually some superstructure missing, and the theory is like a collection of rafts floating around in the sea and totally out of reach of each other. See The Story of Unix - Chapter Ω: The Captains All Jumped Ship. If we really had even half an idea of what we were trying to do with computers then we would have a decent unifying mathematical framework for practical computer development, but we don't, we just have a chaotic "blooming" of half-arsed ideas that all look like fruitful areas for future research! See David Corfield on Sweedler Theory for Systems. This is because what is good for research is what gets the Principal Investigators the most money.

What is missing is the formal superstructure: syntax. Syntax is easy, because it's entirely formal, and it's great stuff to have as input to computer programs. But everybody is far more concerned about what is actually true, and they think they can talk meaningfully about that without using syntax, which is a terrible, stupid mistake: see John Searle's Chinese Room Argument and Searle on Consciousness.

See Brady Haran interview with Terence Tao. 

Subscribe to p473r.

Coincidentally, Andrej Bauer's LMN online exercise today is mappings (preslikavah) as isomorphisms. Each of these isomorphisms is a pair of morphisms, and each morphism could be a typed lambda expression, as Steve Awodey explains at the start of his lecture above. 


Subscribe to Andrej Bauer.

The channel Category Theory Proofs has a lot of proofs that are very close to those you would do if you were following Steve Awodey's OPLSS 2012 course:



Subscribe to CategoryTheoryProofs.

Comments

Post a Comment

Popular posts from this blog

John Searle's Chinese Room Argument

Image
He's fed up with talking about this. I used to have a copy of the little book he wrote called Minds, Brains & Science. Apparently the AI at Google has read it too and gets it completely: How does stuff like this happen? Most people won't even notice what I'm saying even if I point out that the Google search changed the title. The book was really called Minds, Brains & Science , not Minds, Brains & Programs . (But maybe that was a later edition or something?) I asked Google and it said: John Searle's book Minds, Brains and Science did not become "Minds, Brains & Programs"—rather, they are two separate, distinct works published a few years apart: "Minds, Brains, and Programs" (1980): A landmark academic paper published in the journal Behavioral and Brain Sciences. This is where Searle first introduced his famous Chinese Room Argument to challenge the concept of "strong AI". "Minds, Brains and Science" (1984): A shor...
Read more

Tensor Fields and Simplicial Complexes

Image
Listening to Freya Holmér last night I started to get glimmers of an idea I had long ago about how to represent vector spaces in computational processes using this recursive abstract type :  abstype 'a point = POINT   of {getx :  'a vector,       diff :  'a point -> 'a point,       move :  'a point -> 'a point,       scale : 'a -> 'a point,       proj :  'a point -> 'a} with    fun new i (op +) (op -) (op * ) dot =    let fun self x =  POINT       {getx = x,        move = fn (POINT pr) =>           (self (x + (#getx pr))),        diff = fn (POINT pr) =>          self (x - (#getx pr)),        scale = fn i =>          (self (x * i)),        proj = fn (POINT pr) =>     ...
Read more

FUTO FUBS

Image
I think this is the first time they've actually publicly announced anything about this project. See these posts: Eron Woolf on Why Open Source is Failing Matt Mikhailov and Vincent McKibbon on The Problem with Open Hardware Jason Kridner talking About BeagleBoard.org and Software Development .  See these places:  https://danielc.dev/rk/ https://github.com/petabyt/rk https://github.com/futo-org/ret See also  https://pine64.org/devices/pinebook_pro/ . Subscribe to  FUTO .  See  https://github.com/nir9/low-level-learning-resources/tree/master/setups/debian . Subscribe to  Nir Lichtman .  If you're looking for a cool init process, try  https://ctx.graphics/terminal/ . See  Artful Bytes - When to Use a RTOS  and  How to Create a Successful Open Source Project . 
Read more