case refl
C : Type u₁
inst✝ : Category C
X Z : C
q : X ⟶ Z
⊢ cast (_ : (X ⟶ Z) = (X ⟶ Z)) q = eqToHom (_ : X = X) ≫ q
C : Type u₁
inst✝ : Category C
X Y Z : C
p : X = Y
q : Y ⟶ Z
⊢ cast (_ : (Y ⟶ Z) = (X ⟶ Z)) q = eqToHom p ≫ q
cases p
no goals
case refl
C : Type u₁
inst✝ : Category C
X Z : C
q : X ⟶ Z
⊢ cast (_ : (X ⟶ Z) = (X ⟶ Z)) q = eqToHom (_ : X = X) ≫ q
simp