feat(category_theory): basic definitions #152

semorrison · 2018-06-04T03:39:38Z

This is just the start of a PR of my category theory library.

I'm very happy to add components to this PR if it is easier to see more things in context.

I am not attached at all to any of the notational choices, and am quite happy to change these. (I do really want to keep a notation like the current f ≫ g for "do f, then g", but don't mind the symbol.)

semorrison · 2018-06-04T03:51:14Z

A note: the category theory library I have been developing relies heavily on automation, in particular my tidy and rewrite_search tactics. This PR has all that automation stripped out, so we can focus on just getting the basics right, but I intend to get all that automation mathlib-ready soon.

As an example of how much nicer things look with this automation, have a look at the before/after for this file in which I show that category of types has products, coproducts, equalizers, and coequalizers (to appear in a later PR).

jcommelin

Mostly trivial comments. I can't really comment on the Lean.

jcommelin · 2018-06-04T06:34:55Z

category_theory/functor/default.lean

+variable {C : Type u₁}
+variable [category.{u₁ v₁} C]
+
+@[simp] lemma IdentityFunctor.onObjects   {C : Type u₁} [category.{u₁ v₁} C] (X : C)                 : (IdentityFunctor C) +> X = X := by refl


The colon doesn't algin with the line below, but it looks like you want it to.

It seems there are duplicate variables {C : Type u₁} [category.{u₁ v₁} C] here?

... and below here, as well.

I couldn't get it to align exactly (slight variations in character widths), so I've removed all the spurious spaces.

@spl, I don't think there was any actual duplication, because of sectioning commands, but in any case I've tidied the variables up.

jcommelin · 2018-06-04T06:38:27Z

category_theory/natural_transformation.lean

+
+@[simp,ematch] lemma vertical_composition_of_NaturalTransformations.components (α : F ⟹ G) (β : G ⟹ H) (X : C) : (α ⊟ β).components X = (α.components X) ≫ (β.components X) := by refl
+
+-- We'll want to be able to prove that two natural transformations are equal if they are componentwise equal.


It seems like this is an intermezzo between vertical and horizontal composition of natural transformations. Is that on purpose?

No, it wasn't on purpose; I've rearranged now.

jcommelin · 2018-06-04T06:42:31Z

docs/theories/categories.md

+### Categories
+
+We use the `⟶` (`\hom`) arrow to denote sets of morphisms, as in `X ⟶ Y`.
+This leaves the actual category implicit; it is inferred from the type of X and Y but typeclass inference.


s/but/by/ -- "by typeclass inference".

jcommelin · 2018-06-04T06:43:53Z

category_theory/category.lean

+  (right_identity : ∀ {X Y : Obj} (f : Hom X Y), compose f (identity Y) = f . obviously)
+  (associativity  : ∀ {W X Y Z : Obj} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z), compose (compose f g) h = compose f (compose g h) . obviously)
+
+notation `𝟙` := category.identity     -- type as \b1


I can imagine that we will also love to have this notation for the unit object in a monoidal category. But then... we also want good notation for identity morphisms, and I don't have a good alternative in mind.

Besides the double-struck 1, there are several other variant numeral 1s available in unicode:

"bold": 𝟏
"sans-serif": 𝟣
"sans-serif bold": 𝟭
"monospace": 𝟷

Currently none of these have shortcuts in VSCode, but those are easy to add. My monoidal categories library hasn't fixed on any notation for monoidal units. I'm not sure that having two slightly different 1s is a good idea.

jcommelin · 2018-06-04T06:45:47Z

docs/theories/categories.md

+We use `𝟙` (`\b1`) to denote identity morphisms, as in `𝟙 X`.
+
+We use `≫` (`\gg`) to denote composition of morphisms, as in `f ≫ g`, which means "`f` followed by `g`".
+This is the opposite order than the usual convention (which is lame).  


Mathematicians are going to love you for this [/sarcasm]. Is it possible to also have notation for "ordinary" composition? Would it even be possible to overload \circ? Or will madness ensue? If so, then preferably something that reminds of \circ.

I will investigate overloading \circ, or finding something nearby.

I'd been hoping that everyone would be relieved that starting to write mathematics in Lean gave them a good opportunity to abandon the no-good-terrible-horrible \circ notation after so many years. :-)

Regardless of one's personal preferences, for the purpose of formalizing existing mathematics, it's greatly helpful if the Lean notation is as similar as possible to the source notation; and that will almost always require having some form of applicative-order composition notation available.

