case w
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ ↑(F.map f ≫ coconeMorphism F j') x✝ = ↑(coconeMorphism F j) x✝
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j
ext
case w.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j' (↑(F.map f) x✝)) (Prequotient.of j x✝)
case w
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ ↑(F.map f ≫ coconeMorphism F j') x✝ = ↑(coconeMorphism F j) x✝
apply Quot.sound
no goals
case w.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ AddCommGroupCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j' (↑(F.map f) x✝)) (Prequotient.of j x✝)
apply Relation.map