Lean: σ is reserved after open unitInterval; build a ContinuousMap.Homotopy inline

After open unitInterval, the identifier σ is notation for unitInterval.symm, so a binder (σ : ℝ) fails with "unexpected token 'σ'; expected '_' or identifier". The later errors are cascades (unknown identifiers for every lemma that used σ). Rename the variable. To show a loop ζ ↦ φ(equator ζ) is null-homotopic when φ is continuous on a cap, build the homotopy inline as { toFun := fun q : I × Circle ↦ φ (capPoint q.1 q.2), continuous_toFun := hφ.comp_continuous hcap hmem, map_zero_left := …, map_one_left := … } of type ContinuousMap.Homotopy f (ContinuousMap.const _ c). Here ContinuousOn.comp_continuous : ContinuousOn g s → Continuous f → (∀ x, f x ∈ s) → Continuous (g ∘ f) is the key glue, and map_zero_left/map_one_left close by simp once you have point-equality lemmas (capPoint 0 ζ = equator ζ; capPoint 1 ζ independent of ζ, which follows from √(1-1) = 0).