Defs

📁 Source: Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean

Statistics

Metric	Count
Definitions SimplexCategory, comp, id, mk, toOrderHom, tr, incl, inclCompInclusion, inclusion, fullyFaithful, instInhabited, mkNotation, tacticTrunc, homEquivFunctor, homEquivOrderHom, len, mk, rec, smallCategory, «term⦋_⦌»	20
Theorems ext, ext', ext_iff, mk_toOrderHom, mk_toOrderHom_apply, toOrderHom_mk, ext, ext_iff, tr_comp, tr_comp', tr_comp'_assoc, tr_comp_assoc, tr_id, comp_toOrderHom, ext, ext_iff, id_toOrderHom, len_mk, mk_len	19
Total	39

SimplexCategory

Definitions

Name	Category	Theorems
homEquivFunctor 📖	CompOp	—
homEquivOrderHom 📖	CompOp	—
len 📖	CompOp	261 math math: SimplicialObject.Splitting.cofan_inj_πSummand_eq_id_assoc, Truncated.δ₂_two_comp_σ₂_one_assoc, SSet.stdSimplex.coe_triangle_down_toOrderHom, eq_const_of_zero, SimplexCategoryGenRel.toSimplexCategory_len, SSet.Truncated.tensor_map_apply_snd, CategoryTheory.nerve.σ_obj, const_eq_id, SSet.Truncated.mapHomotopyCategory_homMk, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp_assoc, CategoryTheory.Arrow.augmentedCechNerve_hom_app, CategoryTheory.Arrow.mapCechNerve_app, CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_base, SSet.Truncated.Path.mk₂_arrow, len_mk, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', CategoryTheory.nerve.functorOfNerveMap_map, SSet.Truncated.StrictSegal.spine_spineToSimplex, CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_obj, SimplicialObject.Splitting.PInfty_comp_πSummand_id, const_comp, SSet.S.equivElements_symm_apply_dim, SSet.Truncated.Edge.map_fst, CategoryTheory.SimplicialObject.Truncated.whiskering_map_app_app, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app, AugmentedSimplexCategory.eqToHom_toOrderHom, SSet.Truncated.Edge.CompStruct.d₂, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app, SSet.stdSimplex.map_id, SimplicialObject.Splitting.cofan_inj_eq, SSet.Truncated.Path.map_arrow, Truncated.δ₂_zero_comp_δ₂_two_assoc, const_subinterval_eq, CategoryTheory.CosimplicialObject.augment_hom_app, CategoryTheory.nerve.homEquiv_apply, SSet.Truncated.StrictSegal.spineToSimplex_spine, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand_assoc, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, SSet.Truncated.HomotopyCategory₂.mk_surjective, len_le_of_mono, Hom.mk_toOrderHom_apply, CategoryTheory.SimplicialObject.Truncated.trunc_obj_obj, SimplicialObject.Splitting.IndexSet.eqId_iff_len_eq, CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_obj, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_hom_app, const_fac_thru_zero, SSet.Truncated.Edge.CompStruct.tensor_simplex_snd, SSet.stdSimplex.face_eq_ofSimplex, eq_const_to_zero, Truncated.δ₂_zero_eq_const, SSet.Truncated.Edge.id_tensor_id, SSet.prodStdSimplex.objEquiv_naturality, toTop_obj, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, toTop_map, δ_one_eq_const, SSet.Truncated.spine_map_subinterval, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_left, CategoryTheory.Arrow.cechNerve_obj, isIso_iff_of_epi, toTop₀_map, PartialOrder.mem_nerve_nonDegenerate_iff_injective, congr_toOrderHom_apply, CategoryTheory.nerve.mk₁_homEquiv_apply, CategoryTheory.CosimplicialObject.Truncated.whiskering_map_app_app, SSet.Truncated.HomotopyCategory.mk_surjective, ext_iff, SSet.horn_obj, SSet.Truncated.StrictSegal.spine_δ_arrow_lt, toTop₀_obj, isIso_iff_of_mono, SSet.Truncated.id_app, SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero, SSet.stdSimplex.face_obj, SSet.Truncated.spine_map_vertex, id_toOrderHom, SSet.Truncated.Edge.CompStruct.tensor_simplex_fst, classifyingSpaceUniversalCover_map, SSet.Truncated.Edge.map_associator_hom, len_le_of_epi, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀, SSet.Truncated.Edge.src_eq, SSet.Truncated.rightExtensionInclusion_right_as, SSet.stdSimplex.coe_edge_down_toOrderHom, eqToHom_toOrderHom, SSet.Truncated.StrictSegal.spine_δ_arrow_gt, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀', SSet.stdSimplex.isoNerve_hom_app_apply, SSet.Truncated.StrictSegal.spineInjective, PartialOrder.mem_range_nerve_σ_iff, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, SimplicialObject.Splitting.cofan_inj_πSummand_eq_id, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp, CategoryTheory.SimplicialObject.augment_hom_app, CategoryTheory.SimplicialObject.isCoskeletal_iff, mono_iff_injective, δ_zero_eq_const, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id, SimplicialObject.Split.cofan_inj_naturality_symm_assoc, CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_map_app, SSet.Truncated.Edge.map_whiskerLeft, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id, SSet.const_app, SSet.Truncated.Edge.map_snd, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂, SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk, AlgebraicTopology.DoldKan.Γ₀_map_app, rev_map_apply, Truncated.δ₂_zero_comp_δ₂_two, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk, SSet.Truncated.Edge.map_id, CategoryTheory.SimplicialObject.Truncated.trunc_obj_map, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_right_as, instReflectsIsomorphismsForgetOrderHomFinHAddNatLenOfNat, CategoryTheory.Arrow.mapCechConerve_app, Truncated.δ₂_zero_comp_σ₂_one_assoc, CategoryTheory.Limits.FormalCoproduct.cechFunctor_map_app, SSet.Truncated.StrictSegal.spineToSimplex_vertex, SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero, Truncated.initial_inclusion, SSet.Truncated.StrictSegal.spine_δ_vertex_ge, Truncated.δ₂_one_eq_const, SSet.Truncated.StrictSegal.spineToSimplex_edge, SSet.Truncated.spine_arrow, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃, PartialOrder.mem_nerve_nonDegenerate_iff_strictMono, SSet.Truncated.HomotopyCategory.homToNerveMk_app_one, SSet.prodStdSimplex.objEquiv_map_apply, Truncated.Hom.ext_iff, SSet.Truncated.Edge.mk'_edge, SimplicialObject.Splitting.cofan_inj_comp_app, AlgebraicTopology.DoldKan.Γ₀.map_app, SSet.Truncated.comp_app_assoc, SSet.Truncated.Edge.map_tensorHom, CategoryTheory.Limits.FormalCoproduct.cech_map, SSet.Truncated.StrictSegal.spineToSimplex_arrow, SSet.Truncated.rightExtensionInclusion_left, SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero_assoc, SSet.stdSimplex.const_down_toOrderHom, SSet.Truncated.spine_vertex, CategoryTheory.SimplicialObject.Truncated.trunc_map_app, SSet.Truncated.mapHomotopyCategory_obj, SimplexCategoryGenRel.simplicialEvalσ_of_isAdmissible, SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc, CategoryTheory.nerve_map, SSet.Truncated.Edge.map_edge, SSet.Truncated.Edge.id_edge, Truncated.δ₂_two_comp_σ₂_zero, CategoryTheory.nerve.δ_obj, SimplicialObject.Splitting.decomposition_id, SSet.Truncated.Path.arrow_src, SSet.spine_map_vertex, CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality, SSet.horn.spineId_vertex_coe, mk_len, CategoryTheory.nerve_obj, SSet.Truncated.tensor_map_apply_fst, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_obj, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand, SSet.horn.spineId_arrow_coe, CategoryTheory.SimplicialObject.equivalenceRightToLeft_left, CategoryTheory.SimplicialObject.IsCoskeletal.isRightKanExtension, const_apply, AugmentedSimplexCategory.inl'_eval, SSet.Truncated.Edge.tensor_edge, SSet.Truncated.Path.map_vertex, SSet.Truncated.StrictSegal.spine_δ_arrow_eq, Truncated.δ₂_two_comp_σ₂_zero_assoc, CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_map, CategoryTheory.CosimplicialObject.equivalenceRightToLeft_right_app, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀_assoc, SSet.Subcomplex.liftPath_arrow_coe, SSet.Truncated.HomotopyCategory.BinaryProduct.square, SSet.Truncated.Path₁.arrow_tgt, SSet.Truncated.HomotopyCategory.homToNerveMk_app_edge, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, SSet.Truncated.StrictSegal.spineToSimplex_interval, SSet.Truncated.hom_ext_iff, SimplicialObject.Split.natTransCofanInj_app, toType_apply, SSet.Truncated.Path.arrow_tgt, toCat_obj, CategoryTheory.Arrow.cechNerve_map, concreteCategoryHom_id, skeletalFunctor_obj, SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero_assoc, CategoryTheory.Arrow.cechConerve_map, SSet.Subcomplex.liftPath_vertex_coe, Truncated.δ₂_zero_comp_σ₂_one, SimplicialObject.Splitting.comp_PInfty_eq_zero_iff, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map, CategoryTheory.Idempotents.DoldKan.Γ_map_app, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, comp_toOrderHom, SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero, CategoryTheory.nerve.ext_of_isThin_iff, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁, len_eq_of_isIso, CategoryTheory.Arrow.cechConerve_obj, SSet.Truncated.Path.mk₂_vertex, len_lt_of_mono, SSet.Truncated.IsStrictSegal.spine_bijective, SSet.OneTruncation₂.nerveHomEquiv_apply, skeletalFunctor_map, SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero, SSet.Truncated.Edge.CompStruct.d₀, SSet.Truncated.Edge.map_whiskerRight, SSet.Truncated.comp_app, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, SSet.Truncated.Edge.CompStruct.map_simplex, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id, CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_map, SSet.OneTruncation₂.map_obj, AlgebraicTopology.DoldKan.Γ₂_map_f_app, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_map, CategoryTheory.nerveMap_app, SSet.Truncated.rightExtensionInclusion_hom_app, CategoryTheory.SimplicialObject.augmentedCechNerve_map_left_app, CategoryTheory.nerve.functorOfNerveMap_obj, SSet.Truncated.Path₁.arrow_src, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_map, AugmentedSimplexCategory.inr'_eval, SSet.Truncated.Edge.CompStruct.d₁, Truncated.δ₂_two_comp_σ₂_one, SSet.OneTruncation₂.id_edge, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_obj, toCat_map, CategoryTheory.CosimplicialObject.equivalenceLeftToRight_right, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', CategoryTheory.Limits.FormalCoproduct.cech_obj, SSet.stdSimplex.objEquiv_symm_apply, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc, SSet.Truncated.StrictSegal.spine_δ_vertex_lt, SSet.Truncated.HomotopyCategory.descOfTruncation_obj_mk, SimplicialObject.Split.cofan_inj_naturality_symm, II_obj, SimplicialObject.Splitting.cofan_inj_comp_app_assoc, epi_iff_surjective, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_obj, Truncated.initial_incl, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality_assoc, SSet.StrictSegal.isRightKanExtension, SSet.Truncated.IsStrictSegal.segal, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty, SimplicialObject.Splitting.cofan_inj_eq_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc, CategoryTheory.SimplicialObject.equivalenceLeftToRight_left_app, SSet.Truncated.spine_injective, CategoryTheory.SimplicialObject.Truncated.whiskering_obj_map_app, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_hom_app, SSet.Truncated.Edge.CompStruct.idCompId_simplex, SimplicialObject.Splitting.IndexSet.eqId_iff_len_le, classifyingSpaceUniversalCover_obj, CategoryTheory.Arrow.augmentedCechConerve_hom_app, SSet.Truncated.Edge.tgt_eq, SSet.stdSimplex.isoNerve_inv_app_apply, SSet.Truncated.StrictSegal.spineToSimplex_map
mk 📖	CompOp	—
rec 📖	CompOp	—
smallCategory 📖	CompOp	905 math math: SSet.op_δ, SimplicialObject.Splitting.cofan_inj_πSummand_eq_id_assoc, CategoryTheory.SimplicialObject.id_left_app, δ_comp_δ', SSet.RelativeMorphism.image_le, CategoryTheory.SimplicialObject.whiskering_obj_map_app, mkOfSucc_eq_id, SSet.Subcomplex.preimage_eq_top_iff, CategoryTheory.CosimplicialObject.δ_comp_δ_self_assoc, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_left, Truncated.δ₂_two_comp_σ₂_one_assoc, instNonemptyCarrierObjTopCatToTop₀, SSet.stdSimplex.mem_nonDegenerate_iff_strictMono, SSet.stdSimplex.coe_triangle_down_toOrderHom, CategoryTheory.SimplicialObject.δ_comp_δ_self_assoc, SimplexCategoryGenRel.toSimplexCategory_len, CategoryTheory.CosimplicialObject.whiskering_obj_obj_obj, SSet.Truncated.tensor_map_apply_snd, eq_id_of_isIso, CategoryTheory.CosimplicialObject.comp_app, instSplitEpiCategory, SSet.PtSimplex.RelStruct.δ_map_of_lt, AlgebraicTopology.DoldKan.σ_comp_PInfty_assoc, SimplicialObject.Splitting.IndexSet.epiComp_fst, CategoryTheory.SimplicialObject.δ_comp_δ''_assoc, CategoryTheory.CosimplicialObject.δ_comp_δ_self', const_eq_id, AlgebraicTopology.NormalizedMooreComplex.obj_d, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt, SkeletalFunctor.instEssSurjNonemptyFinLinOrdSkeletalFunctor, SimplicialObject.Splitting.IndexSet.id_fst, CategoryTheory.CosimplicialObject.id_right_app, AugmentedSimplexCategory.inr_comp_associator, SSet.ι₀_snd_assoc, SSet.Subcomplex.mem_ofSimplex_obj_iff, CategoryTheory.CosimplicialObject.δ_comp_δ''_assoc, SSet.degenerate_eq_top_of_hasDimensionLT, SSet.Truncated.mapHomotopyCategory_homMk, CategoryTheory.CosimplicialObject.δ_comp_δ_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp_assoc, CategoryTheory.SimplicialObject.σ_naturality_assoc, CategoryTheory.Arrow.augmentedCechNerve_hom_app, SSet.instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk, SSet.horn.faceSingletonComplIso_inv_ι_assoc, AlgebraicTopology.DoldKan.MorphComponents.preComp_a, CategoryTheory.Arrow.mapCechNerve_app, SSet.degenerate_iff_of_mono, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ, AugmentedSimplexCategory.inclusion_obj, δ_comp_δ'', AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_map_app, SSet.σ_mem_degenerate, SimplicialObject.Splitting.IndexSet.fac_pull_assoc, SSet.ofSimplex_le_skeleton, SSet.Subcomplex.toSSetFunctor_map, SSet.iSup_subcomplexOfSimplex_prod_eq_top, CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_base, SSet.Truncated.Path.mk₂_arrow, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk, Truncated.δ₂_zero_comp_σ₂_zero, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', SSet.stdSimplex.obj₀Equiv_symm_apply, AugmentedSimplexCategory.whiskerLeft_id_star, SSet.finite_iSup_iff, CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_obj, CategoryTheory.nerve.functorOfNerveMap_map, SSet.opFunctorCompOpFunctorIso_inv_app_app, SSet.Truncated.StrictSegal.spine_spineToSimplex, CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_obj, CategoryTheory.cosimplicialSimplicialEquiv_counitIso_hom_app_app, SimplicialObject.Splitting.PInfty_comp_πSummand_id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id_assoc, SSet.Subcomplex.range_eq_ofSimplex, CategoryTheory.CosimplicialObject.δ_comp_δ', const_comp, SSet.spine_map_subinterval, SSet.PtSimplex.MulStruct.δ_map_of_gt, SSet.nonDegenerate_iff_of_mono, δ_comp_σ_of_gt'_assoc, CategoryTheory.simplicialCosimplicialEquiv_counitIso_inv_app_app, SSet.tensorHom_app_apply, CategoryTheory.simplicialCosimplicialEquiv_inverse_map, CategoryTheory.SimplicialObject.Augmented.toArrow_map_right, SimplicialObject.opFunctor_obj_σ, SSet.Edge.map_id, CategoryTheory.nerve.homEquiv_edgeMk_map_nerveMap, SSet.S.equivElements_symm_apply_dim, AugmentedSimplexCategory.inr_comp_inl_comp_associator, SSet.prodStdSimplex.instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat, instFiniteHom, SSet.Truncated.Edge.map_fst, instHasTerminal, SimplexCategoryGenRel.isSplitEpi_toSimplexCategory_map_of_P_σ, SimplicialObject.Splitting.cofan_inj_epi_naturality_assoc, SSet.Subcomplex.image_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_left, SSet.horn.yonedaEquiv_ι, Truncated.Hom.tr_comp, instPathConnectedSpaceCarrierObjTopCatToTop, SSet.Subcomplex.range_eq_top, CategoryTheory.SimplicialObject.Truncated.whiskering_map_app_app, SSet.Finite.instIsFinitelyPresentableObjSimplexCategoryStdSimplex, AugmentedSimplexCategory.inr_comp_inl_comp_associator_assoc, δ_comp_σ_self', CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app, instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex, SSet.Subcomplex.topIso_inv_app_coe, SSet.prodStdSimplex.orderHomOfSimplex_coe, CategoryTheory.CosimplicialObject.σ_naturality_assoc, SimplicialObject.opFunctor_obj_map, AugmentedSimplexCategory.eqToHom_toOrderHom, δ_comp_δ_self', SSet.Truncated.Edge.CompStruct.d₂, SSet.opFunctorCompOpFunctorIso_hom_app_app, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_σ, CategoryTheory.SimplicialObject.Augmented.w₀, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app, AlgebraicTopology.AlternatingCofaceMapComplex.d_eq_unop_d, SSet.Subcomplex.toRange_app_val, Truncated.δ₂_one_comp_σ₂_one, CategoryTheory.SimplicialObject.σ_naturality, CategoryTheory.CosimplicialObject.eqToIso_refl, SSet.RelativeMorphism.Homotopy.h₀_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_map_app, CategoryTheory.SimplicialObject.Augmented.toArrow_map_left, revEquivalence_unitIso, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε, SSet.prodStdSimplex.objEquiv_apply_fst, SSet.stdSimplex.map_id, SimplicialObject.Splitting.cofan_inj_eq, SSet.Truncated.Path.map_arrow, CategoryTheory.SimplicialObject.Augmented.toArrow_obj_left, Truncated.δ₂_zero_comp_δ₂_two_assoc, SSet.exists_nonDegenerate, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_hom_app, const_subinterval_eq, CategoryTheory.SimplicialObject.δ_comp_σ_succ'_assoc, CategoryTheory.SimplicialObject.δ_def, σ_injective, SSet.Truncated.StrictSegal.spineToSimplex_spine, II_σ, SSet.Subcomplex.degenerate_eq_top_iff, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f, δ_comp_σ_self_assoc, AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc, SSet.horn₂₂.sq, SSet.iSup_skeleton, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, SSet.nonDegenerateEquivOfIso_symm_apply_coe, SimplicialObject.opFunctor_map_app, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f, SSet.Truncated.HomotopyCategory₂.mk_surjective, SSet.spine_vertex, CategoryTheory.SimplicialObject.δ_comp_δ_assoc, AlgebraicTopology.DoldKan.comp_P_eq_self_iff, δ_zero_mkOfSucc, SSet.Subcomplex.preimage_min, SSet.Subcomplex.eq_top_iff_of_hasDimensionLT, SSet.stdSimplex.ext_iff, SSet.δ_naturality_apply, CategoryTheory.SimplicialObject.Truncated.trunc_obj_obj, SSet.mem_degenerate_iff_notMem_nonDegenerate, SimplicialObject.Splitting.IndexSet.eqId_iff_len_eq, SSet.opFunctor_map, SimplicialObject.Splitting.IndexSet.ext', CategoryTheory.CosimplicialObject.δ_comp_σ_self', CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_obj, SSet.Subcomplex.topIso_inv_ι, SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_hom_app, const_fac_thru_zero, SSet.Subcomplex.ofSimplexProd_eq_range, SSet.Truncated.Edge.CompStruct.tensor_simplex_snd, δ_comp_σ_succ_assoc, SSet.stdSimplex.face_eq_ofSimplex, SSet.PtSimplex.RelStruct.δ_castSucc_map, CategoryTheory.CosimplicialObject.δ_comp_σ_self_assoc, SSet.stdSimplex.obj₀Equiv_apply, AlgebraicTopology.AlternatingFaceMapComplex.map_f, δ_comp_δ_self, SSet.skeleton_le_skeletonOfMono, SSet.prodStdSimplex.objEquiv_δ_apply, mkOfSucc_subinterval_eq, AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, SSet.op_σ, Truncated.Hom.tr_comp', AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_map, CategoryTheory.CosimplicialObject.id_app, CategoryTheory.SimplicialObject.hom_ext_iff, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, SSet.horn.faceSingletonComplIso_inv_ι, SSet.Subcomplex.toSSetFunctor_obj, δ_comp_σ_of_gt', AlgebraicTopology.alternatingFaceMapComplex_map_f, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ, SSet.hasDimensionLT_subcomplex_top_iff, instSubsingletonHomMkOfNatNat, SSet.Truncated.Edge.id_tensor_id, SSet.Subcomplex.instSubsingletonHomToSSetBot, AugmentedSimplexCategory.instHasInitial, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_obj, SimplicialObject.Splitting.IndexSet.mk_snd_coe, SSet.prodStdSimplex.objEquiv_naturality, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_hom_app, toTop_obj, CategoryTheory.CosimplicialObject.δ_comp_δ, SSet.modelCategoryQuillen.instHasLiftingPropertyιHornHAddNatOfNatOfFibration, SSet.stdSimplex.spineId_arrow_apply_zero, SSet.comp_app_assoc, SSet.nonDegenerate_eq_bot_of_hasDimensionLT, CategoryTheory.CosimplicialObject.comp_right_app, AlgebraicTopology.DoldKan.MorphComponents.preComp_b, CategoryTheory.CosimplicialObject.σ_naturality, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, eq_σ_comp_of_not_injective, toTop_map, instPathConnectedSpaceCarrierObjTopCatToTop₀, SSet.Truncated.spine_map_subinterval, SSet.Subcomplex.eq_top_iff_contains_nonDegenerate, SSet.stdSimplex.range_δ, SSet.PtSimplex.RelStruct.δ_castSucc_map_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero_assoc, AlgebraicTopology.AlternatingFaceMapComplex.d_squared, SSet.PtSimplex.MulStruct.δ_succ_succ_map_assoc, SimplexCategoryGenRel.toSimplexCategory_map_σ, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_left, CategoryTheory.Arrow.cechNerve_obj, isIso_iff_of_epi, SSet.instFiniteElemObjOppositeSimplexCategoryOpMkNonDegenerateOfFinite, SSet.id_app, SSet.spine_arrow, CategoryTheory.SimplicialObject.δ_comp_σ_self'_assoc, SimplicialObject.Splitting.IndexSet.eqId_iff_mono, CategoryTheory.id_app, Truncated.δ₂_zero_comp_σ₂_zero_assoc, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_left, PartialOrder.mem_nerve_degenerate_of_eq, SSet.Augmented.stdSimplex_map_right, SSet.Subcomplex.preimage_range, SSet.Subcomplex.toImage_app_coe, SSet.PtSimplex.MulStruct.δ_succ_succ_map, toTop₀_map, AugmentedSimplexCategory.inl_comp_inl_comp_associator_assoc, PartialOrder.mem_nerve_nonDegenerate_iff_injective, SSet.prodStdSimplex.objEquiv_apply_snd, AlgebraicTopology.DoldKan.Γ₀_obj_map, CategoryTheory.cosimplicialSimplicialEquiv_functor_obj_obj, SSet.S.mk_map_eq_iff_of_mono, SSet.Subcomplex.image_le_iff, CategoryTheory.simplicialCosimplicialEquiv_unitIso_hom_app, mkOfSucc_δ_lt, SSet.Augmented.stdSimplex_obj_left, SSet.hom_ext_iff, SSet.S.le_iff, SSet.hasDimensionLT_iff, CategoryTheory.nerveMap_app_mk₁, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_obj, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, CategoryTheory.CosimplicialObject.Truncated.whiskering_map_app_app, instHasStrongEpiImages, isIso_of_bijective, SSet.instFiniteObjOppositeSimplexCategoryTensorObj, AugmentedSimplexCategory.tensorObj_hom_ext_iff, eq_id_of_epi, CategoryTheory.simplicialCosimplicialEquiv_counitIso_hom_app_app, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero, AugmentedSimplexCategory.inr_comp_associator_assoc, CategoryTheory.SimplicialObject.δ_naturality, SSet.horn.spineId_map_hornInclusion, SSet.Truncated.HomotopyCategory.mk_surjective, isSkeletonOf, SSet.Subcomplex.image_monotone, SSet.horn_obj, AugmentedSimplexCategory.instFullSimplexCategoryInclusion, instNonemptyCarrierObjTopCatToTop, SSet.Truncated.StrictSegal.spine_δ_arrow_lt, CategoryTheory.SimplicialObject.σ_def, SSet.leftUnitor_inv_app_apply, SSet.ι₀_fst_assoc, SSet.ι₁_comp, SSet.skeleton_obj_eq_top, SSet.Subcomplex.yonedaEquiv_coe, SSet.Augmented.StandardSimplex.nonempty_extraDegeneracy_stdSimplex, CategoryTheory.CosimplicialObject.Augmented.leftOp_left_map, SimplicialObject.Splitting.IndexSet.mk_fst, AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero, toTop₀_obj, isIso_iff_of_mono, SSet.instFiniteObjOppositeSimplexCategoryOfFinite, CategoryTheory.cosimplicialSimplicialEquiv_inverse_obj, δ_comp_σ_of_le, SSet.RelativeMorphism.le_preimage, CategoryTheory.CosimplicialObject.δ_naturality_assoc, SSet.Truncated.id_app, SSet.whiskerRight_app_apply, SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero, σ_comp_σ_assoc, SSet.StrictSegal.spineToSimplex_map, SSet.rightUnitor_inv_app_apply, SSet.stdSimplex.face_obj, SSet.stdSimplex.nonDegenerateEquiv_apply_apply, SSet.modelCategoryQuillen.horn_ι_mem_J, factor_δ_spec, SSet.stdSimplex.map_apply, SSet.instHasDimensionLTToSSetBotSubcomplex, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, rev_map_δ, SSet.Truncated.spine_map_vertex, id_toOrderHom, SSet.ι₀_snd, SSet.Truncated.Edge.CompStruct.tensor_simplex_fst, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map, classifyingSpaceUniversalCover_map, SSet.StrictSegal.spineInjective, CategoryTheory.CosimplicialObject.δ_comp_σ_succ_assoc, SSet.degenerate_le_preimage, SSet.Subcomplex.mem_nonDegenerate_iff, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right, toCat.obj_eq_Fin, CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt_assoc, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁_assoc, SSet.mem_skeleton_obj_iff_of_nonDegenerate, SSet.StrictSegal.spineToSimplex_interval, AlgebraicTopology.DoldKan.Γ₂_obj_X_map, SSet.Truncated.Edge.map_associator_hom, SSet.degenerate_zero, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'_assoc, AlgebraicTopology.AlternatingCofaceMapComplex.d_squared, SSet.horn₂₀.sq, SSet.Truncated.Edge.src_eq, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, SSet.stdSimplex.mem_face_iff, CategoryTheory.SimplicialObject.Augmented.rightOp_right_map, SSet.Truncated.rightExtensionInclusion_right_as, CategoryTheory.CosimplicialObject.δ_comp_σ_succ'_assoc, CategoryTheory.CosimplicialObject.δ_comp_δ_self'_assoc, CategoryTheory.CosimplicialObject.δ_comp_σ_of_le, SimplexCategoryGenRel.toSimplexCategory_obj_mk, eq_comp_δ_of_not_surjective', SSet.stdSimplex.coe_edge_down_toOrderHom, CategoryTheory.SimplicialObject.δ_comp_δ'_assoc, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ, CategoryTheory.SimplicialObject.δ_comp_σ_self', eqToHom_toOrderHom, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, revCompRevIso_inv_app, SSet.ι₁_snd_assoc, SimplicialObject.Splitting.ofIso_isColimit', CategoryTheory.CosimplicialObject.Augmented.toArrow_map_right, SSet.horn.edge_coe, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero, diag_subinterval_eq, CategoryTheory.cosimplicialSimplicialEquiv_functor_map_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right, SSet.Truncated.StrictSegal.spine_δ_arrow_gt, SSet.stdSimplex.isoNerve_hom_app_apply, CategoryTheory.CosimplicialObject.δ_comp_δ_self, SSet.Subcomplex.mem_degenerate_iff, AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, AlgebraicTopology.DoldKan.QInfty_f_naturality_assoc, AlgebraicTopology.DoldKan.MorphComponents.postComp_a, SSet.stdSimplex.faceSingletonComplIso_hom_ι, CategoryTheory.SimplicialObject.δ_comp_δ', SSet.ι₁_app_fst, SSet.skeleton_succ, SSet.Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top, AugmentedSimplexCategory.inl_comp_tensorHom, SSet.ι₁_snd, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_inv_app, SSet.Truncated.StrictSegal.spineInjective, PartialOrder.mem_range_nerve_σ_iff, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_inv_left_app, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, SimplicialObject.Splitting.cofan_inj_πSummand_eq_id, SSet.Path.map_arrow, AugmentedSimplexCategory.id_star_whiskerRight, CategoryTheory.cosimplicialSimplicialEquiv_counitIso_inv_app_app, CategoryTheory.CosimplicialObject.Augmented.toArrow_map_left, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp, CategoryTheory.SimplicialObject.isCoskeletal_iff, CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_hom_left_app, SSet.whiskerLeft_app_apply, mono_iff_injective, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id, SSet.comp_app, CategoryTheory.SimplicialObject.δ_comp_σ_succ', AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, skeletal, SSet.Augmented.stdSimplex_obj_right, SimplicialObject.Splitting.IndexSet.fac_pull, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right, SSet.StrictSegal.spineToSimplex_spine, SSet.Subcomplex.prod_obj, SimplicialObject.Split.cofan_inj_naturality_symm_assoc, CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_map_app, SimplicialObject.Splitting.ofIso_ι, SkeletalFunctor.isEquivalence, SSet.Truncated.Edge.map_whiskerLeft, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id, SimplicialObject.opFunctor_obj_δ, CategoryTheory.SimplicialObject.σ_comp_σ, Truncated.Hom.tr_id, SSet.const_app, SSet.Truncated.Edge.map_snd, AlgebraicTopology.DoldKan.MorphComponents.id_φ, SSet.stdSimplex.instFiniteObjOppositeSimplexCategory, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂, CategoryTheory.SimplicialObject.δ_comp_δ'', AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app, SSet.Subcomplex.preimage_obj, SSet.Subcomplex.image_top, SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk, AlgebraicTopology.DoldKan.Γ₀_map_app, CategoryTheory.SimplicialObject.comp_left_app, rev_map_apply, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, Truncated.δ₂_zero_comp_δ₂_two, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk, SSet.Truncated.Edge.map_id, SSet.orderEmbeddingN_apply, CategoryTheory.SimplicialObject.Truncated.trunc_obj_map, δ_comp_δ_self'_assoc, SimplicialObject.Split.Hom.comm, CategoryTheory.SimplicialObject.whiskering_map_app_app, CategoryTheory.SimplicialObject.Augmented.rightOp_right_obj, AlgebraicTopology.DoldKan.QInfty_f_naturality, rev_map_σ, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_right_as, SSet.face_le_horn, SSet.Subcomplex.image_preimage_le, SimplicialObject.Splitting.IndexSet.id_snd_coe, instReflectsIsomorphismsForgetOrderHomFinHAddNatLenOfNat, CategoryTheory.Arrow.mapCechConerve_app, CategoryTheory.SimplicialObject.δ_comp_δ_self, δ_comp_σ_of_gt, Truncated.δ₂_zero_comp_σ₂_one_assoc, CategoryTheory.Limits.FormalCoproduct.cechFunctor_map_app, SSet.Truncated.StrictSegal.spineToSimplex_vertex, CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_hom_right_app, CategoryTheory.cosimplicialSimplicialEquiv_unitIso_hom_app, AugmentedSimplexCategory.inl_comp_inl_comp_associator, SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero, CategoryTheory.CosimplicialObject.δ_comp_σ_succ', Truncated.initial_inclusion, AlgebraicTopology.DoldKan.P_f_naturality_assoc, SSet.Truncated.StrictSegal.spine_δ_vertex_ge, SSet.StrictSegal.spineToSimplex_edge, CategoryTheory.SimplicialObject.Augmented.whiskering_map_app_left, SSet.PtSimplex.MulStruct.δ_map_of_lt, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ, SSet.Truncated.StrictSegal.spineToSimplex_edge, SSet.Truncated.spine_arrow, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, SSet.stdSimplex.instHasDimensionLEObjSimplexCategoryMk, SSet.stdSimplex.monotone_apply, SSet.horn.faceι_ι, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃, δ_comp_δ, SSet.S.equivElements_apply_fst, SSet.Subcomplex.ofSimplex_le_iff, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, SSet.N.le_iff_exists_mono, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, PartialOrder.mem_nerve_nonDegenerate_iff_strictMono, Truncated.δ₂_one_comp_σ₂_zero, SimplicialObject.Splitting.IndexSet.instEpiSimplexCategoryE, SSet.Subcomplex.image_ofSimplex, SSet.Truncated.HomotopyCategory.homToNerveMk_app_one, SSet.prodStdSimplex.objEquiv_map_apply, SSet.Subcomplex.le_iff_of_hasDimensionLT, Truncated.Hom.ext_iff, SSet.stdSimplex.objEquiv_symm_mem_nonDegenerate_iff_mono, SSet.Truncated.Edge.mk'_edge, SimplicialObject.Splitting.cofan_inj_comp_app, rev_obj, CategoryTheory.comp_app, AlgebraicTopology.NormalizedMooreComplex.d_squared, CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_right, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁, instBalanced, SSet.nonDegenerate_iff_of_isIso, CategoryTheory.SimplicialObject.δ_comp_σ_of_le, AlgebraicTopology.DoldKan.Γ₀.map_app, AugmentedSimplexCategory.instFaithfulSimplexCategoryInclusion, CategoryTheory.hoFunctor.isIso_prodComparison_stdSimplex, instEpiσ, CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_hom, SSet.Truncated.comp_app_assoc, SSet.Truncated.Edge.map_tensorHom, CategoryTheory.Limits.FormalCoproduct.cech_map, SSet.Truncated.StrictSegal.spineToSimplex_arrow, SSet.horn.edge₃_coe_down, SSet.Truncated.rightExtensionInclusion_left, SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero_assoc, CategoryTheory.SimplicialObject.δ_comp_σ_self, SSet.stdSimplex.const_down_toOrderHom, SSet.Subcomplex.topIso_inv_ι_assoc, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_X, SSet.horn₂₁.isPushout, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt_assoc, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ_assoc, SSet.Subcomplex.fromPreimage_app_coe, AlgebraicTopology.DoldKan.MorphComponents.preComp_φ, SSet.horn_eq_iSup, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self_assoc, AlgebraicTopology.DoldKan.Γ₀_obj_obj, CategoryTheory.cosimplicialSimplicialEquiv_unitIso_inv_app, AlgebraicTopology.DoldKan.Q_f_naturality_assoc, SSet.Truncated.spine_vertex, revCompRevIso_hom_app, SSet.stdSimplex.obj₀Equiv_symm_mem_face_iff, SimplicialObject.opFunctorCompOpFunctorIso_hom_app_app, SSet.range_eq_iSup_sigma_ι, SSet.Subcomplex.BicartSq.isPushout, CategoryTheory.CosimplicialObject.δ_comp_σ_succ, SSet.Subcomplex.PairingCore.nonDegenerate₂, CategoryTheory.SimplicialObject.Truncated.trunc_map_app, SSet.prodStdSimplex.instFiniteTensorObjObjSimplexCategoryStdSimplexMk, SSet.stdSimplex.objEquiv_symm_comp, CategoryTheory.SimplicialObject.Augmented.w₀_assoc, δ_injective, CategoryTheory.SimplicialObject.whiskering_obj_obj_obj, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self, δ_comp_δ_self_assoc, CategoryTheory.Idempotents.DoldKan.Γ_obj_map, SSet.Truncated.mapHomotopyCategory_obj, SimplexCategoryGenRel.simplicialEvalσ_of_isAdmissible, SSet.ι₀_comp_assoc, SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc, CategoryTheory.nerve_map, SSet.Truncated.Edge.map_edge, CategoryTheory.CosimplicialObject.σ_comp_σ, SSet.skeletonOfMono_zero, AugmentedSimplexCategory.tensor_id, SSet.Truncated.Edge.id_edge, CategoryTheory.SimplicialObject.δ_naturality_assoc, CategoryTheory.simplicialCosimplicialEquiv_inverse_obj, Truncated.δ₂_two_comp_σ₂_zero, SSet.ι₀_comp, CategoryTheory.Idempotents.DoldKan.Γ_obj_obj, CategoryTheory.simplicialCosimplicialEquiv_functor_map_app, CategoryTheory.SimplicialObject.δ_comp_σ_succ, SSet.IsStrictSegal.segal, AlgebraicTopology.NormalizedMooreComplex.map_f, CategoryTheory.CosimplicialObject.δ_comp_δ'', CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt'_assoc, CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt, SSet.Augmented.stdSimplex_obj_hom_app, CategoryTheory.SimplicialObject.whiskering_obj_obj_map, SSet.horn.faceι_ι_assoc, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app, SimplicialObject.Splitting.decomposition_id, SSet.Truncated.Path.arrow_src, SSet.spine_map_vertex, CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0, SSet.RelativeMorphism.Homotopy.h₁_assoc, AlgebraicTopology.DoldKan.MorphComponents.postComp_b, SSet.hasDimensionLT_iSup_iff, SSet.Subcomplex.le_iff_contains_nonDegenerate, AugmentedSimplexCategory.inclusion_map, eq_σ_comp_of_not_injective', SimplexCategoryGenRel.toSimplexCategory_map_δ, SSet.stdSimplex.yonedaEquiv_map, SSet.RelativeMorphism.Homotopy.ofEq_h, instHasStrongEpiMonoFactorisations, SSet.horn_obj_zero, AlgebraicTopology.DoldKan.hσ'_eq, CategoryTheory.SimplicialObject.eqToIso_refl, SSet.mem_skeleton, AlgebraicTopology.DoldKan.MorphComponents.id_a, SSet.horn.spineId_vertex_coe, CategoryTheory.CosimplicialObject.δ_comp_δ'_assoc, SSet.rightUnitor_hom_app_apply, SSet.iSup_skeletonOfMono, δ_one_mkOfSucc, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right, revEquivalence_functor, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε_assoc, CategoryTheory.CosimplicialObject.whiskering_obj_map_app, CategoryTheory.nerve_obj, SSet.Truncated.tensor_map_apply_fst, rev_map_rev_map, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_obj, AlgebraicTopology.DoldKan.PInfty_f_naturality, SSet.horn.multicoequalizerDiagram, mkOfSucc_δ_gt, SSet.horn.spineId_arrow_coe, CategoryTheory.SimplicialObject.equivalenceRightToLeft_left, SSet.skeletonOfMono_obj_eq_top, δ_comp_σ_of_gt_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.of_comp, SimplicialObject.opFunctorCompOpFunctorIso_inv_app_app, SSet.iSup_range_eq_top_of_isColimit, CategoryTheory.SimplicialObject.IsCoskeletal.isRightKanExtension, SSet.stdSimplex.objEquiv_toOrderHom_apply, AugmentedSimplexCategory.tensorHom_id, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀, SSet.ι₁_fst, SSet.const_comp, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.const_s, CategoryTheory.simplicialCosimplicialEquiv_unitIso_inv_app, CategoryTheory.CosimplicialObject.σ_comp_σ_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, SSet.Truncated.Edge.tensor_edge, SSet.Edge.map_edge, SSet.Edge.CompStruct.map_simplex, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, SSet.Truncated.Path.map_vertex, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, SSet.mem_nonDegenerate_iff_notMem_degenerate, δ_comp_σ_succ', SSet.finite_subcomplex_top_iff, SSet.Truncated.StrictSegal.spine_δ_arrow_eq, Truncated.δ₂_two_comp_σ₂_zero_assoc, SSet.Subcomplex.preimage_max, δ_comp_σ_self, SSet.Subcomplex.mem_ofSimplex_obj, CategoryTheory.CosimplicialObject.δ_comp_σ_self, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt', SSet.Subcomplex.image_le_range, CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_map, CategoryTheory.CosimplicialObject.equivalenceRightToLeft_right_app, CategoryTheory.CosimplicialObject.hom_ext_iff, AlgebraicTopology.DoldKan.N₂_obj_p_f, SSet.Truncated.HomotopyCategory.BinaryProduct.square, SSet.horn₂₀.isPushout, SSet.stdSimplex.ofSimplex_yonedaEquiv_δ, AlgebraicTopology.DoldKan.σ_comp_PInfty, AlgebraicTopology.NormalizedMooreComplex.obj_X, SSet.mem_skeletonOfMono_obj_iff_of_nonDegenerate, SSet.Truncated.Path₁.arrow_tgt, SSet.S.equivElements_apply_snd, CategoryTheory.SimplicialObject.δ_comp_σ_self_assoc, AlgebraicTopology.NormalizedMooreComplex.objX_add_one, SimplicialObject.Splitting.IndexSet.epiComp_snd_coe, AlgebraicTopology.DoldKan.N₂_obj_X_X, SimplicialObject.Split.Hom.comm_assoc, SSet.HasDimensionLT.degenerate_eq_top, CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_succ, SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left, SSet.Quasicategory.hornFilling, SSet.stdSimplex.instFiniteObjSimplexCategory, δ_comp_σ_of_le_assoc, SSet.stdSimplex.objMk_apply, SSet.Truncated.HomotopyCategory.homToNerveMk_app_edge, SSet.Subcomplex.PairingCore.notMem₁, AlgebraicTopology.DoldKan.MorphComponents.postComp_φ, CategoryTheory.SimplicialObject.Augmented.rightOp_hom_app, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, SSet.Truncated.StrictSegal.spineToSimplex_interval, SSet.Truncated.hom_ext_iff, SSet.N.mk_surjective, Truncated.δ₂_one_comp_σ₂_one_assoc, SimplicialObject.Split.natTransCofanInj_app, CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_map, AlgebraicTopology.DoldKan.Γ₀.obj_map, CategoryTheory.SimplicialObject.δ_comp_δ_self', Truncated.Hom.tr_comp_assoc, CategoryTheory.CosimplicialObject.Augmented.leftOp_left_obj, toType_apply, AugmentedSimplexCategory.id_tensorHom, SSet.RelativeMorphism.Homotopy.h₀, CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_inv_right_app, iso_eq_iso_refl, SSet.Truncated.Path.arrow_tgt, SSet.mem_degenerate_iff, SSet.nonDegenerateEquivOfIso_apply_coe, SSet.S.le_iff_nonempty_hom, SSet.modelCategoryQuillen.boundary_ι_mem_I, toCat_obj, CategoryTheory.CosimplicialObject.whiskering_map_app_app, SSet.Augmented.stdSimplex_map_left, CategoryTheory.Arrow.cechNerve_map, SSet.stdSimplex.faceSingletonComplIso_hom_ι_assoc, SSet.RelativeMorphism.Homotopy.precomp_h, concreteCategoryHom_id, SSet.N.le_iff, AlgebraicTopology.NormalizedMooreComplex.objX_zero, SSet.ι₀_fst, skeletalFunctor_obj, AlgebraicTopology.DoldKan.N₂_obj_X_d, CategoryTheory.SimplicialObject.Augmented.toArrow_obj_hom, SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero_assoc, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left, CategoryTheory.CosimplicialObject.Augmented.whiskering_map_app_right, SSet.associator_hom_app_apply, CategoryTheory.SimplicialObject.σ_comp_σ_assoc, CategoryTheory.Arrow.cechConerve_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, SSet.image_degenerate_le, AlgebraicTopology.DoldKan.karoubi_PInfty_f, Truncated.δ₂_zero_comp_σ₂_one, SSet.boundary_eq_iSup, SSet.RelativeMorphism.Homotopy.h₁, SimplicialObject.Splitting.comp_PInfty_eq_zero_iff, SSet.stdSimplex.spineId_vertex, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map, CategoryTheory.simplicialCosimplicialEquiv_functor_obj_obj, CategoryTheory.Idempotents.DoldKan.Γ_map_app, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, SSet.degenerate_eq_iUnion_range_σ, comp_toOrderHom, SSet.RelativeMorphism.Homotopy.postcomp_h, CategoryTheory.simplicialToCosimplicialAugmented_map_right, CategoryTheory.CosimplicialObject.whiskering_obj_obj_map, CategoryTheory.CosimplicialObject.Augmented.leftOp_hom_app, SSet.S.equivElements_symm_apply_simplex, SSet.stdSimplex.face_inter_face, SSet.stdSimplex.mem_nonDegenerate_iff_mono, SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁, SSet.N.nonDegenerate, CategoryTheory.Arrow.cechConerve_obj, SSet.Truncated.Path.mk₂_vertex, SSet.horn₂₂.isPushout, eq_id_of_mono, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, SSet.yonedaEquiv_comp, SSet.Truncated.IsStrictSegal.spine_bijective, SSet.op_map, SimplicialObject.Splitting.IndexSet.eqId_iff_eq, SkeletalFunctor.instFaithfulNonemptyFinLinOrdSkeletalFunctor, SSet.stdSimplex.spineId_arrow_apply_one, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq, SSet.Quasicategory.hornFilling', AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_map, CategoryTheory.cosimplicialToSimplicialAugmented_map, SSet.OneTruncation₂.nerveHomEquiv_apply, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right, SSet.StrictSegalCore.map_mkOfSucc_zero_spineToSimplex, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, SSet.RelativeMorphism.Homotopy.rel, SSet.horn.primitiveEdge_coe_down, AugmentedSimplexCategory.inr_comp_tensorHom, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ_assoc, SSet.StrictSegal.spineToSimplex_arrow, SSet.Subcomplex.range_eq_top_iff, skeletalFunctor_map, SSet.StrictSegal.spine_spineToSimplex, SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero, SSet.Truncated.Edge.CompStruct.d₀, SSet.Truncated.Edge.map_whiskerRight, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_right_app, SSet.Truncated.comp_app, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, SSet.Subcomplex.preimage_iSup, CategoryTheory.cosimplicialSimplicialEquiv_inverse_map, CategoryTheory.SimplicialObject.δ_comp_σ_of_le_assoc, CategoryTheory.SimplicialObject.δ_comp_δ, SSet.Path.map_vertex, SSet.Truncated.Edge.CompStruct.map_simplex, revEquivalence_inverse, SSet.stdSimplex.face_le_face_iff, AugmentedSimplexCategory.inl_comp_tensorHom_assoc, AlgebraicTopology.DoldKan.Γ₂_obj_X_obj, SSet.RelativeMorphism.Homotopy.refl_h, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id, mkOfSucc_δ_eq, SSet.PtSimplex.RelStruct.δ_succ_map, CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_map, CategoryTheory.CosimplicialObject.δ_naturality, SSet.OneTruncation₂.map_obj, SSet.σ_naturality_apply, AlgebraicTopology.DoldKan.Γ₂_map_f_app, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_map, skeletalFunctor.coe_map, AugmentedSimplexCategory.inr_comp_tensorHom_assoc, AlgebraicTopology.DoldKan.decomposition_Q, revEquivalence_counitIso, AlgebraicTopology.DoldKan.σ_comp_P_eq_zero, SSet.S.mk_map_le, SSet.S.IsUniquelyCodimOneFace.existsUnique_δ_cast_simplex, AlgebraicTopology.DoldKan.Γ₀.obj_obj, CategoryTheory.nerveMap_app, δ_comp_σ_succ'_assoc, SSet.Truncated.rightExtensionInclusion_hom_app, CategoryTheory.SimplicialObject.augmentedCechNerve_map_left_app, AlgebraicTopology.AlternatingFaceMapComplex.obj_X, CategoryTheory.nerve.functorOfNerveMap_obj, SSet.N.iSup_subcomplex_eq_top, SSet.Truncated.Path₁.arrow_src, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_map, AlgebraicTopology.DoldKan.Q_f_naturality, SSet.ι₁_fst_assoc, Truncated.δ₂_one_comp_σ₂_zero_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id, SSet.Truncated.Edge.CompStruct.d₁, SSet.Subcomplex.PairingCore.notMem₂, Truncated.δ₂_two_comp_σ₂_one, SSet.Subcomplex.topIso_hom, SSet.OneTruncation₂.id_edge, AlgebraicTopology.inclusionOfMooreComplexMap_f, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_obj, SSet.horn.ι_ι_assoc, toCat_map, AlgebraicTopology.alternatingFaceMapComplex_obj_X, eq_of_one_to_one, CategoryTheory.CosimplicialObject.equivalenceLeftToRight_right, SSet.leftUnitor_hom_app_apply, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', σ_comp_σ, hom_zero_zero, CategoryTheory.Limits.FormalCoproduct.cech_obj, CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_map_app, SSet.stdSimplex.objEquiv_symm_apply, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc, instEpiFactorThruImage, AlgebraicTopology.DoldKan.N₂_map_f_f, SSet.Subcomplex.PairingCore.nonDegenerate₁, SSet.KanComplex.hornFilling, SSet.PtSimplex.RelStruct.δ_map_of_gt, SSet.Truncated.StrictSegal.spine_δ_vertex_lt, eq_comp_δ_of_not_surjective, SSet.nondegenerate_zero, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app, Truncated.Hom.tr_comp'_assoc, AlgebraicTopology.DoldKan.P_f_naturality, SSet.Truncated.HomotopyCategory.descOfTruncation_obj_mk, SSet.S.IsUniquelyCodimOneFace.iff, AlgebraicTopology.DoldKan.MorphComponents.id_b, SimplicialObject.Split.cofan_inj_naturality_symm, AlgebraicTopology.DoldKan.factors_normalizedMooreComplex_PInfty, II_obj, SSet.associator_inv_app_apply, SSet.stdSimplex.nonDegenerateEquiv_symm_apply_coe, SSet.horn.ι_ι, SimplicialObject.Splitting.cofan_inj_comp_app_assoc, CategoryTheory.cosimplicialSimplicialEquiv_functor_obj_map, epi_iff_surjective, CategoryTheory.SimplicialObject.δ_comp_σ_succ_assoc, SSet.RelativeMorphism.map_coe, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_obj, SSet.Subcomplex.N.notMem, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map, Truncated.initial_incl, AlgebraicTopology.DoldKan.hσ'_naturality, AlgebraicTopology.DoldKan.P_add_Q_f, SSet.horn.const_val_apply, AlgebraicTopology.DoldKan.hσ'_eq', SSet.StrictSegal.isRightKanExtension, SSet.Truncated.IsStrictSegal.segal, AlgebraicTopology.DoldKan.HigherFacesVanish.induction, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty, CategoryTheory.nerveMap_app_mk₀, SSet.horn₂₁.sq, SSet.Subcomplex.image_iSup, SimplicialObject.Splitting.cofan_inj_eq_assoc, II_δ, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app, SkeletalFunctor.instFullNonemptyFinLinOrdSkeletalFunctor, SSet.horn.primitiveTriangle_coe, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc, δ_comp_σ_succ, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_obj, CategoryTheory.SimplicialObject.equivalenceLeftToRight_left_app, SSet.degenerate_iff_of_isIso, SSet.stdSimplex.face_singleton_compl, SSet.ι₀_app_fst, CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt', SSet.Truncated.spine_injective, AugmentedSimplexCategory.tensorHom_comp_tensorHom, CategoryTheory.SimplicialObject.Truncated.whiskering_obj_map_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_obj, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_hom_app, SimplicialObject.Splitting.cofan_inj_epi_naturality, instMonoδ, SSet.Truncated.Edge.CompStruct.idCompId_simplex, SimplexCategoryGenRel.isSplitMono_toSimplexCategory_map_of_P_δ, SimplicialObject.Splitting.IndexSet.eqId_iff_len_le, SSet.range_eq_iSup_of_isColimit, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app, SSet.Subcomplex.preimage_iInf, CategoryTheory.simplicialCosimplicialEquiv_functor_obj_map, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_left, SSet.S.le_def, CategoryTheory.CosimplicialObject.δ_comp_σ_self'_assoc, classifyingSpaceUniversalCover_obj, SSet.ι₁_comp_assoc, SSet.skeletonOfMono_succ, CategoryTheory.Arrow.augmentedCechConerve_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app, CategoryTheory.SimplicialObject.δ_comp_δ_self'_assoc, SSet.PtSimplex.RelStruct.δ_succ_map_assoc, δ_comp_σ_self'_assoc, SSet.StrictSegal.spineToSimplex_vertex, SSet.Truncated.Edge.tgt_eq, SSet.stdSimplex.isoNerve_inv_app_apply, SSet.Truncated.StrictSegal.spineToSimplex_map, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map, SSet.RelativeMorphism.Homotopy.rel_assoc, SSet.skeleton_zero, CategoryTheory.CosimplicialObject.δ_comp_σ_of_le_assoc, morphismProperty_eq_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_toOrderHom 📖	mathematical	—	Hom.toOrderHom CategoryTheory.CategoryStruct.comp SimplexCategory CategoryTheory.Category.toCategoryStruct smallCategory OrderHom.comp len PartialOrder.toPreorder Fin.instPartialOrder	—	—
ext 📖	—	len	—	—	—
ext_iff 📖	mathematical	—	len	—	ext
id_toOrderHom 📖	mathematical	—	Hom.toOrderHom CategoryTheory.CategoryStruct.id SimplexCategory CategoryTheory.Category.toCategoryStruct smallCategory OrderHom.id len PartialOrder.toPreorder Fin.instPartialOrder	—	—
len_mk 📖	mathematical	—	len	—	—
mk_len 📖	mathematical	—	len	—	—

