case refl
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X Z : C
f : W ⟶ X
h' : X = Z
g : W ⟶ Z
⊢ f = eqToHom (_ : W = W) ≫ g ≫ eqToHom (_ : Z = X) ↔ HEq f g
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
h : W = Y
h' : X = Z
⊢ f = eqToHom h ≫ g ≫ eqToHom (_ : Z = X) ↔ HEq f g
cases h
case refl.refl
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X : C
f g : W ⟶ X
⊢ f = eqToHom (_ : W = W) ≫ g ≫ eqToHom (_ : X = X) ↔ HEq f g
case refl
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X Z : C
f : W ⟶ X
h' : X = Z
g : W ⟶ Z
⊢ f = eqToHom (_ : W = W) ≫ g ≫ eqToHom (_ : Z = X) ↔ HEq f g
cases h'
no goals
case refl.refl
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X : C
f g : W ⟶ X
⊢ f = eqToHom (_ : W = W) ≫ g ≫ eqToHom (_ : X = X) ↔ HEq f g
simp