case refl
C : Type u₁
inst✝ : Category C
X : C
⊢ (eqToHom (_ : X = X)).op = eqToHom (_ : X.op = X.op)
C : Type u₁
inst✝ : Category C
X Y : C
h : X = Y
⊢ (eqToHom h).op = eqToHom (_ : Y.op = X.op)
cases h
no goals
case refl
C : Type u₁
inst✝ : Category C
X : C
⊢ (eqToHom (_ : X = X)).op = eqToHom (_ : X.op = X.op)
rfl