SimplexCategory.Hom

Definitions

Name	Category	Theorems
comp 📖	CompOp	—
id 📖	CompOp	—
mk 📖	CompOp	—
toOrderHom 📖	CompOp	39 math math: SSet.stdSimplex.coe_triangle_down_toOrderHom, SimplexCategory.eq_const_of_zero, SimplexCategory.const_comp, AugmentedSimplexCategory.eqToHom_toOrderHom, SimplexCategory.mkOfSucc_homToOrderHom_one, mk_toOrderHom_apply, SSet.prodStdSimplex.objEquiv_naturality, SimplexCategory.congr_toOrderHom_apply, SSet.stdSimplex.face_obj, SSet.Truncated.spine_map_vertex, SimplexCategory.id_toOrderHom, classifyingSpaceUniversalCover_map, SSet.stdSimplex.coe_edge_down_toOrderHom, SimplexCategory.eqToHom_toOrderHom, SimplexCategory.mono_iff_injective, ext_iff, SimplexCategory.rev_map_apply, SimplexCategory.mkOfSucc_homToOrderHom_zero, SSet.prodStdSimplex.objEquiv_map_apply, SimplexCategory.Truncated.Hom.ext_iff, CategoryTheory.Limits.FormalCoproduct.cech_map, SSet.stdSimplex.const_down_toOrderHom, SimplexCategoryGenRel.simplicialEvalσ_of_isAdmissible, toOrderHom_mk, SSet.spine_map_vertex, mk_toOrderHom, SSet.stdSimplex.objEquiv_toOrderHom_apply, SimplexCategory.const_apply, AugmentedSimplexCategory.inl'_eval, CategoryTheory.Arrow.cechNerve_map, CategoryTheory.Arrow.cechConerve_map, SimplexCategory.comp_toOrderHom, SimplexCategory.skeletalFunctor_map, SimplexCategory.skeletalFunctor.coe_map, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_map, AugmentedSimplexCategory.inr'_eval, SimplexCategory.toCat_map, SSet.stdSimplex.objEquiv_symm_apply, SimplexCategory.epi_iff_surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	toOrderHom	—	—	ext'
ext' 📖	—	toOrderHom	—	—	—
ext_iff 📖	mathematical	—	toOrderHom	—	ext
mk_toOrderHom 📖	mathematical	—	toOrderHom	—	—
mk_toOrderHom_apply 📖	mathematical	—	DFunLike.coe OrderHom SimplexCategory.len PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike toOrderHom	—	—
toOrderHom_mk 📖	mathematical	—	toOrderHom	—	—