In my own project, I just write local notation f ` ∘ `:80 g:80 := g ≫ f at the top of most files, and this works pretty well for me, though I occasionally need to write function.comp for the usual ∘ operator. Not a very good solution for the library, though.

jcommelin · 2018-06-04T06:47:22Z

docs/theories/categories.md

+
+For now we just write out `τ.components X`.
+
+For vertical and horiztonal composition of natural transformations we "cutely" use `⊟` (`\boxminus`) and `◫` (currently untypeable, but we could ask for `\boxbar`).


Or maybe \boxvert(?), which arguably has better mnemonics.

Good suggestion, I've included that.

semorrison

Originally I thought it was inappropriate to put @[simp] on associativity, but it seems to work out okay.

Removing it here entirely changes some proofs; in some places we need to do rewrites (which can nevertheless be discovered automatically) instead of just simp,

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

rwbarton · 2018-06-12T14:21:14Z

I noticed that the composition notation ≫ (or in my case, ∘) binds tighter than functor application (to morphisms) &>. This feels backwards to me, as I'd like to pretend &> is really function application and isn't there at all, and so it should have the highest binding power, like function application. I'm thinking of F &> f ∘ g as corresponding to math F f ∘ g which means (F f) ∘ g, not F (f ∘ g).

rwbarton · 2018-06-12T14:26:30Z

I've recently been working with categories presented by graphs and relations, and I noticed your full category theory library also defines graph and graph_homomorphism types. Have you considered making graph be a class which contains only the Hom field, and having category extend it, and similarly Functor extend graph_homomorphism? This seems like it would be helpful when discussing the free/forgetful adjunction between categories and graphs, just to avoid some explicit graph_homomorphism_of_functor boilerplate. I haven't actually tried redefining category like this, though.

rwbarton · 2018-06-12T18:55:07Z

Some notation for the components of a natural transformation is necessary. I've been using

notation t ` @> `:90 X:90 := t.components X

@rwbarton

Using `@>` per @rwbarton's suggestion.

semorrison · 2018-06-15T07:13:24Z

@rwbarton, I've added @> for components of natural transformations.

How about we use ⊚ for the conventional order composition? It's easy to type as \oo, and looks similar enough to the usual operator to be unambiguous? (I've include this in the latest commit.)

semorrison · 2018-06-15T07:17:17Z

@rwbarton, I did try having category extend graph at some point, and from memory it worked, but decided:

sometimes you had to refer to graph.Hom when you really were talking about the Hom for a category, and this felt weird and awkward
It's weird to talk about the Homs of a graph.

Even though logically an extension works fine here, I don't think it's giving you much, and it's conceptually unclear. Given the fairly narrow payoff (i.e. only inside a file or two where we develop that adjunction between categories and graphs) I didn't like it.

rwbarton · 2018-06-15T20:31:50Z

@semorrison, regarding category and graph, that makes sense. Perhaps it would be nice if one could rename the fields of a parent structure when extending...

semorrison · 2018-06-20T21:58:09Z

Does anyone have more review comments? As far as I'm aware, this is ready to go.

The travis failure is just due to a timeout (which on bad days mathlib is running up against), and as far as I can see does not indicate a problem with this PR.

jcommelin · 2018-06-21T07:13:40Z

There is not even a travis failure on your last commit, right?

semorrison · 2018-06-21T08:56:01Z

You're right --- merging in master prompted travis to rebuild, and succeed this time.

johoelzl

Should we really break with the naming conventions we have in Lean? I especially don't like onObjects and onMorphisms. But I would prefer if most names are a lower case with _.

johoelzl · 2018-07-02T10:00:50Z

category_theory/category.lean

+import tactic.make_lemma
+import tactic.interactive
+
+namespace categories


what about category_theory instead?

johoelzl · 2018-07-02T10:05:10Z

category_theory/category.lean

@@ -0,0 +1,44 @@
+-- Copyright (c) 2017 Scott Morrison. All rights reserved.


The header we use look like:

/- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura notation, basic datatypes and type classes -/

so use /--/ instead of --. The difference looks minor, but might be helpful when we use scripts to analyze the header.

johoelzl · 2018-07-02T10:09:23Z

category_theory/functor/default.lean

+
+open categories
+
+namespace categories.functor


I think everything should went into category_theory.

johoelzl · 2018-07-02T10:09:45Z

category_theory/functor/default.lean

