Theorems · Definition · category theory

SimplexCategory.Truncated.Hom.tr

{n : ℕ} →
  {a b : SimplexCategory} →
    (a ⟶ b) →
      (ha : autoParam (a.len ≤ n) SimplexCategory.Truncated.Hom.tr._auto_1) →
        (hb : autoParam (b.len ≤ n) SimplexCategory.Truncated.Hom.tr._auto_3) →
          { obj := a, property := ha } ⟶ { obj := b, property := hb }

Make a morphism in Truncated n from a morphism in SimplexCategory. This is equivalent to @id (⦋a⦌ₙ ⟶ ⦋b⦌ₙ) f.

Defined in

Mathlib.AlgebraicTopology.SimplexCategory.Defs

Cited by

43 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Quot.sound