SimplexCategory.Truncated

Definitions

Name	Category	Theorems
incl 📖	CompOp	10 math math: SSet.Truncated.Path.mk₂_arrow, CategoryTheory.SimplicialObject.Truncated.trunc_obj_obj, CategoryTheory.SimplicialObject.Truncated.trunc_obj_map, CategoryTheory.SimplicialObject.Truncated.trunc_map_app, SSet.horn.spineId_vertex_coe, SSet.horn.spineId_arrow_coe, SSet.Subcomplex.liftPath_arrow_coe, SSet.Subcomplex.liftPath_vertex_coe, SSet.Truncated.Path.mk₂_vertex, initial_incl
inclCompInclusion 📖	CompOp	—
inclusion 📖	CompOp	20 math math: SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_hom_app, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_left, SSet.Truncated.rightExtensionInclusion_right_as, CategoryTheory.SimplicialObject.isCoskeletal_iff, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_right_as, initial_inclusion, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃, SSet.Truncated.rightExtensionInclusion_left, SSet.horn.spineId_vertex_coe, SSet.horn.spineId_arrow_coe, CategoryTheory.SimplicialObject.IsCoskeletal.isRightKanExtension, SSet.Subcomplex.liftPath_arrow_coe, SSet.Subcomplex.liftPath_vertex_coe, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁, SSet.OneTruncation₂.nerveHomEquiv_apply, SSet.Truncated.rightExtensionInclusion_hom_app, SSet.StrictSegal.isRightKanExtension
instInhabited 📖	CompOp	—
mkNotation 📖	CompOp	—
tacticTrunc 📖	CompOp	—

