case h
F✝ : Type ?u.84224
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
F : Homotopy f₀ f₁
x✝ : ↑I × X
⊢ ↑(symm (symm F)) x✝ = ↑F x✝
F✝ : Type ?u.84224
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
F : Homotopy f₀ f₁
⊢ symm (symm F) = F
ext
no goals
case h
F✝ : Type ?u.84224
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ : C(X, Y)
F : Homotopy f₀ f₁
x✝ : ↑I × X
⊢ ↑(symm (symm F)) x✝ = ↑F x✝
simp