Matthew, I'm an imperative languages guy (did some lisp ages ago...) but find itchy that in your enumeration you seem to put Haskellite monads in other shelf than the category-theory ones. I had the vague impression that in Haskell there was more…
Does "may not be" here mean "is forbidden to be" or "is not necessarily"? My impression from the context is the latter but maybe I'm mistaken.
The second: The Identity is monotone and so is its inverse (as it is its own inverse). The example ab…
I think you also want a sort of syntax category, where the morphisms are actual blueprints.
Composition gets a little funky because you need to specify the location and rotation of the second blueprint relative to the first, and because of how inse…
"(Exercise: check that the cardinality of the groupoid of finite sets is e = 2.718281828... If you get stuck, read "week147".)"
Ah! That's why the species of bags (aka finite multisets) is the taylor series of e^x.
Okay, one thing I keep noticing is that in these "richer" "spaces" (especially in CS applications) its often much more natural to define division then subtraction. So I guess I am asking, is there a theory of "division rigs", or "positive fields"?
I wonder what the sort of complex manipulation of sums and products seen in say Real Analysis looks like as string diagrams? Probably you would want some sort of monad to let you skip down a sequence..
The dual of a vector space is space of linear functions from the vector space to the underlying field. For vector spaces of finite dimension they are isomorphic, with the dot product (curried) as the transformation from one to the other.
[ v \in V…
Okay so in Haskell and other compile-time* typed languages each expresion has a type. This lets the compiler catch a lot of problems before the program is run. It turns out that just as you can describe a set theory as a category, you can also do so…
Well I think for a quine to make sense we need a programming language, and the ability to talk about the source in the quine.
So I think a quine and a Godle(sp?) sentence are closely related.
You can construct formulae where it is ambiguous, but that requires a ambiguous refactoring of a product. Which ends up being really obviously ambiguous and weird looking anyway!
Oh man, I was really confused. I thought '2 category' meant what bicategory means, and 'bicategory' what double category actually means.
So this also answers the question I tried to answer in the other thread. The full sub double category of Prof_V…
You know we can actually repair David's functional notation because currying is valid in the category of small V enriched Categories and V enriched functors, and by identifying subsets with their characteristic function, and mapping bool to 0,1 in V…
So I was trying to write up this stuff in a constructive context, but ran into a problem that the naive function for arbitrary joins (which has type (set V -> V)) seems to be uncomputable (for V with infinite elements) to me.
Is there a way to r…
I have been enjoying the course immensely, and feel like I am finally getting my grounding in category theory. I've explored all sorts of advanced topics, but coming back to base has really made me feel like I understand, not just parrot these ideas…