Category Theory Using String Diagrams

Understand

In work of Fokkinga and Meertens a calculational approach to category theory is developed.

• The scheme has many merits, but sacrifices useful type information in the move to an equational style of reasoning.
• By contrast, traditional proofs by diagram pasting retain the vital type information, but poorly express the reasoning and development of categorical proofs.
• In order to combine the strengths of these two perspectives, we propose the use of string diagrams, common folklore in the category theory community, allowing us to retain the type information whilst pursuing a calculational form of proof.