"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

Follow

category theory 

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

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...

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.