## Stream: new members

### Topic: comma category

#### Jakob Scholbach (Mar 29 2021 at 19:46):

another newbie question: I want to define a projection functor from a comma category. In one case this works, in the other it doesn't -- why?
(The error message I get in the first case is type mismatch at field 'obj' λ (X : comma L R), X.left has type comma L R → auto_param A (name.mk_string "obviously" name.anonymous) but is expected to have type comma L R → A_1

import category_theory.comma

namespace category_theory

universes v v₁ v₂ v₃ u u₁ u₂ u₃
variables {A : Type u₁} [category.{v} A]
variables {B : Type u₂} [category.{v} B]
variables {T : Type u₃} [category.{v} T]

variables {L : A ⥤ T} {R : B ⥤ T}

def proj_left_fails {A : Type u₁} [category.{v} A] {B : Type u₂} [category.{v} B] {T : Type u₃} [category.{v} T] :
(comma.{v v v} L R) ⥤ A :=
{ obj := λ X , X.left,
map := λ X Y f, f.left }

def proj_left_works : (comma.{v v v} L R) ⥤ A :=
{ obj := λ X, X.left,
map := λ X Y f, f.left }

end category_theory


#### Markus Himmel (Mar 29 2021 at 19:52):

In the first case, you have two different things called A, and L and R are declared using the first A, but the A in (comma L R) \func A is the second A

Aha!

#### Markus Himmel (Mar 29 2021 at 19:55):

The error message tries to hint at this by calling them A and A_1, but the auto_param stuff (which can be ignored) obscures this

#### Jakob Scholbach (Mar 29 2021 at 19:59):

OK, I see. Will watch out for _1 in the future...

#### Kevin Buzzard (Mar 29 2021 at 20:12):

The trick with all that autoparam nonsense is to just note that you can just cross out the auto_param and also the name.mk_string stuff and then it's easier to read what it actually says :-)

#### Adam Topaz (Mar 29 2021 at 21:21):

@Jakob Scholbach note that we have docs#category_theory.comma.fst and docs#category_theory.comma.snd

#### Adam Topaz (Mar 29 2021 at 21:23):

What's going on with this topic BTW? It looks like at some point the topic no topic was renamed to comma category? :rofl:

#### Bryan Gin-ge Chen (Mar 29 2021 at 21:30):

What's going on with this topic BTW? It looks like at some point the topic no topic was renamed to comma category? :rofl: