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