OAI/CategoryTheory/Thomason/Simplicial/WeakPathSurjectivity.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Exact cubical boundary extensions and simplicial nullhomotopies

  1. def OAI.Thomason.Construction.RealizedCube.boundaryNullhomotopyOfExtension line 28

    Source documentation

    Restrict the simultaneous cube contraction through a given extension. This is a homotopy of the whole cubical boundary, with both endpoints exact.

    def boundaryNullhomotopyOfExtension {X : SSet.{0}} (n : ℕ)
    (a : (boundary n : SSet.{0}) ⟶ X) (d : obj (n+1) ⟶ X)
    (hd : (boundary n).ι ≫ d = a) :
    SSet.Homotopy (SSet.const (d.app _ (initialVertex (n+1)))) a := by
…

    Mentions: OAI.Thomason.Construction.RealizedCube.boundary, OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.RealizedCube.initialVertex

  2. theorem OAI.Thomason.Construction.RealizedCube.kan_boundary_extension_iff_nullhomotopy line 37

    Source documentation

    The whole cubical boundary has an exact extension in a Kan complex if and only if its given map has an actual simplicial nullhomotopy.

    theorem kan_boundary_extension_iff_nullhomotopy {X : SSet.{0}} [SSet.KanComplex X]
    (n : ℕ) (a : (boundary n : SSet.{0}) ⟶ X) :
    (∃ d : obj (n+1) ⟶ X, (boundary n).ι ≫ d = a) ↔
      ∃ x : X _⦋0⦌, Nonempty (SSet.Homotopy (SSet.const x) a) := by
…

    Mentions: OAI.Thomason.Construction.RealizedCube.boundary, OAI.Thomason.Construction.RealizedCube.obj

  3. def OAI.Thomason.Construction.realizationUnitHomotopy line 67

    Source documentation

    A continuous homotopy between realized simplicial maps gives an actual simplicial homotopy after the realization/singular unit. Its evaluation is exact; no weak-equivalence assertion about that unit is used.

    def realizationUnitHomotopy {A X : SSet.{0}} {f g : A ⟶ X}
    (H : (SSet.toTop.map f).hom.Homotopy (SSet.toTop.map g).hom) :
    SSet.Homotopy (f ≫ sSetTopAdj.unit.app X) (g ≫ sSetTopAdj.unit.app X) where
…
  4. theorem OAI.Thomason.Construction.realizationUnitHomotopy_evaluate line 99

    Source documentation

    The singular carrier retains the complete original continuous homotopy.

    theorem realizationUnitHomotopy_evaluate {A X : SSet.{0}} {f g : A ⟶ X}
    (H : (SSet.toTop.map f).hom.Homotopy (SSet.toTop.map g).hom)
    (t : unitInterval) (x : SSet.toTop.obj A) :
    evaluateSingularCylinder (realizationUnitHomotopy H).h (t, x) = H (t, x) :=
…

    Mentions: OAI.Thomason.Construction.evaluateSingularCylinder, OAI.Thomason.Construction.realizationUnitHomotopy

  5. theorem OAI.Thomason.Construction.finite_singular_homotopy_support line 108

    Source documentation

    For a finite parameter complex, the entire continuous homotopy gives one finite singular subcomplex, with both original endpoint maps retained exactly after the unit. It does not assert an approximation in X itself.

    theorem finite_singular_homotopy_support {A X : SSet.{0}} [A.Finite] {f g : A ⟶ X}
    (H : (SSet.toTop.map f).hom.Homotopy (SSet.toTop.map g).hom) :
    ∃ S : (TopCat.toSSet.obj (SSet.toTop.obj X)).Subcomplex,
      SSet.Finite S.toSSet ∧ ∃ (fS gS : A ⟶ S.toSSet) (HS : SSet.Homotopy fS gS),
        fS ≫ S.ι = f ≫ sSetTopAdj.unit.app X ∧
        gS ≫ S.ι = g ≫ sSetTopAdj.unit.app X ∧
        HS.h ≫ S.ι = (realizationUnitHomotopy H).h := by