SimplexCategory.Truncated.Hom

Definitions

Name	Category	Theorems
tr 📖	CompOp	23 math math: tr_comp, tr_comp', SimplexCategory.Truncated.δ₂_zero_eq_const, SSet.Truncated.spine_map_subinterval, SSet.Truncated.StrictSegal.spine_δ_arrow_lt, SSet.Truncated.StrictSegal.spine_δ_arrow_gt, tr_id, SSet.Truncated.StrictSegal.spineToSimplex_vertex, SSet.Truncated.StrictSegal.spine_δ_vertex_ge, SimplexCategory.Truncated.δ₂_one_eq_const, SSet.Truncated.StrictSegal.spineToSimplex_edge, SSet.Truncated.spine_arrow, SSet.Truncated.StrictSegal.spineToSimplex_arrow, SSet.Truncated.spine_vertex, SSet.Truncated.Path.arrow_src, SSet.Truncated.StrictSegal.spine_δ_arrow_eq, SSet.Truncated.Path₁.arrow_tgt, SSet.Truncated.StrictSegal.spineToSimplex_interval, tr_comp_assoc, SSet.Truncated.Path.arrow_tgt, SSet.Truncated.Path₁.arrow_src, SSet.Truncated.StrictSegal.spine_δ_vertex_lt, tr_comp'_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	SimplexCategory.Hom.toOrderHom CategoryTheory.ObjectProperty.FullSubcategory.obj SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	—	CategoryTheory.ObjectProperty.hom_ext SimplexCategory.Hom.ext
ext_iff 📖	mathematical	—	SimplexCategory.Hom.toOrderHom CategoryTheory.ObjectProperty.FullSubcategory.obj SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	ext
tr_comp 📖	mathematical	SimplexCategory.len	tr CategoryTheory.CategoryStruct.comp SimplexCategory CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category	—	—
tr_comp' 📖	mathematical	SimplexCategory.len	tr CategoryTheory.ObjectProperty.FullSubcategory.obj SimplexCategory SimplexCategory.smallCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category	—	—
tr_comp'_assoc 📖	mathematical	SimplexCategory.len	CategoryTheory.CategoryStruct.comp CategoryTheory.ObjectProperty.FullSubcategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category tr CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory.obj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tr_comp'
tr_comp_assoc 📖	mathematical	SimplexCategory.len	CategoryTheory.CategoryStruct.comp CategoryTheory.ObjectProperty.FullSubcategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category tr	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tr_comp
tr_id 📖	mathematical	SimplexCategory.len	tr CategoryTheory.CategoryStruct.id SimplexCategory CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category	—	—

SimplexCategory.Truncated.inclusion

Definitions

Name	Category	Theorems
fullyFaithful 📖	CompOp	—

Simplicial

Definitions

Name	Category	Theorems
«term⦋_⦌» 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
SimplexCategory 📖	CompOp	915 math math: SSet.op_δ, SimplicialObject.Splitting.cofan_inj_πSummand_eq_id_assoc, CategoryTheory.SimplicialObject.id_left_app, SimplexCategory.δ_comp_δ', SSet.RelativeMorphism.image_le, CategoryTheory.SimplicialObject.whiskering_obj_map_app, SimplexCategory.mkOfSucc_eq_id, SSet.Subcomplex.preimage_eq_top_iff, CategoryTheory.CosimplicialObject.δ_comp_δ_self_assoc, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_left, SimplexCategory.Truncated.δ₂_two_comp_σ₂_one_assoc, SimplexCategory.instNonemptyCarrierObjTopCatToTop₀, SSet.stdSimplex.mem_nonDegenerate_iff_strictMono, SSet.stdSimplex.coe_triangle_down_toOrderHom, CategoryTheory.SimplicialObject.δ_comp_δ_self_assoc, SimplexCategoryGenRel.toSimplexCategory_len, CategoryTheory.CosimplicialObject.whiskering_obj_obj_obj, SSet.Truncated.tensor_map_apply_snd, SimplexCategory.eq_id_of_isIso, CategoryTheory.CosimplicialObject.comp_app, CategoryTheory.nerve.σ_obj, SimplexCategory.instSplitEpiCategory, SSet.PtSimplex.RelStruct.δ_map_of_lt, AlgebraicTopology.DoldKan.σ_comp_PInfty_assoc, SimplicialObject.Splitting.IndexSet.epiComp_fst, CategoryTheory.SimplicialObject.δ_comp_δ''_assoc, CategoryTheory.CosimplicialObject.δ_comp_δ_self', SimplexCategory.const_eq_id, AlgebraicTopology.NormalizedMooreComplex.obj_d, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt, SimplexCategory.SkeletalFunctor.instEssSurjNonemptyFinLinOrdSkeletalFunctor, SimplicialObject.Splitting.IndexSet.id_fst, CategoryTheory.CosimplicialObject.id_right_app, AugmentedSimplexCategory.inr_comp_associator, SSet.ι₀_snd_assoc, SSet.Subcomplex.mem_ofSimplex_obj_iff, CategoryTheory.CosimplicialObject.δ_comp_δ''_assoc, SSet.degenerate_eq_top_of_hasDimensionLT, SSet.Truncated.mapHomotopyCategory_homMk, CategoryTheory.CosimplicialObject.δ_comp_δ_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp_assoc, CategoryTheory.SimplicialObject.σ_naturality_assoc, CategoryTheory.Arrow.augmentedCechNerve_hom_app, SSet.instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk, SSet.horn.faceSingletonComplIso_inv_ι_assoc, AlgebraicTopology.DoldKan.MorphComponents.preComp_a, CategoryTheory.Arrow.mapCechNerve_app, SSet.degenerate_iff_of_mono, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ, AugmentedSimplexCategory.inclusion_obj, SimplexCategory.δ_comp_δ'', AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_map_app, SSet.σ_mem_degenerate, SimplicialObject.Splitting.IndexSet.fac_pull_assoc, SSet.ofSimplex_le_skeleton, SSet.Subcomplex.toSSetFunctor_map, SSet.iSup_subcomplexOfSimplex_prod_eq_top, CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_base, SSet.Truncated.Path.mk₂_arrow, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk, SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', SSet.stdSimplex.obj₀Equiv_symm_apply, AugmentedSimplexCategory.whiskerLeft_id_star, SSet.finite_iSup_iff, AlgebraicTopology.DoldKan.HigherFacesVanish.on_Γ₀_summand_id, CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_obj, CategoryTheory.nerve.functorOfNerveMap_map, SSet.opFunctorCompOpFunctorIso_inv_app_app, SSet.Truncated.StrictSegal.spine_spineToSimplex, CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_obj, CategoryTheory.cosimplicialSimplicialEquiv_counitIso_hom_app_app, SimplicialObject.Splitting.PInfty_comp_πSummand_id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id_assoc, SSet.Subcomplex.range_eq_ofSimplex, CategoryTheory.CosimplicialObject.δ_comp_δ', SimplexCategory.const_comp, SSet.spine_map_subinterval, SSet.PtSimplex.MulStruct.δ_map_of_gt, SSet.nonDegenerate_iff_of_mono, SimplexCategory.δ_comp_σ_of_gt'_assoc, CategoryTheory.simplicialCosimplicialEquiv_counitIso_inv_app_app, SSet.tensorHom_app_apply, CategoryTheory.simplicialCosimplicialEquiv_inverse_map, CategoryTheory.SimplicialObject.Augmented.toArrow_map_right, SimplicialObject.opFunctor_obj_σ, SSet.Edge.map_id, CategoryTheory.nerve.homEquiv_edgeMk_map_nerveMap, SSet.S.equivElements_symm_apply_dim, AugmentedSimplexCategory.inr_comp_inl_comp_associator, SSet.prodStdSimplex.instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat, SimplexCategory.instFiniteHom, SSet.Truncated.Edge.map_fst, SimplexCategory.instHasTerminal, SimplexCategoryGenRel.isSplitEpi_toSimplexCategory_map_of_P_σ, SimplicialObject.Splitting.cofan_inj_epi_naturality_assoc, SSet.Subcomplex.image_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_left, SSet.horn.yonedaEquiv_ι, SimplexCategory.Truncated.Hom.tr_comp, SimplexCategory.instPathConnectedSpaceCarrierObjTopCatToTop, SSet.Subcomplex.range_eq_top, CategoryTheory.SimplicialObject.Truncated.whiskering_map_app_app, SSet.Finite.instIsFinitelyPresentableObjSimplexCategoryStdSimplex, AugmentedSimplexCategory.inr_comp_inl_comp_associator_assoc, SimplexCategory.δ_comp_σ_self', CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app, instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex, SSet.Subcomplex.topIso_inv_app_coe, SSet.prodStdSimplex.orderHomOfSimplex_coe, CategoryTheory.CosimplicialObject.σ_naturality_assoc, SimplicialObject.opFunctor_obj_map, SimplexCategory.δ_comp_δ_self', SSet.Truncated.Edge.CompStruct.d₂, SSet.opFunctorCompOpFunctorIso_hom_app_app, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_σ, CategoryTheory.SimplicialObject.Augmented.w₀, SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app, AlgebraicTopology.AlternatingCofaceMapComplex.d_eq_unop_d, SSet.Subcomplex.toRange_app_val, SimplexCategory.Truncated.δ₂_one_comp_σ₂_one, CategoryTheory.SimplicialObject.σ_naturality, CategoryTheory.CosimplicialObject.eqToIso_refl, SSet.RelativeMorphism.Homotopy.h₀_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_map_app, CategoryTheory.SimplicialObject.Augmented.toArrow_map_left, SimplexCategory.revEquivalence_unitIso, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε, SSet.prodStdSimplex.objEquiv_apply_fst, SSet.stdSimplex.map_id, SimplicialObject.Splitting.cofan_inj_eq, SSet.Truncated.Path.map_arrow, CategoryTheory.SimplicialObject.Augmented.toArrow_obj_left, SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two_assoc, SSet.exists_nonDegenerate, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_hom_app, SimplexCategory.const_subinterval_eq, CategoryTheory.nerve.homEquiv_apply, CategoryTheory.SimplicialObject.δ_comp_σ_succ'_assoc, CategoryTheory.SimplicialObject.δ_def, SimplexCategory.σ_injective, SSet.Truncated.StrictSegal.spineToSimplex_spine, SimplexCategory.II_σ, SSet.Subcomplex.degenerate_eq_top_iff, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f, SimplexCategory.δ_comp_σ_self_assoc, AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc, SSet.horn₂₂.sq, SSet.iSup_skeleton, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, SSet.nonDegenerateEquivOfIso_symm_apply_coe, SimplicialObject.opFunctor_map_app, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f, SSet.Truncated.HomotopyCategory₂.mk_surjective, SSet.spine_vertex, CategoryTheory.SimplicialObject.δ_comp_δ_assoc, AlgebraicTopology.DoldKan.comp_P_eq_self_iff, SimplexCategory.δ_zero_mkOfSucc, SSet.Subcomplex.preimage_min, SSet.Subcomplex.eq_top_iff_of_hasDimensionLT, SSet.stdSimplex.ext_iff, SSet.δ_naturality_apply, CategoryTheory.SimplicialObject.Truncated.trunc_obj_obj, SSet.mem_degenerate_iff_notMem_nonDegenerate, SimplicialObject.Splitting.IndexSet.eqId_iff_len_eq, SSet.opFunctor_map, SimplicialObject.Splitting.IndexSet.ext', CategoryTheory.CosimplicialObject.δ_comp_σ_self', CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_obj, SSet.Subcomplex.topIso_inv_ι, SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_hom_app, SimplexCategory.const_fac_thru_zero, SSet.Subcomplex.ofSimplexProd_eq_range, SSet.Truncated.Edge.CompStruct.tensor_simplex_snd, SimplexCategory.δ_comp_σ_succ_assoc, SSet.stdSimplex.face_eq_ofSimplex, SSet.PtSimplex.RelStruct.δ_castSucc_map, CategoryTheory.CosimplicialObject.δ_comp_σ_self_assoc, SSet.stdSimplex.obj₀Equiv_apply, AlgebraicTopology.AlternatingFaceMapComplex.map_f, SimplexCategory.δ_comp_δ_self, SSet.skeleton_le_skeletonOfMono, SSet.prodStdSimplex.objEquiv_δ_apply, SimplexCategory.mkOfSucc_subinterval_eq, AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, SSet.op_σ, SimplexCategory.Truncated.Hom.tr_comp', AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_map, CategoryTheory.CosimplicialObject.id_app, CategoryTheory.SimplicialObject.hom_ext_iff, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, SSet.horn.faceSingletonComplIso_inv_ι, SSet.Subcomplex.toSSetFunctor_obj, SimplexCategory.δ_comp_σ_of_gt', AlgebraicTopology.alternatingFaceMapComplex_map_f, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ, SSet.hasDimensionLT_subcomplex_top_iff, SimplexCategory.instSubsingletonHomMkOfNatNat, SSet.Truncated.Edge.id_tensor_id, SSet.Subcomplex.instSubsingletonHomToSSetBot, AugmentedSimplexCategory.instHasInitial, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_obj, SimplicialObject.Splitting.IndexSet.mk_snd_coe, SSet.prodStdSimplex.objEquiv_naturality, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_hom_app, SimplexCategory.toTop_obj, CategoryTheory.CosimplicialObject.δ_comp_δ, SSet.modelCategoryQuillen.instHasLiftingPropertyιHornHAddNatOfNatOfFibration, SSet.stdSimplex.spineId_arrow_apply_zero, SSet.comp_app_assoc, SSet.nonDegenerate_eq_bot_of_hasDimensionLT, CategoryTheory.CosimplicialObject.comp_right_app, AlgebraicTopology.DoldKan.MorphComponents.preComp_b, CategoryTheory.CosimplicialObject.σ_naturality, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, SimplexCategory.eq_σ_comp_of_not_injective, SimplexCategory.toTop_map, SimplexCategory.instPathConnectedSpaceCarrierObjTopCatToTop₀, SSet.Truncated.spine_map_subinterval, SSet.Subcomplex.eq_top_iff_contains_nonDegenerate, SSet.stdSimplex.range_δ, SSet.PtSimplex.RelStruct.δ_castSucc_map_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero_assoc, AlgebraicTopology.AlternatingFaceMapComplex.d_squared, SSet.PtSimplex.MulStruct.δ_succ_succ_map_assoc, SimplexCategoryGenRel.toSimplexCategory_map_σ, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_left, CategoryTheory.Arrow.cechNerve_obj, SimplexCategory.isIso_iff_of_epi, SSet.instFiniteElemObjOppositeSimplexCategoryOpMkNonDegenerateOfFinite, SSet.id_app, SSet.spine_arrow, CategoryTheory.SimplicialObject.δ_comp_σ_self'_assoc, SimplicialObject.Splitting.IndexSet.eqId_iff_mono, CategoryTheory.id_app, SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero_assoc, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_left, SSet.Augmented.stdSimplex_map_right, SSet.Subcomplex.preimage_range, SSet.Subcomplex.toImage_app_coe, SSet.PtSimplex.MulStruct.δ_succ_succ_map, SimplexCategory.toTop₀_map, AugmentedSimplexCategory.inl_comp_inl_comp_associator_assoc, PartialOrder.mem_nerve_nonDegenerate_iff_injective, SSet.prodStdSimplex.objEquiv_apply_snd, AlgebraicTopology.DoldKan.Γ₀_obj_map, CategoryTheory.cosimplicialSimplicialEquiv_functor_obj_obj, SSet.S.mk_map_eq_iff_of_mono, SSet.Subcomplex.image_le_iff, CategoryTheory.simplicialCosimplicialEquiv_unitIso_hom_app, SimplexCategory.mkOfSucc_δ_lt, CategoryTheory.nerve.mk₁_homEquiv_apply, SSet.Augmented.stdSimplex_obj_left, SSet.hom_ext_iff, SSet.S.le_iff, SSet.hasDimensionLT_iff, CategoryTheory.nerveMap_app_mk₁, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_obj, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, CategoryTheory.CosimplicialObject.Truncated.whiskering_map_app_app, SimplexCategory.instHasStrongEpiImages, SimplexCategory.isIso_of_bijective, SSet.instFiniteObjOppositeSimplexCategoryTensorObj, AugmentedSimplexCategory.tensorObj_hom_ext_iff, SimplexCategory.eq_id_of_epi, CategoryTheory.simplicialCosimplicialEquiv_counitIso_hom_app_app, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero, AugmentedSimplexCategory.inr_comp_associator_assoc, CategoryTheory.SimplicialObject.δ_naturality, SSet.horn.spineId_map_hornInclusion, SSet.Truncated.HomotopyCategory.mk_surjective, SimplexCategory.isSkeletonOf, SSet.Subcomplex.image_monotone, SSet.horn_obj, AugmentedSimplexCategory.instFullSimplexCategoryInclusion, SimplexCategory.instNonemptyCarrierObjTopCatToTop, SSet.Truncated.StrictSegal.spine_δ_arrow_lt, CategoryTheory.SimplicialObject.σ_def, SSet.leftUnitor_inv_app_apply, SSet.ι₀_fst_assoc, SSet.ι₁_comp, SSet.skeleton_obj_eq_top, SSet.Subcomplex.yonedaEquiv_coe, SSet.Augmented.StandardSimplex.nonempty_extraDegeneracy_stdSimplex, CategoryTheory.CosimplicialObject.Augmented.leftOp_left_map, SimplicialObject.Splitting.IndexSet.mk_fst, AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero, SimplexCategory.toTop₀_obj, SimplexCategory.isIso_iff_of_mono, SSet.instFiniteObjOppositeSimplexCategoryOfFinite, CategoryTheory.cosimplicialSimplicialEquiv_inverse_obj, SimplexCategory.δ_comp_σ_of_le, SSet.RelativeMorphism.le_preimage, CategoryTheory.CosimplicialObject.δ_naturality_assoc, SSet.Truncated.id_app, SSet.whiskerRight_app_apply, SimplexCategory.σ_comp_σ_assoc, SSet.StrictSegal.spineToSimplex_map, SSet.rightUnitor_inv_app_apply, SSet.stdSimplex.face_obj, SSet.stdSimplex.nonDegenerateEquiv_apply_apply, SSet.modelCategoryQuillen.horn_ι_mem_J, SimplexCategory.factor_δ_spec, SSet.stdSimplex.map_apply, SSet.instHasDimensionLTToSSetBotSubcomplex, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, SimplexCategory.rev_map_δ, SSet.Truncated.spine_map_vertex, SimplexCategory.id_toOrderHom, SSet.ι₀_snd, SSet.Truncated.Edge.CompStruct.tensor_simplex_fst, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map, classifyingSpaceUniversalCover_map, SSet.StrictSegal.spineInjective, CategoryTheory.CosimplicialObject.δ_comp_σ_succ_assoc, SSet.degenerate_le_preimage, SSet.Subcomplex.mem_nonDegenerate_iff, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right, SimplexCategory.toCat.obj_eq_Fin, CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt_assoc, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁_assoc, SSet.mem_skeleton_obj_iff_of_nonDegenerate, SSet.StrictSegal.spineToSimplex_interval, AlgebraicTopology.DoldKan.Γ₂_obj_X_map, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, SSet.Truncated.Edge.map_associator_hom, SSet.degenerate_zero, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'_assoc, AlgebraicTopology.AlternatingCofaceMapComplex.d_squared, SSet.horn₂₀.sq, SSet.Truncated.Edge.src_eq, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, SSet.stdSimplex.mem_face_iff, CategoryTheory.SimplicialObject.Augmented.rightOp_right_map, SSet.Truncated.rightExtensionInclusion_right_as, CategoryTheory.CosimplicialObject.δ_comp_σ_succ'_assoc, CategoryTheory.CosimplicialObject.δ_comp_δ_self'_assoc, CategoryTheory.CosimplicialObject.δ_comp_σ_of_le, SimplexCategoryGenRel.toSimplexCategory_obj_mk, SimplexCategory.eq_comp_δ_of_not_surjective', SSet.stdSimplex.coe_edge_down_toOrderHom, CategoryTheory.SimplicialObject.δ_comp_δ'_assoc, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ, CategoryTheory.SimplicialObject.δ_comp_σ_self', SimplexCategory.eqToHom_toOrderHom, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, SimplexCategory.revCompRevIso_inv_app, SSet.ι₁_snd_assoc, SimplicialObject.Splitting.ofIso_isColimit', CategoryTheory.CosimplicialObject.Augmented.toArrow_map_right, SSet.horn.edge_coe, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero, SimplexCategory.diag_subinterval_eq, CategoryTheory.cosimplicialSimplicialEquiv_functor_map_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right, SSet.Truncated.StrictSegal.spine_δ_arrow_gt, SSet.stdSimplex.isoNerve_hom_app_apply, CategoryTheory.CosimplicialObject.δ_comp_δ_self, SSet.Subcomplex.mem_degenerate_iff, AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, AlgebraicTopology.DoldKan.QInfty_f_naturality_assoc, AlgebraicTopology.DoldKan.MorphComponents.postComp_a, SSet.stdSimplex.faceSingletonComplIso_hom_ι, CategoryTheory.SimplicialObject.δ_comp_δ', SSet.ι₁_app_fst, SSet.skeleton_succ, SSet.Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top, AugmentedSimplexCategory.inl_comp_tensorHom, SSet.ι₁_snd, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_inv_app, SSet.Truncated.StrictSegal.spineInjective, PartialOrder.mem_range_nerve_σ_iff, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_inv_left_app, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, SimplicialObject.Splitting.cofan_inj_πSummand_eq_id, SSet.Path.map_arrow, AugmentedSimplexCategory.id_star_whiskerRight, CategoryTheory.cosimplicialSimplicialEquiv_counitIso_inv_app_app, CategoryTheory.CosimplicialObject.Augmented.toArrow_map_left, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp, CategoryTheory.SimplicialObject.isCoskeletal_iff, CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_hom_left_app, SSet.whiskerLeft_app_apply, SimplexCategory.mono_iff_injective, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id, SSet.comp_app, CategoryTheory.SimplicialObject.δ_comp_σ_succ', AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, SimplexCategory.skeletal, SSet.Augmented.stdSimplex_obj_right, SimplicialObject.Splitting.IndexSet.fac_pull, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right, SSet.StrictSegal.spineToSimplex_spine, SSet.Subcomplex.prod_obj, SimplicialObject.Split.cofan_inj_naturality_symm_assoc, CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_map_app, SimplicialObject.Splitting.ofIso_ι, SimplexCategory.SkeletalFunctor.isEquivalence, SSet.Truncated.Edge.map_whiskerLeft, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id, SimplicialObject.opFunctor_obj_δ, CategoryTheory.SimplicialObject.σ_comp_σ, SimplexCategory.Truncated.Hom.tr_id, SSet.const_app, SSet.Truncated.Edge.map_snd, AlgebraicTopology.DoldKan.MorphComponents.id_φ, SSet.stdSimplex.instFiniteObjOppositeSimplexCategory, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂, CategoryTheory.SimplicialObject.δ_comp_δ'', AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app, SSet.Subcomplex.preimage_obj, SSet.Subcomplex.image_top, SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk, AlgebraicTopology.DoldKan.Γ₀_map_app, CategoryTheory.SimplicialObject.comp_left_app, SimplexCategory.rev_map_apply, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk, SSet.Truncated.Edge.map_id, SSet.orderEmbeddingN_apply, CategoryTheory.SimplicialObject.Truncated.trunc_obj_map, SimplexCategory.δ_comp_δ_self'_assoc, SimplicialObject.Split.Hom.comm, CategoryTheory.SimplicialObject.whiskering_map_app_app, CategoryTheory.SimplicialObject.Augmented.rightOp_right_obj, AlgebraicTopology.DoldKan.QInfty_f_naturality, SimplexCategory.rev_map_σ, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_right_as, SSet.face_le_horn, SSet.Subcomplex.image_preimage_le, SimplicialObject.Splitting.IndexSet.id_snd_coe, SimplexCategory.instReflectsIsomorphismsForgetOrderHomFinHAddNatLenOfNat, CategoryTheory.Arrow.mapCechConerve_app, CategoryTheory.SimplicialObject.δ_comp_δ_self, SimplexCategory.δ_comp_σ_of_gt, SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one_assoc, CategoryTheory.Limits.FormalCoproduct.cechFunctor_map_app, SSet.Truncated.StrictSegal.spineToSimplex_vertex, CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_hom_right_app, CategoryTheory.cosimplicialSimplicialEquiv_unitIso_hom_app, AugmentedSimplexCategory.inl_comp_inl_comp_associator, SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero, CategoryTheory.CosimplicialObject.δ_comp_σ_succ', SimplexCategory.Truncated.initial_inclusion, AlgebraicTopology.DoldKan.P_f_naturality_assoc, SSet.Truncated.StrictSegal.spine_δ_vertex_ge, SSet.StrictSegal.spineToSimplex_edge, CategoryTheory.SimplicialObject.Augmented.whiskering_map_app_left, SSet.PtSimplex.MulStruct.δ_map_of_lt, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ, SSet.Truncated.StrictSegal.spineToSimplex_edge, SSet.Truncated.spine_arrow, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, SSet.stdSimplex.instHasDimensionLEObjSimplexCategoryMk, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, SSet.stdSimplex.monotone_apply, SSet.horn.faceι_ι, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃, SimplexCategory.δ_comp_δ, SSet.S.equivElements_apply_fst, SSet.Subcomplex.ofSimplex_le_iff, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, SSet.N.le_iff_exists_mono, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, PartialOrder.mem_nerve_nonDegenerate_iff_strictMono, SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero, SimplicialObject.Splitting.IndexSet.instEpiSimplexCategoryE, SSet.Subcomplex.image_ofSimplex, SSet.Truncated.HomotopyCategory.homToNerveMk_app_one, SSet.prodStdSimplex.objEquiv_map_apply, SSet.Subcomplex.le_iff_of_hasDimensionLT, SimplexCategory.Truncated.Hom.ext_iff, SSet.stdSimplex.objEquiv_symm_mem_nonDegenerate_iff_mono, SSet.Truncated.Edge.mk'_edge, SimplicialObject.Splitting.cofan_inj_comp_app, SimplexCategory.rev_obj, CategoryTheory.comp_app, AlgebraicTopology.NormalizedMooreComplex.d_squared, CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_right, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁, SimplexCategory.instBalanced, SSet.nonDegenerate_iff_of_isIso, CategoryTheory.SimplicialObject.δ_comp_σ_of_le, AlgebraicTopology.DoldKan.Γ₀.map_app, AugmentedSimplexCategory.instFaithfulSimplexCategoryInclusion, CategoryTheory.hoFunctor.isIso_prodComparison_stdSimplex, SimplexCategory.instEpiσ, CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_hom, SSet.Truncated.comp_app_assoc, SSet.Truncated.Edge.map_tensorHom, CategoryTheory.Limits.FormalCoproduct.cech_map, SSet.Truncated.StrictSegal.spineToSimplex_arrow, SSet.horn.edge₃_coe_down, SSet.Truncated.rightExtensionInclusion_left, SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero_assoc, CategoryTheory.SimplicialObject.δ_comp_σ_self, SSet.stdSimplex.const_down_toOrderHom, SSet.Subcomplex.topIso_inv_ι_assoc, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_X, SSet.horn₂₁.isPushout, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt_assoc, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ_assoc, SSet.Subcomplex.fromPreimage_app_coe, AlgebraicTopology.DoldKan.MorphComponents.preComp_φ, SSet.horn_eq_iSup, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self_assoc, AlgebraicTopology.DoldKan.Γ₀_obj_obj, CategoryTheory.cosimplicialSimplicialEquiv_unitIso_inv_app, AlgebraicTopology.DoldKan.Q_f_naturality_assoc, SSet.Truncated.spine_vertex, SimplexCategory.revCompRevIso_hom_app, SSet.stdSimplex.obj₀Equiv_symm_mem_face_iff, SimplicialObject.opFunctorCompOpFunctorIso_hom_app_app, SSet.range_eq_iSup_sigma_ι, SSet.Subcomplex.BicartSq.isPushout, CategoryTheory.CosimplicialObject.δ_comp_σ_succ, SSet.Subcomplex.PairingCore.nonDegenerate₂, CategoryTheory.SimplicialObject.Truncated.trunc_map_app, SSet.prodStdSimplex.instFiniteTensorObjObjSimplexCategoryStdSimplexMk, SSet.stdSimplex.objEquiv_symm_comp, CategoryTheory.SimplicialObject.Augmented.w₀_assoc, SimplexCategory.δ_injective, CategoryTheory.SimplicialObject.whiskering_obj_obj_obj, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self, SimplexCategory.δ_comp_δ_self_assoc, CategoryTheory.Idempotents.DoldKan.Γ_obj_map, SSet.Truncated.mapHomotopyCategory_obj, SimplexCategoryGenRel.simplicialEvalσ_of_isAdmissible, SSet.ι₀_comp_assoc, SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc, CategoryTheory.nerve_map, SSet.Truncated.Edge.map_edge, CategoryTheory.CosimplicialObject.σ_comp_σ, SSet.skeletonOfMono_zero, AugmentedSimplexCategory.tensor_id, SSet.Truncated.Edge.id_edge, CategoryTheory.SimplicialObject.δ_naturality_assoc, CategoryTheory.simplicialCosimplicialEquiv_inverse_obj, SimplexCategory.Truncated.δ₂_two_comp_σ₂_zero, SSet.ι₀_comp, CategoryTheory.nerve.δ_obj, CategoryTheory.Idempotents.DoldKan.Γ_obj_obj, CategoryTheory.simplicialCosimplicialEquiv_functor_map_app, CategoryTheory.SimplicialObject.δ_comp_σ_succ, SSet.IsStrictSegal.segal, AlgebraicTopology.NormalizedMooreComplex.map_f, CategoryTheory.CosimplicialObject.δ_comp_δ'', CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt'_assoc, CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt, SSet.Augmented.stdSimplex_obj_hom_app, CategoryTheory.SimplicialObject.whiskering_obj_obj_map, SSet.horn.faceι_ι_assoc, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app, SimplicialObject.Splitting.decomposition_id, SSet.Truncated.Path.arrow_src, SSet.spine_map_vertex, CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0, SSet.RelativeMorphism.Homotopy.h₁_assoc, AlgebraicTopology.DoldKan.MorphComponents.postComp_b, SSet.hasDimensionLT_iSup_iff, SSet.Subcomplex.le_iff_contains_nonDegenerate, AugmentedSimplexCategory.inclusion_map, SimplexCategory.eq_σ_comp_of_not_injective', SimplexCategoryGenRel.toSimplexCategory_map_δ, SSet.stdSimplex.yonedaEquiv_map, SSet.RelativeMorphism.Homotopy.ofEq_h, SimplexCategory.instHasStrongEpiMonoFactorisations, SSet.horn_obj_zero, AlgebraicTopology.DoldKan.hσ'_eq, CategoryTheory.SimplicialObject.eqToIso_refl, SSet.mem_skeleton, AlgebraicTopology.DoldKan.MorphComponents.id_a, SSet.horn.spineId_vertex_coe, CategoryTheory.CosimplicialObject.δ_comp_δ'_assoc, SSet.rightUnitor_hom_app_apply, SSet.iSup_skeletonOfMono, SimplexCategory.δ_one_mkOfSucc, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right, SimplexCategory.revEquivalence_functor, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε_assoc, CategoryTheory.CosimplicialObject.whiskering_obj_map_app, CategoryTheory.nerve_obj, SSet.Truncated.tensor_map_apply_fst, SimplexCategory.rev_map_rev_map, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_obj, AlgebraicTopology.DoldKan.PInfty_f_naturality, SSet.horn.multicoequalizerDiagram, SimplexCategory.mkOfSucc_δ_gt, SSet.horn.spineId_arrow_coe, CategoryTheory.SimplicialObject.equivalenceRightToLeft_left, SSet.skeletonOfMono_obj_eq_top, SimplexCategory.δ_comp_σ_of_gt_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.of_comp, SimplicialObject.opFunctorCompOpFunctorIso_inv_app_app, SSet.iSup_range_eq_top_of_isColimit, CategoryTheory.SimplicialObject.IsCoskeletal.isRightKanExtension, SSet.stdSimplex.objEquiv_toOrderHom_apply, AugmentedSimplexCategory.tensorHom_id, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀, SSet.ι₁_fst, SSet.const_comp, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.const_s, CategoryTheory.simplicialCosimplicialEquiv_unitIso_inv_app, CategoryTheory.CosimplicialObject.σ_comp_σ_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, SSet.Truncated.Edge.tensor_edge, SSet.Edge.map_edge, SSet.Edge.CompStruct.map_simplex, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, SSet.Truncated.Path.map_vertex, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, SSet.mem_nonDegenerate_iff_notMem_degenerate, SimplexCategory.δ_comp_σ_succ', SSet.finite_subcomplex_top_iff, SSet.Truncated.StrictSegal.spine_δ_arrow_eq, SimplexCategory.Truncated.δ₂_two_comp_σ₂_zero_assoc, SSet.Subcomplex.preimage_max, SimplexCategory.δ_comp_σ_self, SSet.Subcomplex.mem_ofSimplex_obj, CategoryTheory.CosimplicialObject.δ_comp_σ_self, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt', SSet.Subcomplex.image_le_range, CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_map, CategoryTheory.CosimplicialObject.equivalenceRightToLeft_right_app, CategoryTheory.CosimplicialObject.hom_ext_iff, AlgebraicTopology.DoldKan.N₂_obj_p_f, SSet.Truncated.HomotopyCategory.BinaryProduct.square, SSet.horn₂₀.isPushout, SSet.stdSimplex.ofSimplex_yonedaEquiv_δ, AlgebraicTopology.DoldKan.σ_comp_PInfty, AlgebraicTopology.NormalizedMooreComplex.obj_X, SSet.mem_skeletonOfMono_obj_iff_of_nonDegenerate, SSet.Truncated.Path₁.arrow_tgt, SSet.S.equivElements_apply_snd, CategoryTheory.SimplicialObject.δ_comp_σ_self_assoc, AlgebraicTopology.NormalizedMooreComplex.objX_add_one, SimplicialObject.Splitting.IndexSet.epiComp_snd_coe, AlgebraicTopology.DoldKan.N₂_obj_X_X, SimplicialObject.Split.Hom.comm_assoc, SSet.HasDimensionLT.degenerate_eq_top, CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_succ, SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left, SSet.Quasicategory.hornFilling, SSet.stdSimplex.instFiniteObjSimplexCategory, SimplexCategory.δ_comp_σ_of_le_assoc, SSet.stdSimplex.objMk_apply, SSet.Truncated.HomotopyCategory.homToNerveMk_app_edge, SSet.Subcomplex.PairingCore.notMem₁, AlgebraicTopology.DoldKan.MorphComponents.postComp_φ, CategoryTheory.SimplicialObject.Augmented.rightOp_hom_app, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, SSet.Truncated.StrictSegal.spineToSimplex_interval, SSet.Truncated.hom_ext_iff, SSet.N.mk_surjective, SimplexCategory.Truncated.δ₂_one_comp_σ₂_one_assoc, SimplicialObject.Split.natTransCofanInj_app, CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_map, AlgebraicTopology.DoldKan.Γ₀.obj_map, CategoryTheory.SimplicialObject.δ_comp_δ_self', SimplexCategory.Truncated.Hom.tr_comp_assoc, CategoryTheory.CosimplicialObject.Augmented.leftOp_left_obj, SimplexCategory.toType_apply, AugmentedSimplexCategory.id_tensorHom, SSet.RelativeMorphism.Homotopy.h₀, CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_inv_right_app, SimplexCategory.iso_eq_iso_refl, SSet.Truncated.Path.arrow_tgt, SSet.mem_degenerate_iff, SSet.nonDegenerateEquivOfIso_apply_coe, SSet.S.le_iff_nonempty_hom, SSet.modelCategoryQuillen.boundary_ι_mem_I, SimplexCategory.toCat_obj, CategoryTheory.CosimplicialObject.whiskering_map_app_app, SSet.Augmented.stdSimplex_map_left, CategoryTheory.Arrow.cechNerve_map, SSet.stdSimplex.faceSingletonComplIso_hom_ι_assoc, SSet.RelativeMorphism.Homotopy.precomp_h, SimplexCategory.concreteCategoryHom_id, SSet.N.le_iff, AlgebraicTopology.NormalizedMooreComplex.objX_zero, SSet.ι₀_fst, SimplexCategory.skeletalFunctor_obj, AlgebraicTopology.DoldKan.N₂_obj_X_d, CategoryTheory.SimplicialObject.Augmented.toArrow_obj_hom, SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero_assoc, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left, CategoryTheory.CosimplicialObject.Augmented.whiskering_map_app_right, SSet.associator_hom_app_apply, CategoryTheory.SimplicialObject.σ_comp_σ_assoc, CategoryTheory.Arrow.cechConerve_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, SSet.image_degenerate_le, AlgebraicTopology.DoldKan.karoubi_PInfty_f, SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one, SSet.boundary_eq_iSup, SSet.RelativeMorphism.Homotopy.h₁, SimplicialObject.Splitting.comp_PInfty_eq_zero_iff, SSet.stdSimplex.spineId_vertex, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map, CategoryTheory.simplicialCosimplicialEquiv_functor_obj_obj, CategoryTheory.Idempotents.DoldKan.Γ_map_app, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, SSet.degenerate_eq_iUnion_range_σ, SimplexCategory.comp_toOrderHom, SSet.RelativeMorphism.Homotopy.postcomp_h, SimplicialObject.Splitting.cofan_inj_id, CategoryTheory.simplicialToCosimplicialAugmented_map_right, CategoryTheory.CosimplicialObject.whiskering_obj_obj_map, CategoryTheory.CosimplicialObject.Augmented.leftOp_hom_app, SSet.S.equivElements_symm_apply_simplex, SSet.stdSimplex.face_inter_face, SSet.stdSimplex.mem_nonDegenerate_iff_mono, SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero, CategoryTheory.nerve.ext_of_isThin_iff, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁, SSet.N.nonDegenerate, CategoryTheory.Arrow.cechConerve_obj, SSet.Truncated.Path.mk₂_vertex, SSet.horn₂₂.isPushout, SimplexCategory.eq_id_of_mono, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, SSet.yonedaEquiv_comp, SSet.Truncated.IsStrictSegal.spine_bijective, SSet.op_map, SimplicialObject.Splitting.IndexSet.eqId_iff_eq, SimplexCategory.SkeletalFunctor.instFaithfulNonemptyFinLinOrdSkeletalFunctor, SSet.stdSimplex.spineId_arrow_apply_one, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq, SSet.Quasicategory.hornFilling', AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_map, CategoryTheory.cosimplicialToSimplicialAugmented_map, SSet.OneTruncation₂.nerveHomEquiv_apply, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right, SSet.StrictSegalCore.map_mkOfSucc_zero_spineToSimplex, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, SSet.RelativeMorphism.Homotopy.rel, SSet.horn.primitiveEdge_coe_down, AugmentedSimplexCategory.inr_comp_tensorHom, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ_assoc, SSet.StrictSegal.spineToSimplex_arrow, SSet.Subcomplex.range_eq_top_iff, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, SimplexCategory.skeletalFunctor_map, SSet.StrictSegal.spine_spineToSimplex, SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero, SSet.Truncated.Edge.CompStruct.d₀, SSet.Truncated.Edge.map_whiskerRight, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_right_app, SSet.Truncated.comp_app, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, SSet.Subcomplex.preimage_iSup, CategoryTheory.cosimplicialSimplicialEquiv_inverse_map, CategoryTheory.SimplicialObject.δ_comp_σ_of_le_assoc, CategoryTheory.SimplicialObject.δ_comp_δ, SSet.Path.map_vertex, SSet.Truncated.Edge.CompStruct.map_simplex, SimplexCategory.revEquivalence_inverse, SSet.stdSimplex.face_le_face_iff, AugmentedSimplexCategory.inl_comp_tensorHom_assoc, AlgebraicTopology.DoldKan.Γ₂_obj_X_obj, SSet.RelativeMorphism.Homotopy.refl_h, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id, SimplexCategory.mkOfSucc_δ_eq, SSet.PtSimplex.RelStruct.δ_succ_map, CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_map, CategoryTheory.CosimplicialObject.δ_naturality, SSet.OneTruncation₂.map_obj, SSet.σ_naturality_apply, AlgebraicTopology.DoldKan.Γ₂_map_f_app, SSet.Truncated.HomotopyCategory.BinaryProduct.functor_map, SimplexCategory.skeletalFunctor.coe_map, AugmentedSimplexCategory.inr_comp_tensorHom_assoc, AlgebraicTopology.DoldKan.decomposition_Q, SimplexCategory.revEquivalence_counitIso, AlgebraicTopology.DoldKan.σ_comp_P_eq_zero, SSet.S.mk_map_le, SSet.S.IsUniquelyCodimOneFace.existsUnique_δ_cast_simplex, AlgebraicTopology.DoldKan.Γ₀.obj_obj, CategoryTheory.nerveMap_app, SimplexCategory.δ_comp_σ_succ'_assoc, SSet.Truncated.rightExtensionInclusion_hom_app, CategoryTheory.SimplicialObject.augmentedCechNerve_map_left_app, AlgebraicTopology.AlternatingFaceMapComplex.obj_X, CategoryTheory.nerve.functorOfNerveMap_obj, SSet.N.iSup_subcomplex_eq_top, SSet.Truncated.Path₁.arrow_src, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_map, AlgebraicTopology.DoldKan.Q_f_naturality, SSet.ι₁_fst_assoc, SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id, SSet.Truncated.Edge.CompStruct.d₁, SSet.Subcomplex.PairingCore.notMem₂, SimplexCategory.Truncated.δ₂_two_comp_σ₂_one, SSet.Subcomplex.topIso_hom, SSet.OneTruncation₂.id_edge, AlgebraicTopology.inclusionOfMooreComplexMap_f, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_obj, SSet.horn.ι_ι_assoc, SimplexCategory.toCat_map, AlgebraicTopology.alternatingFaceMapComplex_obj_X, SimplexCategory.eq_of_one_to_one, CategoryTheory.CosimplicialObject.equivalenceLeftToRight_right, SSet.leftUnitor_hom_app_apply, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', SimplexCategory.σ_comp_σ, SimplexCategory.hom_zero_zero, CategoryTheory.Limits.FormalCoproduct.cech_obj, CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_map_app, SSet.stdSimplex.objEquiv_symm_apply, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc, SimplexCategory.instEpiFactorThruImage, AlgebraicTopology.DoldKan.N₂_map_f_f, SSet.Subcomplex.PairingCore.nonDegenerate₁, SSet.KanComplex.hornFilling, SSet.PtSimplex.RelStruct.δ_map_of_gt, SSet.Truncated.StrictSegal.spine_δ_vertex_lt, SimplexCategory.eq_comp_δ_of_not_surjective, SSet.nondegenerate_zero, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app, SimplexCategory.Truncated.Hom.tr_comp'_assoc, AlgebraicTopology.DoldKan.P_f_naturality, SSet.Truncated.HomotopyCategory.descOfTruncation_obj_mk, SSet.S.IsUniquelyCodimOneFace.iff, AlgebraicTopology.DoldKan.MorphComponents.id_b, SimplicialObject.Split.cofan_inj_naturality_symm, AlgebraicTopology.DoldKan.factors_normalizedMooreComplex_PInfty, SimplexCategory.II_obj, SSet.associator_inv_app_apply, SSet.stdSimplex.nonDegenerateEquiv_symm_apply_coe, SSet.horn.ι_ι, SimplicialObject.Splitting.cofan_inj_comp_app_assoc, CategoryTheory.cosimplicialSimplicialEquiv_functor_obj_map, SimplexCategory.epi_iff_surjective, CategoryTheory.SimplicialObject.δ_comp_σ_succ_assoc, SSet.RelativeMorphism.map_coe, SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_obj, SSet.Subcomplex.N.notMem, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map, SimplexCategory.Truncated.initial_incl, AlgebraicTopology.DoldKan.hσ'_naturality, AlgebraicTopology.DoldKan.P_add_Q_f, SSet.horn.const_val_apply, AlgebraicTopology.DoldKan.hσ'_eq', SSet.StrictSegal.isRightKanExtension, SSet.Truncated.IsStrictSegal.segal, AlgebraicTopology.DoldKan.HigherFacesVanish.induction, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty, CategoryTheory.nerveMap_app_mk₀, SSet.horn₂₁.sq, SSet.Subcomplex.image_iSup, SimplicialObject.Splitting.cofan_inj_eq_assoc, SimplexCategory.II_δ, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app, SimplexCategory.SkeletalFunctor.instFullNonemptyFinLinOrdSkeletalFunctor, SSet.horn.primitiveTriangle_coe, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc, SimplexCategory.δ_comp_σ_succ, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_obj, CategoryTheory.SimplicialObject.equivalenceLeftToRight_left_app, SSet.degenerate_iff_of_isIso, SSet.stdSimplex.face_singleton_compl, SSet.ι₀_app_fst, CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt', SSet.Truncated.spine_injective, AugmentedSimplexCategory.tensorHom_comp_tensorHom, CategoryTheory.SimplicialObject.Truncated.whiskering_obj_map_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_obj, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_hom_app, SimplicialObject.Splitting.cofan_inj_epi_naturality, SimplexCategory.instMonoδ, SSet.Truncated.Edge.CompStruct.idCompId_simplex, SimplexCategoryGenRel.isSplitMono_toSimplexCategory_map_of_P_δ, SimplicialObject.Splitting.IndexSet.eqId_iff_len_le, SSet.range_eq_iSup_of_isColimit, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app, SSet.Subcomplex.preimage_iInf, CategoryTheory.simplicialCosimplicialEquiv_functor_obj_map, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_left, SSet.S.le_def, CategoryTheory.CosimplicialObject.δ_comp_σ_self'_assoc, classifyingSpaceUniversalCover_obj, SSet.ι₁_comp_assoc, SSet.skeletonOfMono_succ, CategoryTheory.Arrow.augmentedCechConerve_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app, CategoryTheory.SimplicialObject.δ_comp_δ_self'_assoc, SSet.PtSimplex.RelStruct.δ_succ_map_assoc, SimplexCategory.δ_comp_σ_self'_assoc, SSet.StrictSegal.spineToSimplex_vertex, SSet.Truncated.Edge.tgt_eq, SSet.stdSimplex.isoNerve_inv_app_apply, SSet.Truncated.StrictSegal.spineToSimplex_map, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map, SSet.RelativeMorphism.Homotopy.rel_assoc, SSet.skeleton_zero, CategoryTheory.CosimplicialObject.δ_comp_σ_of_le_assoc, SimplexCategory.morphismProperty_eq_top

---

← Back to Index