J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X : limit (F ⋙ objects)
j : J
⊢ limit.π (homDiagram X X) j (eqToHom (_ : X = X)) = eqToHom (_ : limit.π (F ⋙ objects) j X = limit.π (F ⋙ objects) j X)
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
j : J
h : X = Y
⊢ limit.π (homDiagram X Y) j (eqToHom h) = eqToHom (_ : limit.π (F ⋙ objects) j X = limit.π (F ⋙ objects) j Y)
subst h
no goals
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X : limit (F ⋙ objects)
j : J
⊢ limit.π (homDiagram X X) j (eqToHom (_ : X = X)) = eqToHom (_ : limit.π (F ⋙ objects) j X = limit.π (F ⋙ objects) j X)
simp