doc(docs/tutorial/category_theory): introductory category theory tutorial (#2104)
* doc(docs/tutorial/category_theory): Adding WIP beginner category theory docs
* linewraps
* presumably uncontroversial edits
* oops
* whitespace
* explaining more about universes
* warning about definitional associativity
* add TODO
* Update docs/tutorial/category_theory/category_theory_intro.md
* rename
* cleanup
* adding lean version
* various
* add a note about debugging universe problems
* rename
* delete old markdown tutorial
* adding sections to make variable names nicer
* tidy up universes
* url escape parentheses inside links
* tweaking text
* Update docs/tutorial/category_theory/intro.lean
Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>