J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
j j' : J
x : F.obj j
x' : F.obj j'
w : colimit.ι F j x = colimit.ι F j' x'
⊢ Quot.mk (Quot.Rel F) { fst := j, snd := x } = Quot.mk (Quot.Rel F) { fst := j', snd := x' }
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
j j' : J
x : F.obj j
x' : F.obj j'
w : colimit.ι F j x = colimit.ι F j' x'
⊢ EqvGen (Quot.Rel F) { fst := j, snd := x } { fst := j', snd := x' }
apply Quot.eq.1
no goals
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
j j' : J
x : F.obj j
x' : F.obj j'
w : colimit.ι F j x = colimit.ι F j' x'
⊢ Quot.mk (Quot.Rel F) { fst := j, snd := x } = Quot.mk (Quot.Rel F) { fst := j', snd := x' }
simpa using congr_arg (colimitEquivQuot.{v, u} F) w