I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category (D i)
A : Type u₁
inst✝ : Category A
x : (i : I) → C i
i : I
⊢ eqToHom (_ : x = x) i = eqToHom (_ : x i = x i)
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category (D i)
A : Type u₁
inst✝ : Category A
x x' : (i : I) → C i
h : x = x'
i : I
⊢ eqToHom h i = eqToHom (_ : x i = x' i)
subst h
no goals
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category (D i)
A : Type u₁
inst✝ : Category A
x : (i : I) → C i
i : I
⊢ eqToHom (_ : x = x) i = eqToHom (_ : x i = x i)
rfl