Theorems · Theorem · category theory

AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso.inv.app X).left =
    CategoryTheory.CategoryStruct.id
      (X.obj
        (match CategoryTheory.WithTerminal.incl.obj (Opposite.op { len := 0 }) with
        | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
        | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star))

Defined in

Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category