…

    Mentions: OAI.Thomason.Construction.realizationUnitHomotopy

  6. theorem OAI.Thomason.Construction.finite_singular_nullhomotopy_support line 157

    Source documentation

    A continuous nullhomotopy of a finite simplicial family has an exact simplicial nullhomotopy in one finite subcomplex of the singular realization. The given family is retained after the unit. Moving this witness into X itself requires approximation.

    theorem finite_singular_nullhomotopy_support {A X : SSet.{0}} [A.Finite]
    (v : A _⦋0⦌) (x : X _⦋0⦌) (a : A ⟶ X)
    (H : (ContinuousMap.const (SSet.toTop.obj A) (RealizationPrism.vertexPoint X x)).Homotopy
      (SSet.toTop.map a).hom) :
    ∃ S : (TopCat.toSSet.obj (SSet.toTop.obj X)).Subcomplex,
      SSet.Finite S.toSSet ∧ ∃ (xS : S.toSSet _⦋0⦌) (aS : A ⟶ S.toSSet),
        aS ≫ S.ι = a ≫ sSetTopAdj.unit.app X ∧
        Nonempty (SSet.Homotopy (SSet.const xS) aS) := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.vertexPoint

  7. theorem OAI.Thomason.Construction.kan_lift_iff_contracted_fiber_extension line 209

    Source documentation

    For every monomorphic relative lifting problem over an explicitly contracted base, extension of the transported boundary inside its actual simplicial fibre is equivalent to an exact lift in the original total space. The same chosen retraction is a strict retraction on that fibre.

    theorem kan_lift_iff_contracted_fiber_extension {A K E B : SSet.{0}}
    (v : B _⦋0⦌) (C : SSet.Homotopy (SSet.const v) (𝟙 B))
    (hC : ∀ L : SSet.{0}, (SSet.const (X := L) v) ▷ Δ[1] ≫ C.h =
…
  8. theorem OAI.Thomason.Construction.RealizedCube.boundary_lift_iff_fiber_nullhomotopy line 281

    Source documentation

    An arbitrary cubical boundary square over a finite cube lifts exactly if and only if its transported boundary has a simplicial nullhomotopy in the initial Kan fibre. All maps in the square and its boundary are retained.

    theorem boundary_lift_iff_fiber_nullhomotopy {E : SSet.{0}} (m n : ℕ)
    (p : E ⟶ obj m) [HomotopicalAlgebra.Fibration p]
    (a : (boundary n : SSet.{0}) ⟶ E) (b : obj (n+1) ⟶ obj m)
    (hab : a ≫ p = (boundary n).ι ≫ b) :
    ∃ r : E ⟶ (simplicialPointFiber p (initialVertex m)).toSSet,
      (simplicialPointFiber p (initialVertex m)).ι ≫ r = 𝟙 _ ∧
      ((∃ d : obj (n+1) ⟶ E, (boundary n).ι ≫ d = a ∧ d ≫ p = b) ↔
        ∃ x, Nonempty (SSet.Homotopy (SSet.const x) (a ≫ r))) := by
…

    Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.RealizedCube.boundary, OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.RealizedCube.initialVertex

  9. theorem OAI.Thomason.Construction.kan_endpoint_fibers_homotopy_inverse line 316

    Source documentation

    The two endpoint fibres of a Kan fibration over the interval have actual simplicial homotopy inverse maps. Both maps are realization weak equivalences, without any acyclic-Kan-lifting hypothesis.

    theorem kan_endpoint_fibers_homotopy_inverse {E : SSet.{0}}
    (p : E ⟶ (Δ[1] : SSet.{0})) [HomotopicalAlgebra.Fibration p] :
    ∃ (f : (simplicialPointFiber p (initialSimplexVertex 1)).toSSet ⟶
          (simplicialPointFiber p (finalSimplexVertex 1)).toSSet)
      (g : (simplicialPointFiber p (finalSimplexVertex 1)).toSSet ⟶
          (simplicialPointFiber p (initialSimplexVertex 1)).toSSet),
      realizationWeakEquivalences f ∧ realizationWeakEquivalences g ∧
      Nonempty (SSet.Homotopy (𝟙 _) (f ≫ g)) ∧
      Nonempty (SSet.Homotopy (g ≫ f) (𝟙 _)) := by
…

    Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.finalSimplexVertex, OAI.Thomason.Construction.realizationWeakEquivalences

  10. theorem OAI.Thomason.Construction.kan_endpoint_fibers_exact_extension line 355

    Source documentation

    A single weak simplicial transport map simultaneously preserves and reflects exact extension problems for every monomorphism, hence all higher boundaries. This assertion is stronger than transporting W-status.

    theorem kan_endpoint_fibers_exact_extension {E : SSet.{0}}
    (p : E ⟶ (Δ[1] : SSet.{0})) [HomotopicalAlgebra.Fibration p] :
    ∃ f : (simplicialPointFiber p (initialSimplexVertex 1)).toSSet ⟶
        (simplicialPointFiber p (finalSimplexVertex 1)).toSSet,
      realizationWeakEquivalences f ∧
      ∀ (A K : SSet.{0}) (i : A ⟶ K) (_ : Mono i)
        (a : A ⟶ (simplicialPointFiber p (initialSimplexVertex 1)).toSSet),
        (∃ d : K ⟶ (simplicialPointFiber p (initialSimplexVertex 1)).toSSet, i ≫ d = a) ↔
          (∃ d : K ⟶ (simplicialPointFiber p (finalSimplexVertex 1)).toSSet, i ≫ d = a ≫ f) := by
…

    Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.finalSimplexVertex, OAI.Thomason.Construction.realizationWeakEquivalences

  11. theorem OAI.Thomason.Construction.kan_interval_fibers_homotopy_inverse line 390

    Source documentation

    Pullback identifies transport along any base interval with the actual endpoint homotopy equivalence. No contractibility of the ambient base is required.

    theorem kan_interval_fibers_homotopy_inverse {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (g : (Δ[1] : SSet.{0}) ⟶ B) :
    ∃ (f : (simplicialPointFiber p (g.app _ (initialSimplexVertex 1))).toSSet ⟶
          (simplicialPointFiber p (g.app _ (finalSimplexVertex 1))).toSSet)
      (r : (simplicialPointFiber p (g.app _ (finalSimplexVertex 1))).toSSet ⟶
          (simplicialPointFiber p (g.app _ (initialSimplexVertex 1))).toSSet),
      realizationWeakEquivalences f ∧ realizationWeakEquivalences r ∧
      Nonempty (SSet.Homotopy (𝟙 _) (f ≫ r)) ∧
      Nonempty (SSet.Homotopy (r ≫ f) (𝟙 _)) := by
…

    Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.finalSimplexVertex, OAI.Thomason.Construction.realizationWeakEquivalences

  12. theorem OAI.Thomason.Construction.kan_fiber_boundary_extension_iff_of_interval line 425

    Source documentation

    In every degree, exact boundary extension in the fibre is invariant along an arbitrary base interval. Both implications produce exact fillers.

    theorem kan_fiber_boundary_extension_iff_of_interval {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (g : (Δ[1] : SSet.{0}) ⟶ B) (n : ℕ) :
    (∀ a : (SSet.boundary n : SSet.{0}) ⟶
        (simplicialPointFiber p (g.app _ (initialSimplexVertex 1))).toSSet,
      ∃ d : (Δ[n] : SSet.{0}) ⟶ _, (SSet.boundary n).ι ≫ d = a) ↔
    (∀ a : (SSet.boundary n : SSet.{0}) ⟶
        (simplicialPointFiber p (g.app _ (finalSimplexVertex 1))).toSSet,
      ∃ d : (Δ[n] : SSet.{0}) ⟶ _, (SSet.boundary n).ι ≫ d = a) := by
…

    Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.finalSimplexVertex

  13. theorem OAI.Thomason.Construction.kan_fiber_boundary_extension_iff_of_edge line 455

    Source documentation

    Exact higher fibre extensions are constant on a simplicial edge.

    theorem kan_fiber_boundary_extension_iff_of_edge {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] {x y : B _⦋0⦌} (e : SSet.Edge x y) (n : ℕ) :
    (∀ a : (SSet.boundary n : SSet.{0}) ⟶ (simplicialPointFiber p x).toSSet,
      ∃ d : (Δ[n] : SSet.{0}) ⟶ _, (SSet.boundary n).ι ≫ d = a) ↔
    (∀ a : (SSet.boundary n : SSet.{0}) ⟶ (simplicialPointFiber p y).toSSet,
      ∃ d : (Δ[n] : SSet.{0}) ⟶ _, (SSet.boundary n).ι ≫ d = a) := by
…

    Mentions: OAI.Thomason.Construction.simplicialPointFiber

  14. theorem OAI.Thomason.Construction.kan_fiber_boundary_extension_iff_of_realization_path line 491

    Source documentation

    A continuous path between realized base vertices transports every higher exact fibre extension test. Only the proved component comparison is used to pass to a finite edge zigzag.

    theorem kan_fiber_boundary_extension_iff_of_realization_path {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] {x y : B _⦋0⦌}
    (h : Path (RealizationPrism.vertexPoint B x) (RealizationPrism.vertexPoint B y)) (n : ℕ) :
    (∀ a : (SSet.boundary n : SSet.{0}) ⟶ (simplicialPointFiber p x).toSSet,
      ∃ d : (Δ[n] : SSet.{0}) ⟶ _, (SSet.boundary n).ι ≫ d = a) ↔
    (∀ a : (SSet.boundary n : SSet.{0}) ⟶ (simplicialPointFiber p y).toSSet,
      ∃ d : (Δ[n] : SSet.{0}) ⟶ _, (SSet.boundary n).ι ≫ d = a) := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.vertexPoint, OAI.Thomason.Construction.simplicialPointFiber

  15. theorem OAI.Thomason.Construction.simplex_boundary_lifting_of_initial_fiber line 528

    Source documentation

    For a Kan fibration over a standard simplex, a prescribed boundary lifts exactly whenever all boundaries of that degree extend in the initial vertex fibre. The proof transports the whole boundary along the stationary base contraction, extends in the fibre, and lifts the return cylinder.

    theorem simplex_boundary_lifting_of_initial_fiber {E : SSet.{0}} (m n : ℕ)
    (p : E ⟶ (Δ[m] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
    (hF : ∀ a : (SSet.boundary n : SSet.{0}) ⟶
        (simplicialPointFiber p (initialSimplexVertex m)).toSSet,
      ∃ d : (Δ[n] : SSet.{0}) ⟶ (simplicialPointFiber p (initialSimplexVertex m)).toSSet,
        (SSet.boundary n).ι ≫ d = a) :
    HasLiftingProperty (SSet.boundary n).ι p := by
…

    Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.initialSimplexVertex

  16. theorem OAI.Thomason.Construction.initial_fiber_extension_of_simplex_boundary_lifting line 579

    Source documentation

    The exact converse: boundary lifting against the fibration restricts to boundary extension in its literal initial fibre.

    theorem initial_fiber_extension_of_simplex_boundary_lifting {E : SSet.{0}} (m n : ℕ)
    (p : E ⟶ (Δ[m] : SSet.{0}))
    (hp : HasLiftingProperty (SSet.boundary n).ι p)
    (a : (SSet.boundary n : SSet.{0}) ⟶
      (simplicialPointFiber p (initialSimplexVertex m)).toSSet) :
    ∃ d : (Δ[n] : SSet.{0}) ⟶ (simplicialPointFiber p (initialSimplexVertex m)).toSSet,
      (SSet.boundary n).ι ≫ d = a := by
…

    Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.initialSimplexVertex

  17. theorem OAI.Thomason.Construction.simplex_boundary_lifting_iff_initial_fiber line 599

    Source documentation

    For every degree, lifting over a standard simplex is precisely the extension problem in its initial Kan fibre.

    theorem simplex_boundary_lifting_iff_initial_fiber {E : SSet.{0}} (m n : ℕ)
    (p : E ⟶ (Δ[m] : SSet.{0})) [HomotopicalAlgebra.Fibration p] :
    HasLiftingProperty (SSet.boundary n).ι p ↔
      ∀ a : (SSet.boundary n : SSet.{0}) ⟶
          (simplicialPointFiber p (initialSimplexVertex m)).toSSet,
        ∃ d : (Δ[n] : SSet.{0}) ⟶ (simplicialPointFiber p (initialSimplexVertex m)).toSSet,
          (SSet.boundary n).ι ≫ d = a :=
…

    Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.initialSimplexVertex

  18. theorem OAI.Thomason.Construction.simplex_boundary_lifting_iff_fiber_nullhomotopies line 611

    Source documentation

    The remaining local higher lifting step is EXACTLY a simplicial nullhomotopy in the initial fibre. No continuous approximation is assumed.

    theorem simplex_boundary_lifting_iff_fiber_nullhomotopies {E : SSet.{0}} (m n : ℕ)
    (p : E ⟶ (Δ[m] : SSet.{0})) [HomotopicalAlgebra.Fibration p] :
    HasLiftingProperty (SSet.boundary n).ι p ↔
      ∀ a : (SSet.boundary n : SSet.{0}) ⟶
          (simplicialPointFiber p (initialSimplexVertex m)).toSSet,
        ∃ x, Nonempty (SSet.Homotopy (SSet.const x) a) := by
…

    Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.initialSimplexVertex

  19. abbrev OAI.Thomason.Construction.SubdivisionHornFaces.Faces line 644
  20. def OAI.Thomason.Construction.SubdivisionHornFaces.omitted line 646
  21. abbrev OAI.Thomason.Construction.SubdivisionHornFaces.Remainder line 649
  22. abbrev OAI.Thomason.Construction.SubdivisionHornFaces.HornFaces line 652
  23. instance OAI.Thomason.Construction.SubdivisionHornFaces.(instance at line 655) line 655
  24. instance OAI.Thomason.Construction.SubdivisionHornFaces.(instance at line 658) line 658
  25. def OAI.Thomason.Construction.SubdivisionHornFaces.topFace line 661
  26. def OAI.Thomason.Construction.SubdivisionHornFaces.vertexFace line 665
  27. theorem OAI.Thomason.Construction.SubdivisionHornFaces.vertex_ne_top line 669
  28. def OAI.Thomason.Construction.SubdivisionHornFaces.vertex line 675
  29. def OAI.Thomason.Construction.SubdivisionHornFaces.top line 681
  30. def OAI.Thomason.Construction.SubdivisionHornFaces.inclusion line 687
  31. def OAI.Thomason.Construction.SubdivisionHornFaces.addVertex line 690
  32. theorem OAI.Thomason.Construction.SubdivisionHornFaces.addVertex_proper line 700
  33. def OAI.Thomason.Construction.SubdivisionHornFaces.addVertexHorn line 711
  34. def OAI.Thomason.Construction.SubdivisionHornFaces.rank line 715
  35. def OAI.Thomason.Construction.SubdivisionHornFaces.edgeSection line 725
  36. def OAI.Thomason.Construction.SubdivisionHornFaces.toPoint line 736
  37. def OAI.Thomason.Construction.SubdivisionHornFaces.fromPoint line 739
  38. def OAI.Thomason.Construction.SubdivisionHornFaces.intervalStart line 742
  39. theorem OAI.Thomason.Construction.SubdivisionHornFaces.identity_le_addVertex line 744
  40. theorem OAI.Thomason.Construction.SubdivisionHornFaces.section_rank_le_addVertex line 747
  41. theorem OAI.Thomason.Construction.SubdivisionHornFaces.identity_le_addVertexHorn line 759
  42. theorem OAI.Thomason.Construction.SubdivisionHornFaces.point_le_addVertexHorn line 762
  43. theorem OAI.Thomason.Construction.SubdivisionHornFaces.nerveMap_mono line 766
  44. theorem OAI.Thomason.Construction.SubdivisionHornFaces.intervalStart_anodyne line 777
  45. theorem OAI.Thomason.Construction.SubdivisionHornFaces.hornFaces_inclusion_anodyne line 803

    Source documentation

    After removal of the omitted facet, the full horn face-poset inclusion is anodyne. The proof is the two explicit ordered homotopies of the pair.

    theorem hornFaces_inclusion_anodyne (n : ℕ) (k : Fin (n + 2)) :
    SSet.anodyneExtensions (nerveMap (inclusion n k).monotone.functor) := by
…

    Mentions: OAI.Thomason.Construction.SubdivisionHornFaces.inclusion

  46. theorem OAI.Thomason.Construction.SubdivisionHornFaces.omitted_subset_cases line 857
  47. def OAI.Thomason.Construction.SubdivisionHornFaces.remainderInclusion line 873
  48. def OAI.Thomason.Construction.SubdivisionHornFaces.removeOmitted line 876
  49. theorem OAI.Thomason.Construction.SubdivisionHornFaces.removeOmitted_inclusion line 895
  50. theorem OAI.Thomason.Construction.SubdivisionHornFaces.identity_le_removeOmitted line 900
  51. theorem OAI.Thomason.Construction.SubdivisionHornFaces.remainder_inclusion_anodyne line 910

    Source documentation

    The omitted facet is an up-beat vertex of the full face poset. Removing it induces an anodyne nerve inclusion by a stationary ordered homotopy.

    theorem remainder_inclusion_anodyne (n : ℕ) (k : Fin (n + 2)) :
    SSet.anodyneExtensions (nerveMap (remainderInclusion n k).monotone.functor) := by
…

    Mentions: OAI.Thomason.Construction.SubdivisionHornFaces.remainderInclusion

  52. theorem OAI.Thomason.Construction.SubdivisionHornFaces.full_hornFaces_inclusion_anodyne line 937

    Source documentation

    The actual inclusion of the full horn face poset in the full simplex face poset is anodyne, in every positive dimension and for every horn.

    theorem full_hornFaces_inclusion_anodyne (n : ℕ) (k : Fin (n + 2)) :
    SSet.anodyneExtensions (nerveMap
      ((remainderInclusion n k).comp (inclusion n k)).monotone.functor) := by
…

    Mentions: OAI.Thomason.Construction.SubdivisionHornFaces.remainderInclusion, OAI.Thomason.Construction.SubdivisionHornFaces.inclusion

  53. theorem OAI.Thomason.Construction.fundamentalGroup_map_surjective line 962

    Source documentation

    Surjectivity on the actual first homotopy group implies surjectivity of Mathlib's fundamental-group map under the explicit comparison.

    theorem fundamentalGroup_map_surjective {X Y : Type} [TopologicalSpace X]
    [TopologicalSpace Y] (f : C(X, Y)) (x : X)
    (hf : Function.Surjective (HomotopyMaps.groupMap f 1 x)) :
    Function.Surjective (FundamentalGroup.map f x) := by
…

    Mentions: OAI.Thomason.Construction.HomotopyMaps.groupMap

  54. theorem OAI.Thomason.Construction.weak_path_homotopy_surjective line 973

    Source documentation

    A weak homotopy equivalence lifts any path up to homotopy relative to its specified endpoints. This uses only component injectivity and π₁ surjectivity.

    theorem weak_path_homotopy_surjective {X Y : Type} [TopologicalSpace X]
    [TopologicalSpace Y] (f : C(X, Y)) (hf : IsWeakHomotopyEquivalence f)
    {x₀ x₁ : X} (γ : Path (f x₀) (f x₁)) :
    ∃ α : Path x₀ x₁, (α.map f.continuous).Homotopic γ := by
…

    Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence