Commit 2018-08-07 06:43 9b1be732

View on Github →

feat(category_theory): basic definitions (#152)

feat(category_theory): basic definitions
fixing formatting in documentation
corrections from review
removing second ematch attribute on associativity_lemma
being slightly more careful about variables (I don't think there were any actual errors, but I was sometimes using an argument when there was a variable of the same name available.)
fix(notation): transformation components Using @> per @rwbarton's suggestion.
fix(notation): more conventional notation for composition
adjusting namespaces, capitalisation, and headers
move functor/default.lean to functor.lean (Later PRs will add more files to the functor/ directory, but that can wait.)
oops
fixing indentation
namespace for instances
removing unnecessary @> notation for natural transformations
renaming, namespacing, and removing a spurious attribute
better naming, namespaces, and coercions
updating documentation
renaming id
reordering definitions
rfl lemmas for has_one
formatting
formatting
renaming: snake_case
renaming coe rfl lemmas
functoriality -> map_comp
rfl lemmas for identity C and identity F (reducing both to 1)
renaming ext lemma to ext
rename natural_transformation to nat_trans
rename make_lemma to restate_axiom
renaming nat_trans.components to nat_trans.app
oops, fix import
adding doc_comments, and protected
formatting
removing has_one instances, per zulip chat, and adding a vcomp.assoc lemma
removing the attribute that restate_axiom used to add (it was causing a problem on travis, but not locally? anyway it's useless)
fixing names