Follow

"The outer rectangle commutes because the inner two squares do." What are you going on about

category theory 

Oh I see. If the insides commute, then you can move the outside lines inwards until they meet, and because composition is associative you can rearrange the parentheses however you like

category theory 

Naturality is like, equating the lines from one point to another

category theory 

If your arrows between A and B is an equality between A and B, then naturality is equality of the equalities

category theory 

That's what HoTT is going on about with those diagrams

category theory 

Or no wait. The arrows were functions and naturality was equality of... well I forget

@ionchy the outer rectangle carpools with the inner two squares, so they commute at the same time

category theory 

@ionchy reading these as someone who learned category theory long ago and then forgot it feels a little weird. I'm suddenly compelled to dive into the pool of abstract nonsense again...

@hazel I've reached a diagram claiming that the composition of two natural transformations is also natural

@ionchy lmao I don't think this book even talks about natural transformations

Sign in to participate in the conversation
types.pl

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.