Around 7:30 in the video, we learn about discrete categories, and that a monoid can be considered a discrete monoidal category.
"A category is called discrete when all of its morphisms are identities."
This leaves me a little confused. The morphis…
As far as I know the puzzle doesn't have anything to do with initial F-algebras. I think the type for a list algebra should just be [a] -> a.
@MatthewDoty This contradicts the definition given in the course notes. That's what I'm confused ab…
I'm also a bit confused by the exact terminology used around list algebras. In the course notes we have:
data ListF a x = NilF | ConsF a x
deriving Functor
type List a = Fix (ListF a)
type Algebra f a = f a -> a
type ListAlg a b = Algebra (…
I'm a little confused about how to do this in a way such that the two constructions are strictly inverses of each other (as per 5c). In particular, when I go from the carrier type of the list, X, to the set for the monoid, I had to modify it to be 1…
When I try to use the ListInt type (defined as type ListInt = Fix F), I get errors. The compiler doesn't seem to be able to tell that an F a is also a Fix F.
For example, at the command line, Nil::ListInt gives me:
:82:1: error:
• Couldn't mat…
How do we know that Fix is an initial algebra? As I understand, Lambek's lemma tells us that if it's an initial algebra, then it will be a fixed point (because F(X) is isomorphic to X). But how do we know that the converse is true? Just because some…
At 22 minutes and 7 seconds into the lecture, Brendan holds up a Rubik's cube and says it's a category with one object. And then he demonstrates several rotations and says they are the arrows of the category.
But if rotations are morphisms, then wo…
@PeterJones, I was confused at first by that too, but I think it's making sense to me now.
It seems that part of the idea is that you're supposed to take this very zoomed out abstract view, where you don't care so much about the individual objects …