Theorems · Definition · algebraic topology
SSet.Homotopy
{X Y : SSet} → (X ⟶ Y) → (X ⟶ Y) → Type uThe type of homotopies between morphisms X ⟶ Y of simplicial sets.
The data consists of a morphism h : X ⊗ Δ[1] ⟶ Y which induces
both f and g, see the lemmas SSet.Homotopy.h₀ and SSet.Homotopy.h₁.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- Oppositestatement · cited by 8,081
- Equiv.symmproof · cited by 3,681
- SimplexCategorystatement · cited by 2,204
- SSetstatement and proof · cited by 1,283
- SSet.RelativeMorphism.Homotopyproof · cited by 14
- SSet.RelativeMorphism.botEquivproof · cited by 6
Cited by10
Results whose statement or proof uses this declaration.
- SSet.Homotopy.chainComplexMapstatement and proof · cited by 1
- SSet.Homotopy.congr_homologyMapstatement and proof · cited by 1
- SSet.Homotopy.h₀statement and proof · cited by 1
- SSet.Homotopy.h₁statement and proof · cited by 1
- TopCat.Homotopy.toSSetstatement · cited by 0
- SSet.Homotopy.congr_homologyMap_singularChainComplexFunctorstatement · cited by 0
- SSet.Homotopy.h₀_assocstatement and proof · cited by 0
- SSet.Homotopy.h₁_assocstatement and proof · cited by 0
- SSet.Homotopy.singularChainComplexFunctorObjMapstatement · cited by 0
- SSet.Homotopy.toSimplicialObjectHomotopystatement and proof · cited by 0