Theorems · Inductive type · algebraic topology

SSet.RelativeMorphism.Homotopy

{X Y : SSet} →
  {A : X.Subcomplex} →
    {B : Y.Subcomplex} → {φ : A.toSSet ⟶ B.toSSet} → SSet.RelativeMorphism A B φ → SSet.RelativeMorphism A B φ → Type u

The type of homotopies between morphisms of simplicial sets relatively to given subcomplexes. (See also SSet.Homotopy in the file Mathlib/AlgebraicTopology/SimplicialSet/Homotopy.lean for the non-relative version.)

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism

Cited by

14 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound