case w
C : Type u
inst✝ : Category C
X : SimplicialObject C
n : ℕ
h : n = n
⊢ (eqToIso X h).hom = (Iso.refl (X.obj [n].op)).hom
C : Type u
inst✝ : Category C
X : SimplicialObject C
n : ℕ
h : n = n
⊢ eqToIso X h = Iso.refl (X.obj [n].op)
ext
no goals
case w
C : Type u
inst✝ : Category C
X : SimplicialObject C
n : ℕ
h : n = n
⊢ (eqToIso X h).hom = (Iso.refl (X.obj [n].op)).hom
simp [eqToIso]