OAI/CategoryTheory/Thomason/Gray/FixedPathCylinders.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thomason.Construction.singularCylinderMap_one line 18
2. def OAI.Thomason.Construction.fixedPathFamily line 35
3. def OAI.Thomason.Construction.fixedPathCylinder line 42
4. theorem OAI.Thomason.Construction.fixedPathCylinder_evaluate line 46
5. theorem OAI.Thomason.Construction.fixedPathCylinder_zero line 53
6. theorem OAI.Thomason.Construction.fixedPathCylinder_one line 63
7. theorem OAI.Thomason.Construction.fixedPathCylinder_naturality line 73
8. theorem OAI.Thomason.Construction.fixedPathCylinder_postcomp line 85
9. def OAI.Thomason.Construction.fixedPathRealization line 102

   Source documentation

   An evaluated cylinder with constant endpoints is a continuous family of paths with those endpoints.

   def fixedPathRealization {K : SSet.{0}} {X : TopCat.{0}} {x y : X}
       (e : K ⊗ Δ[1] ⟶ TopCat.toSSet.obj X)
       (h₀ : SSet.ι₀ ≫ e = SSet.const (TopCat.toSSetObj₀Equiv.symm x))
       (h₁ : SSet.ι₁ ≫ e = SSet.const (TopCat.toSSetObj₀Equiv.symm y)) :
       SSet.toTop.obj K ⟶ TopCat.of (Path x y) := TopCat.ofHom {
   …