+structure Functor (C : Type u₁) [category.{u₁ v₁} C] (D : Type u₂) [category.{u₂ v₂} D] : Type (max u₁ v₁ u₂ v₂) :=
+  (onObjects     : C → D)
+  (onMorphisms   : Π {X Y : C}, (X ⟶ Y) → ((onObjects X) ⟶ (onObjects Y)))
+  (identities    : ∀ (X : C), onMorphisms (𝟙 X) = 𝟙 (onObjects X) . obviously)


Now you have categories.functor.Functor, I think it should be just category_theory.functor.

Thanks @johoelzl, I've made all the changes you suggested. I'm very happy to adjust naming to match mathlib conventions better, although would like to err on the side of longer names over ambiguous or not-immediately-obvious ones, where reasonable.

johoelzl · 2018-07-09T16:45:55Z

Further review:

For category: identity -> id, compose -> comp, left_identity: id_comp, right_identity: comp_id, associativity -> comp_assoc.
Why is functor in its own directory?
Identation: we don't add identation when listing the fields of a structure, i.e. for category, Functor, and NaturalTransformation the list of fields in the structure definition are not indented.
While the structures and most theorems should be just in the category_theory namespace, especially the instances should be in the namespace of the corresponding structure: Functor.has_one and NaturalTransformation.has_one
I'm not sure about the best names for functor fields. on_objects -> obj, on_morphisms -> map, identities -> map_id, functoriality -> map_comp
should we really introduce all these infix operators for application?
"Unfortunately, while we'd like to write components of natural transformations via function application (e.g. τ X), this requires coercions to function types, which I don't like." I would prefer the coercion to functions. I don't think this comment should be in the documentation, also you should explain why you don't like it. Why do you force us to use all these strange symbols for applications ;)

(Later PRs will add more files to the functor/ directory, but that can wait.)

semorrison · 2018-07-27T04:28:36Z

Some simple things:

Why is functor in its own directory?
-- I've moved this back: later PRs will add lots of stuff to the functor/ directory, but we can deal with moving it later.
Identation: we don't add identation when listing the fields of a structure, i.e. for category, Functor, and NaturalTransformation the list of fields in the structure definition are not indented.
-- Fixed.
While the structures and most theorems should be just in the category_theory namespace, especially the instances should be in the namespace of the corresponding structure: Functor.has_one and NaturalTransformation.has_one
-- Fixed.

johoelzl · 2018-07-31T06:54:42Z

I still don't like the syntax:

there are 2 morphism composition symbols. I think there should be only one, if users want another one they can add them using local infix
Functors should define a coercion for the object map, and F.map for the morphism map.
the names for NaturalTransformation are very long, I think most of them should be just in the NaturalTransformation namespace, and instead of vertical_composition and horizontal_composition we have vcomp and hcomp

…category_theory

digama0 · 2018-08-07T04:43:55Z

category_theory/functor.lean

+(obj           : C → D)
+(map           : Π {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y)))
+(map_id        : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
+(functoriality : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = (map f) ≫ (map g) . obviously)


I think I will insist on this one. I know that literal description of axioms doesn't appeal to you, but there are just too many different ways of phrasing lemmas and it is a huge benefit to users that are bouncing between fields of mathematics that they may not know in detail the "traditional" way, to be able to guess names based solely on how they are written rather than what they mean. As a simple example, the symmetric version of this equality would also be called "functoriality" by a mathematician, as well as a hypothetical definition like commutes map (≫) which unfolds to this equality. You have map and comp being applied; so it is called map_comp.

digama0 · 2018-08-07T04:45:48Z

category_theory/functor.lean

+{ F   := λ F, C → D,
+  coe := λ F, F.obj }
+
+@[simp] lemma unfold_obj_coercion (F : C ↝ D) (X : C) : F X = F.obj X := rfl


I would prefer a name like coe_def for this.

digama0 · 2018-08-07T04:47:29Z

category_theory/functor.lean

+@[simp] lemma identity.on_objects (X : C) : (identity C) X = X := rfl
+@[simp] lemma identity.on_morphisms {X Y : C} (f : X ⟶ Y) : (identity C).map f = f := rfl
+@[simp] lemma has_one.on_objects (X : C) : (1 : C ↝ C) X = X := rfl
+@[simp] lemma has_one.on_morphisms {X Y : C} (f : X ⟶ Y) : (1 : C ↝ C).map f = f := rfl


Do we need both of these? I would prefer to have identity simplify to 1 so that we only need the second set of lemmas. Unless you are having similar problems as with simp under coe, but I don't think this should happen.

My inclination is to actually remove entirely the has_one instances. I think they're more cosmetic than useful. What do you think?

What is the relation between this identity and the \b1 symbol? I would like to have some kind of symbol for this which is one-like. But it doesn't hurt to have a has_one instance as well; just pick one or the other to be the "idiomatic" one and use it in all your statements, and have a simp lemma from any alternative ways to write it.

Ah, I missed this comment. identity is an "outside" identity, that is C.identity is the identity functor from C to itself. id (and the \b1 symbol) are for the identities "inside" a category, e.g. category.id X is a morphism from the object X to itself.

I agree it would be nice to be clearer here. Suggestions for renamings very welcome!

How about functor.id (protected)? I can live with C.id as a notation, does that work for you?

Edit: oh wait, C is a category not a functor. I can still live with functor.id C, unless there is a good reason to further abbreviate it.

semorrison · 2018-08-07T05:01:00Z

My inclination is to actually remove entirely the `has_one` instances. I think they're more cosmetic than useful. What do you think?

…

On Tue, Aug 7, 2018 at 2:47 PM Mario Carneiro ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In category_theory/functor.lean <#152 (comment)>: > + +definition identity : C ↝ C := +{ obj := λ X, X, + map := λ _ _ f, f, + map_id := begin /- `obviously'` says: -/ intros, refl end, + functoriality := begin /- `obviously'` says: -/ intros, refl end } + +instance has_one : has_one (C ↝ C) := +{ one := identity C } + +variable {C} + ***@***.*** lemma identity.on_objects (X : C) : (identity C) X = X := rfl ***@***.*** lemma identity.on_morphisms {X Y : C} (f : X ⟶ Y) : (identity C).map f = f := rfl ***@***.*** lemma has_one.on_objects (X : C) : (1 : C ↝ C) X = X := rfl ***@***.*** lemma has_one.on_morphisms {X Y : C} (f : X ⟶ Y) : (1 : C ↝ C).map f = f := rfl Do we need both of these? I would prefer to have identity simplify to 1 so that we only need the second set of lemmas. Unless you are having similar problems as with simp under coe, but I don't think this should happen. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#152 (review)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAdLBH11DTk66mfR6UlBDBAwzyvvJkV5ks5uORvjgaJpZM4UYZ19> .

semorrison · 2018-08-07T05:03:08Z

I have made the renamings you suggested. (The `functoriality` -> `map_comp` renaming only under protest! :-)

…

On Tue, Aug 7, 2018 at 3:00 PM Scott Morrison ***@***.***> wrote: My inclination is to actually remove entirely the `has_one` instances. I think they're more cosmetic than useful. What do you think? On Tue, Aug 7, 2018 at 2:47 PM Mario Carneiro ***@***.***> wrote: > ***@***.**** commented on this pull request. > ------------------------------ > > In category_theory/functor.lean > <#152 (comment)>: > > > + > +definition identity : C ↝ C := > +{ obj := λ X, X, > + map := λ _ _ f, f, > + map_id := begin /- `obviously'` says: -/ intros, refl end, > + functoriality := begin /- `obviously'` says: -/ intros, refl end } > + > +instance has_one : has_one (C ↝ C) := > +{ one := identity C } > + > +variable {C} > + > ***@***.*** lemma identity.on_objects (X : C) : (identity C) X = X := rfl > ***@***.*** lemma identity.on_morphisms {X Y : C} (f : X ⟶ Y) : (identity C).map f = f := rfl > ***@***.*** lemma has_one.on_objects (X : C) : (1 : C ↝ C) X = X := rfl > ***@***.*** lemma has_one.on_morphisms {X Y : C} (f : X ⟶ Y) : (1 : C ↝ C).map f = f := rfl > > Do we need both of these? I would prefer to have identity simplify to 1 > so that we only need the second set of lemmas. Unless you are having > similar problems as with simp under coe, but I don't think this should > happen. > > — > You are receiving this because you were mentioned. > Reply to this email directly, view it on GitHub > <#152 (review)>, > or mute the thread > <https://github.com/notifications/unsubscribe-auth/AAdLBH11DTk66mfR6UlBDBAwzyvvJkV5ks5uORvjgaJpZM4UYZ19> > . >

digama0

It's looking good. I think we are nearly there, just a few more nitpicks and then it will be ready.

digama0 · 2018-08-07T04:57:26Z

category_theory/natural_transformation.lean

+
+structure natural_transformation (F G : C ↝ D) : Type (max u₁ v₂) :=
+(components : Π X : C, (F X) ⟶ (G X))
+(naturality : ∀ {X Y : C} (f : X ⟶ Y), (F.map f) ≫ (components Y) = (components X) ≫ (G.map f) . obviously)


Could we perhaps abbreviate these names? components will appear a lot so I would suggest something with 3-5 characters, and natural_transformation could be abbreviated to nat_trans without much loss in readability. @johoelzl Thoughts? I don't even think it has to be an abbreviation of the word "components", something like f or app would work fine.

Okay, nat_trans coming up. I really don't understand the desire to abbreviate. Once upon a time memory was expensive, but it's not anymore, and code is so much more readable if you use unambiguous english words, particularly the explicit mathematical terms everyone is used to.

I've renamed components to app, though it makes me feel sick to obfuscate my code. :-)

When I'm staring at a 30 line goal, long names make everything harder to look at. Lean already has significant term bloat, so I try to control what I can. Symbols are especially good at making things concise and readable, but they generally aren't an option when writing proofs. The names of major concepts have to be especially short because they appear as components in theorem names, and when you use a "name the symbols" approach to theorem naming those names can get long and repetitive, so short components pay for themselves.

I notice that this definition does not have a doc comment. I would much prefer you add all explanatory information to a doc comment rather than giving everything a long name.

Okay! doc comments coming up.

digama0 · 2018-08-07T04:57:49Z

category_theory/natural_transformation.lean

+variables {F G H : C ↝ D}
+
+-- We'll want to be able to prove that two natural transformations are equal if they are componentwise equal.
+@[extensionality] lemma componentwise_equal (α β : F ⟹ G) (w : ∀ X : C, α X = β X) : α = β :=


this theorem should be called ext

digama0 · 2018-08-07T05:04:16Z

tactic/make_lemma.lean

+
+/- Make lemma takes a structure field, and makes a new, definitionally simplified copy of it, appending `_lemma` to the name.
+   The main application is to provide clean versions of structure fields that have been tagged with an auto_param. -/
+meta def make_lemma (d : declaration) (new_name : name) : tactic unit :=


The name of this tactic is extremely generic. How about mk_structure_lemma or restate_axiom?

Done: restate_axiom.

digama0 · 2018-08-07T05:31:58Z

category_theory/category.lean

-make_lemma category.assoc
+restate_axiom category.id_comp
+restate_axiom category.comp_id
+restate_axiom category.assoc


missed a spot (make_lemma)

digama0 · 2018-08-07T06:57:10Z

category_theory/functor.lean

-@[simp] lemma has_one.on_objects (X : C) : (1 : C ↝ C) X = X := rfl
-@[simp] lemma has_one.on_morphisms {X Y : C} (f : X ⟶ Y) : (1 : C ↝ C).map f = f := rfl
+@[simp] protected lemma has_one.on_objects (X : C) : (1 : C ↝ C) X = X := rfl
+@[simp] protected lemma has_one.on_morphisms {X Y : C} (f : X ⟶ Y) : (1 : C ↝ C).map f = f := rfl


these don't all need to be protected, just id itself (assuming you call it id ;) )

So we don't have the option of calling it id, as there's already a structure field category.id, for the identity morphism on an object. This identity is for the identity functor on the category itself.

…oc` lemma

(it was causing a problem on travis, but not locally? anyway it's useless)

digama0 · 2018-08-07T09:44:59Z

category_theory/functor.lean

+variable {C}
+
+@[simp] lemma id.on_objects (X : C) : (functor.id C) X = X := rfl
+@[simp] lemma id.on_morphisms {X Y : C} (f : X ⟶ Y) : (functor.id C).map f = f := rfl


these should be named id_obj and id_map to match the new functor names, same with comp and vcomp, hcomp

Fixed, thanks!

digama0 · 2018-08-07T09:46:52Z

category_theory/natural_transformation.lean

+{ app        := λ X, 𝟙 (F X),
+  naturality := begin /- `obviously'` says: -/ intros, dsimp, simp end }
+
+@[simp] lemma id.app (F : C ↝ D) (X : C) : (nat_trans.id F) X = 𝟙 (F X) := rfl


we usually use _ instead of . for theorems referring to a definition unless it makes sense with projection notation

feat(category_theory): basic definitions

933f4a0

fixing formatting in documentation

46e694c

jcommelin reviewed Jun 4, 2018

View reviewed changes

semorrison added 2 commits June 4, 2018 17:55

corrections from review

88dd1f0

removing second ematch attribute on associativity_lemma

4341b14

semorrison commented Jun 4, 2018

View reviewed changes

being slightly more careful about variables

26dde34

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

semorrison added 2 commits June 15, 2018 17:00

fix(notation): transformation components

062d55f

Using `@>` per @rwbarton's suggestion.

fix(notation): more conventional notation for composition

456594a

Merge branch 'master' into category_theory

eb4dc51

johoelzl reviewed Jul 2, 2018

View reviewed changes

adjusting namespaces, capitalisation, and headers

efe51ee

Scott Morrison added 3 commits July 27, 2018 14:20

move functor/default.lean to functor.lean

fff0238

(Later PRs will add more files to the functor/ directory, but that can wait.)

oops

ce7194d

fixing indentation

c46e78b

Scott Morrison added 2 commits July 27, 2018 14:28

namespace for instances

0205498

removing unnecessary @> notation for natural transformations

e2d0ca4

Scott Morrison added 5 commits August 7, 2018 13:22

Merge branch 'category_theory' of github.com:semorrison/mathlib into …

c030b8d

…category_theory

rfl lemmas for has_one

2b4621d

formatting

433aae7

formatting

52ed9b7

renaming: snake_case

ac4b311

digama0 reviewed Aug 7, 2018

View reviewed changes

renaming coe rfl lemmas

c3984f0

functoriality -> map_comp

b68bc6e

rfl lemmas for identity C and identity F (reducing both to 1)

8f59e1a

digama0 reviewed Aug 7, 2018

View reviewed changes

Scott Morrison added 5 commits August 7, 2018 15:07

renaming ext lemma to ext

d23e348

rename natural_transformation to nat_trans

e29fda0

rename make_lemma to restate_axiom

b832f05

renaming nat_trans.components to nat_trans.app

cb93d51

oops, fix import

eaac4c0

digama0 reviewed Aug 7, 2018

View reviewed changes

Scott Morrison added 2 commits August 7, 2018 16:12

adding doc_comments, and protected

1ce8b0a

formatting

14ba452

digama0 reviewed Aug 7, 2018

View reviewed changes

Scott Morrison and others added 2 commits August 7, 2018 17:47

removing has_one instances, per zulip chat, and adding a `vcomp.ass…

18db512

…oc` lemma

removing the attribute that restate_axiom used to add

3aa69cb

(it was causing a problem on travis, but not locally? anyway it's useless)

digama0 reviewed Aug 7, 2018

View reviewed changes

fixing names

569241e

digama0 merged commit 9b1be73 into leanprover-community:master Aug 7, 2018

semorrison deleted the category_theory branch August 7, 2018 19:58


		@[simp,ematch] lemma vertical_composition_of_NaturalTransformations.components (α : F ⟹ G) (β : G ⟹ H) (X : C) : (α ⊟ β).components X = (α.components X) ≫ (β.components X) := by refl

		-- We'll want to be able to prove that two natural transformations are equal if they are componentwise equal.


		For now we just write out `τ.components X`.

		For vertical and horiztonal composition of natural transformations we "cutely" use `⊟` (`\boxminus`) and `◫` (currently untypeable, but we could ask for `\boxbar`).

		@@ -0,0 +1,44 @@
		-- Copyright (c) 2017 Scott Morrison. All rights reserved.


		open categories

		namespace categories.functor

feat(category_theory): basic definitions #152

feat(category_theory): basic definitions #152

Conversation

semorrison commented Jun 4, 2018

semorrison commented Jun 4, 2018

jcommelin left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

semorrison left a comment

Choose a reason for hiding this comment

rwbarton commented Jun 12, 2018

rwbarton commented Jun 12, 2018

rwbarton commented Jun 12, 2018

semorrison commented Jun 15, 2018

semorrison commented Jun 15, 2018

rwbarton commented Jun 15, 2018

semorrison commented Jun 20, 2018

jcommelin commented Jun 21, 2018

semorrison commented Jun 21, 2018

johoelzl left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

johoelzl commented Jul 9, 2018

semorrison commented Jul 27, 2018

johoelzl commented Jul 31, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

digama0 Aug 7, 2018 • edited

Choose a reason for hiding this comment

semorrison commented Aug 7, 2018 via email

semorrison commented Aug 7, 2018 via email

digama0 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

digama0 Aug 7, 2018 •

edited