Basic

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean

Statistics

Metric	Count
Definitions SSet, cosk, fullyFaithful, reflective, largeCategory, sk, fullyFaithful, coreflective, trunc, uliftFunctor, const, cosk, coskAdj, largeCategory, sk, skAdj, truncation, truncationCompTrunc, uliftFunctor	19
Theorems comp_app, comp_app_assoc, faithful, full, cosk_reflective, hasColimits, hasLimits, hom_ext, hom_ext_iff, id_app, faithful, full, sk_coreflective, comp_app, comp_app_assoc, comp_const, const_app, const_comp, hasColimits, hasLimits, hom_ext, hom_ext_iff, id_app, δ_comp_δ''_apply, δ_comp_δ'_apply, δ_comp_δ_apply, δ_comp_δ_self'_apply, δ_comp_δ_self_apply, δ_comp_σ_of_gt'_apply, δ_comp_σ_of_gt_apply, δ_comp_σ_of_le_apply, δ_comp_σ_self'_apply, δ_comp_σ_self_apply, δ_comp_σ_succ'_apply, δ_comp_σ_succ_apply, δ_naturality_apply, σ_comp_σ_apply, σ_naturality_apply	38
Total	57

SSet

Definitions

Name	Category	Theorems
const 📖	CompOp	24 math math: PtSimplex.RelStruct.δ_map_of_lt, ι₀_snd_assoc, PtSimplex.MulStruct.δ_map_of_gt, PtSimplex.RelStruct.δ_castSucc_map, PtSimplex.RelStruct.δ_castSucc_map_assoc, PtSimplex.MulStruct.δ_succ_succ_map_assoc, RelativeMorphism.ofSimplex₀_map, PtSimplex.MulStruct.δ_succ_succ_map, ι₀_snd, PtSimplex.MulStruct.δ_succ_castSucc_map, ι₁_snd_assoc, ι₁_snd, comp_const, const_app, PtSimplex.MulStruct.δ_map_of_lt, const_comp, PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc, Subcomplex.ofSimplex_ι, RelativeMorphism.const_map, PtSimplex.RelStruct.δ_succ_map, PtSimplex.RelStruct.δ_map_of_gt, PtSimplex.MulStruct.δ_succ_castSucc_map_assoc, PtSimplex.RelStruct.δ_succ_map_assoc, PtSimplex.MulStruct.δ_castSucc_castSucc_map
cosk 📖	CompOp	—
coskAdj 📖	CompOp	1 math math: Truncated.cosk_reflective
largeCategory 📖	CompOp	279 math math: OneTruncation₂.nerveEquiv_apply, Subcomplex.lift_ι, stdSimplex.mem_nonDegenerate_iff_strictMono, OneTruncation₂.ofNerve₂.natIso_hom_app_map, PtSimplex.RelStruct.δ_map_of_lt, Subcomplex.toRange_ι, Truncated.sk.full, ι₀_snd_assoc, Truncated.HomotopyCategory.descOfTruncation_comp, CategoryTheory.SimplicialThickening.SimplicialCategory.comp_id, modelCategoryQuillen.I_le_monomorphisms, instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk, horn.faceSingletonComplIso_inv_ι_assoc, hasColimits, stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ, Subcomplex.fromPreimage_ι_assoc, Subcomplex.toSSetFunctor_map, iSup_subcomplexOfSimplex_prod_eq_top, stdSimplex.obj₀Equiv_symm_apply, OneTruncation₂.nerveHomEquiv_id, CategoryTheory.nerve.functorOfNerveMap_map, opFunctorCompOpFunctorIso_inv_app_app, modelCategoryQuillen.mono_of_cofibration, Subcomplex.range_eq_ofSimplex, PtSimplex.MulStruct.δ_map_of_gt, instHasDimensionLETensorUnitOfNatNat, tensorHom_app_apply, Truncated.sk_coreflective, CategoryTheory.nerveFunctor.faithful, hoFunctor.preservesTerminal', prodStdSimplex.instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat, Subcomplex.toImage_ι, horn.yonedaEquiv_ι, Finite.instIsFinitelyPresentableObjSimplexCategoryStdSimplex, instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex, Subcomplex.topIso_inv_app_coe, prodStdSimplex.orderHomOfSimplex_coe, Subcomplex.homOfLE_refl, opFunctorCompOpFunctorIso_hom_app_app, hasDimensionLT_prod, instIsStableUnderFilteredColimitsMonomorphisms, Subcomplex.toRange_ι_assoc, RelativeMorphism.Homotopy.h₀_assoc, prodStdSimplex.objEquiv_apply_fst, stdSimplex.map_id, Subcomplex.lift_ι_assoc, modelCategoryQuillen.fibrations_eq, modelCategoryQuillen.cofibrations_eq, opEquivalence_inverse, instFiniteTensorUnit, Edge.ofTruncated_edge, horn₂₂.sq, nonDegenerateEquivOfIso_symm_apply_coe, Subcomplex.image_id, stdSimplex.ext_iff, opFunctor_map, Subcomplex.toImage_ι_assoc, Subcomplex.topIso_inv_ι, prodStdSimplex.strictMono_orderHomOfSimplex_iff, Subcomplex.ofSimplexProd_eq_range, stdSimplex.face_eq_ofSimplex, PtSimplex.RelStruct.δ_castSucc_map, stdSimplex.obj₀Equiv_apply, prodStdSimplex.objEquiv_δ_apply, horn.faceSingletonComplIso_inv_ι, Subcomplex.toSSetFunctor_obj, Subcomplex.instSubsingletonHomToSSetBot, instBalanced, prodStdSimplex.objEquiv_naturality, modelCategoryQuillen.instHasLiftingPropertyιHornHAddNatOfNatOfFibration, stdSimplex.spineId_arrow_apply_zero, comp_app_assoc, Subcomplex.eqToIso_hom, stdSimplex.range_δ, PtSimplex.RelStruct.δ_castSucc_map_assoc, PtSimplex.MulStruct.δ_succ_succ_map_assoc, id_app, instFiniteTensorObj, Augmented.stdSimplex_map_right, PtSimplex.MulStruct.δ_succ_succ_map, Subcomplex.homOfLE_comp_assoc, prodStdSimplex.objEquiv_apply_snd, Subcomplex.instEpiToImage, hoFunctor.unitHomEquiv_eq, Augmented.stdSimplex_obj_left, instIsStableUnderCoproductsMonomorphismsOfHasCoproductsType, stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, instFiniteObjOppositeSimplexCategoryTensorObj, horn.spineId_map_hornInclusion, instFiniteCoprod, horn_obj, leftUnitor_inv_app_apply, ι₀_fst_assoc, ι₁_comp, Subcomplex.yonedaEquiv_coe, CategoryTheory.hoFunctor.preservesFiniteProducts, OneTruncation₂.ofNerve₂.natIso_hom_app_obj, Subcomplex.homOfLE_ι_assoc, whiskerRight_app_apply, rightUnitor_inv_app_apply, stdSimplex.face_obj, stdSimplex.nonDegenerateEquiv_apply_apply, modelCategoryQuillen.horn_ι_mem_J, stdSimplex.map_apply, ι₀_snd, PtSimplex.MulStruct.δ_succ_castSucc_map, CategoryTheory.hoFunctor.instIsLeftAdjointSSetCatHoFunctor, Subcomplex.image_comp, horn₂₀.sq, stdSimplex.mem_face_iff, hoFunctor.preservesTerminal, CategoryTheory.SimplicialThickening.functor_map, stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ, instIsStableUnderCobaseChangeMonomorphisms, ι₁_snd_assoc, horn.edge_coe, modelCategoryQuillen.cofibration_of_mono, OneTruncation₂.nerveEquiv_symm_apply_map, stdSimplex.isoNerve_hom_app_apply, stdSimplex.faceSingletonComplIso_hom_ι, instHasDimensionLETensorObjHAddNat, ι₁_app_fst, ι₁_snd, whiskerLeft_app_apply, comp_app, CategoryTheory.nerveFunctor_map, Subcomplex.prod_obj, comp_const, stdSimplex.instFiniteObjOppositeSimplexCategory, Truncated.HomotopyCategory.descOfTruncation_map_homMk, RelativeMorphism.comm_assoc, Subcomplex.instMonoToRange, modelCategoryQuillen.cofibration_iff, instHasDimensionLTTensorObjHAddNat, Subcomplex.homOfLE_ι, face_le_horn, CategoryTheory.hoFunctor.preservesBinaryProducts, Subcomplex.image_eq_range, RelativeMorphism.comm, PtSimplex.MulStruct.δ_map_of_lt, stdSimplex.instHasDimensionLEObjSimplexCategoryMk, stdSimplex.monotone_apply, horn.faceι_ι, Truncated.HomotopyCategory.homToNerveMk_app_one, prodStdSimplex.objEquiv_map_apply, stdSimplex.objEquiv_symm_mem_nonDegenerate_iff_mono, CategoryTheory.hoFunctor.isIso_prodComparison_stdSimplex, Subcomplex.homOfLE_comp, horn.edge₃_coe_down, CategoryTheory.SimplicialThickening.SimplicialCategory.assoc, Subcomplex.topIso_inv_ι_assoc, horn₂₁.isPushout, horn_eq_iSup, stdSimplex.obj₀Equiv_symm_mem_face_iff, range_eq_iSup_sigma_ι, Subcomplex.BicartSq.isPushout, Subcomplex.range_comp, prodStdSimplex.instFiniteTensorObjObjSimplexCategoryStdSimplexMk, stdSimplex.objEquiv_symm_comp, Subcomplex.eqToIso_inv, Subcomplex.prod_monotone, ι₀_comp_assoc, Subcomplex.instMonoι, ι₀_comp, opEquivalence_unitIso, Augmented.stdSimplex_obj_hom_app, horn.faceι_ι_assoc, RelativeMorphism.Homotopy.h₁_assoc, CategoryTheory.nerveFunctor.full, stdSimplex.yonedaEquiv_map, RelativeMorphism.Homotopy.ofEq_h, horn_obj_zero, horn.spineId_vertex_coe, rightUnitor_hom_app_apply, horn.multicoequalizerDiagram, horn.spineId_arrow_coe, iSup_range_eq_top_of_isColimit, stdSimplex.objEquiv_toOrderHom_apply, ι₁_fst, const_comp, PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc, Truncated.cosk.faithful, Subcomplex.liftPath_arrow_coe, horn₂₀.isPushout, stdSimplex.ofSimplex_yonedaEquiv_δ, prodStdSimplex.nonDegenerate_iff_injective_objEquiv, Quasicategory.hornFilling, stdSimplex.instFiniteObjSimplexCategory, stdSimplex.objMk_apply, Truncated.HomotopyCategory.homToNerveMk_app_edge, OneTruncation₂.ofNerve₂.natIso_inv_app_map, RelativeMorphism.Homotopy.h₀, nonDegenerateEquivOfIso_apply_coe, modelCategoryQuillen.boundary_ι_mem_I, Augmented.stdSimplex_map_left, stdSimplex.faceSingletonComplIso_hom_ι_assoc, Finite.exists_epi_from_isCardinalPresentable, ι₀_fst, associator_hom_app_apply, Truncated.cosk.full, OneTruncation₂.nerveEquiv_symm_apply_obj, Subcomplex.liftPath_vertex_coe, modelCategoryQuillen.J_le_monomorphisms, CategoryTheory.hoFunctor.instIsIsoCatProdComparisonSSetHoFunctorNerve, boundary_eq_iSup, RelativeMorphism.Homotopy.h₁, stdSimplex.spineId_vertex, Subcomplex.range_tensorHom, Truncated.cosk_reflective, CategoryTheory.hoFunctor.preservesBinaryProduct, CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map, stdSimplex.face_inter_face, CategoryTheory.nerveFunctor_obj, stdSimplex.mem_nonDegenerate_iff_mono, Subcomplex.mono_homOfLE, horn₂₂.isPushout, prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, yonedaEquiv_comp, stdSimplex.spineId_arrow_apply_one, Quasicategory.hornFilling', OneTruncation₂.nerveHomEquiv_apply, Subcomplex.instEpiToRange, instFiniteSigmaObjOfFinite, RelativeMorphism.Homotopy.rel, horn.primitiveEdge_coe_down, stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ_assoc, Subcomplex.range_eq_top_iff, Truncated.HomotopyCategory.homToNerveMk_app_zero, Subcomplex.fromPreimage_ι, stdSimplex.face_le_face_iff, Finite.instIsFinitelyPresentable, RelativeMorphism.Homotopy.refl_h, truncation_spine, PtSimplex.RelStruct.δ_succ_map, Truncated.HomotopyCategory.homToNerveMk_comp, CategoryTheory.SimplicialThickening.functor_id, modelCategoryQuillen.fibration_iff, hasDimensionLE_prod, ι₁_fst_assoc, hasLimits, Subcomplex.topIso_hom, Edge.toTruncated_id, horn.ι_ι_assoc, Truncated.sk.faithful, opEquivalence_counitIso, leftUnitor_hom_app_apply, stdSimplex.objEquiv_symm_apply, StrictSegal.instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal, KanComplex.hornFilling, PtSimplex.RelStruct.δ_map_of_gt, Truncated.HomotopyCategory.descOfTruncation_obj_mk, associator_inv_app_apply, stdSimplex.nonDegenerateEquiv_symm_apply_coe, horn.ι_ι, CategoryTheory.hoFunctor.isIso_prodComparison, CategoryTheory.SimplicialThickening.functor_obj_as, instIsRegularEpiCategory, CategoryTheory.instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf, PtSimplex.MulStruct.δ_succ_castSucc_map_assoc, horn.const_val_apply, CategoryTheory.nerveAdjunction.isIso_counit, horn₂₁.sq, CategoryTheory.SimplicialThickening.SimplicialCategory.id_comp, instFinitePullback, Truncated.HomotopyCategory.homToNerveMk_comp_assoc, CategoryTheory.SimplicialThickening.functor_comp, horn.primitiveTriangle_coe, stdSimplex.face_singleton_compl, ι₀_app_fst, Edge.toTruncated_edge, range_eq_iSup_of_isColimit, Subcomplex.instIsIsoToRangeOfMono, ι₁_comp_assoc, PtSimplex.RelStruct.δ_succ_map_assoc, opEquivalence_functor, stdSimplex.isoNerve_inv_app_apply, instFiniteInitial, PtSimplex.MulStruct.δ_castSucc_castSucc_map, RelativeMorphism.Homotopy.rel_assoc
sk 📖	CompOp	—
skAdj 📖	CompOp	1 math math: Truncated.sk_coreflective
truncation 📖	CompOp	30 math math: OneTruncation₂.nerveEquiv_apply, OneTruncation₂.ofNerve₂.natIso_hom_app_map, Truncated.HomotopyCategory.descOfTruncation_comp, instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk, OneTruncation₂.nerveHomEquiv_id, CategoryTheory.nerve.functorOfNerveMap_map, Truncated.sk_coreflective, Edge.ofTruncated_edge, OneTruncation₂.ofNerve₂.natIso_hom_app_obj, OneTruncation₂.nerveEquiv_symm_apply_map, Truncated.HomotopyCategory.descOfTruncation_map_homMk, Truncated.HomotopyCategory.homToNerveMk_app_one, horn.spineId_vertex_coe, horn.spineId_arrow_coe, Subcomplex.liftPath_arrow_coe, Truncated.HomotopyCategory.homToNerveMk_app_edge, OneTruncation₂.ofNerve₂.natIso_inv_app_map, OneTruncation₂.nerveEquiv_symm_apply_obj, Subcomplex.liftPath_vertex_coe, Truncated.cosk_reflective, CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map, OneTruncation₂.nerveHomEquiv_apply, Truncated.HomotopyCategory.homToNerveMk_app_zero, truncation_spine, Truncated.HomotopyCategory.homToNerveMk_comp, Edge.toTruncated_id, StrictSegal.instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal, Truncated.HomotopyCategory.descOfTruncation_obj_mk, Truncated.HomotopyCategory.homToNerveMk_comp_assoc, Edge.toTruncated_edge
truncationCompTrunc 📖	CompOp	—
uliftFunctor 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.Functor.obj	—	—
comp_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.NatTrans.app SSet largeCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_app
comp_const 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct largeCategory const	—	—
const_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types const CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.const SimplexCategory.len SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat	—	—
const_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct largeCategory const CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op	—	hom_ext CategoryTheory.types_ext CategoryTheory.FunctorToTypes.naturality
hasColimits 📖	mathematical	—	CategoryTheory.Limits.HasColimits SSet largeCategory	—	CategoryTheory.SimplicialObject.instHasColimits CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self
hasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits SSet largeCategory	—	CategoryTheory.SimplicialObject.instHasLimits CategoryTheory.Limits.Types.hasLimitsOfSize UnivLE.self
hom_ext 📖	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types	—	—	CategoryTheory.SimplicialObject.hom_ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types	—	hom_ext
id_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.CategoryStruct.id SSet CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.Functor.obj	—	—
δ_comp_δ''_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types Fin.le_iff_val_le_val	—	Fin.le_iff_val_le_val CategoryTheory.SimplicialObject.δ_comp_δ''
δ_comp_δ'_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types	—	CategoryTheory.SimplicialObject.δ_comp_δ'
δ_comp_δ_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types	—	CategoryTheory.SimplicialObject.δ_comp_δ
δ_comp_δ_self'_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types	—	CategoryTheory.SimplicialObject.δ_comp_δ_self'
δ_comp_δ_self_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types	—	CategoryTheory.SimplicialObject.δ_comp_δ_self
δ_comp_σ_of_gt'_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.SimplicialObject.σ add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instPartialOrder covariant_swap_add_of_covariant_add Preorder.toLE PartialOrder.toPreorder Nat.instAddCommSemigroup IsOrderedAddMonoid.toAddLeftMono Nat.instAddCommMonoid Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma Nat.instLinearOrder lt_of_lt_of_le Nat.instPreorder	—	add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le lt_of_lt_of_le CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'
δ_comp_σ_of_gt_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.SimplicialObject.σ	—	CategoryTheory.SimplicialObject.δ_comp_σ_of_gt
δ_comp_σ_of_le_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.SimplicialObject.σ	—	CategoryTheory.SimplicialObject.δ_comp_σ_of_le
δ_comp_σ_self'_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.SimplicialObject.σ	—	CategoryTheory.SimplicialObject.δ_comp_σ_self'
δ_comp_σ_self_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.SimplicialObject.σ	—	CategoryTheory.SimplicialObject.δ_comp_σ_self
δ_comp_σ_succ'_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.SimplicialObject.σ	—	CategoryTheory.SimplicialObject.δ_comp_σ_succ'
δ_comp_σ_succ_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.δ CategoryTheory.types CategoryTheory.SimplicialObject.σ	—	CategoryTheory.SimplicialObject.δ_comp_σ_succ
δ_naturality_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op CategoryTheory.SimplicialObject.δ	—	CategoryTheory.SimplicialObject.δ_naturality
σ_comp_σ_apply 📖	mathematical	—	CategoryTheory.SimplicialObject.σ CategoryTheory.types	—	CategoryTheory.SimplicialObject.σ_comp_σ
σ_naturality_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op CategoryTheory.SimplicialObject.σ	—	CategoryTheory.SimplicialObject.σ_naturality

SSet.Truncated

Definitions

Name	Category	Theorems
cosk 📖	CompOp	3 math math: cosk.faithful, cosk.full, cosk_reflective
largeCategory 📖	CompOp	88 math math: SSet.OneTruncation₂.nerveEquiv_apply, HomotopyCategory.BinaryProduct.iso_inv_toFunctor, tensor_map_apply_snd, SSet.oneTruncation₂_obj, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map, CategoryTheory.nerve.instFullCatTruncatedOfNatNatNerveFunctor₂, sk.full, HomotopyCategory.descOfTruncation_comp, SSet.instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk, SSet.oneTruncation₂_map, Path.mk₂_arrow, HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk, SSet.OneTruncation₂.nerveHomEquiv_id, CategoryTheory.nerve.functorOfNerveMap_map, sk_coreflective, Edge.map_fst, HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app, HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app, SSet.Edge.ofTruncated_edge, HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, Edge.CompStruct.tensor_simplex_snd, HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd, Edge.id_tensor_id, CategoryTheory.Nerve.instIsStrictSegalObjCatTruncatedOfNatNatNerveFunctor₂, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj, id_app, HomotopyCategory.BinaryProduct.left_unitality, Edge.CompStruct.tensor_simplex_fst, hasColimits, HomotopyCategory.BinaryProduct.inverseCompFunctorIso_inv_app, Edge.map_associator_hom, SSet.OneTruncation₂.nerveEquiv_symm_apply_map, HomotopyCategory.BinaryProduct.iso_hom_toFunctor, Edge.map_whiskerLeft, HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id, HomotopyCategory.BinaryProduct.mapHomotopyCategory_prod_id_comp_inverse, Edge.map_snd, HomotopyCategory.BinaryProduct.functor_comp_inverse, HomotopyCategory.descOfTruncation_map_homMk, HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk, hoFunctor₂_naturality, HomotopyCategory.BinaryProduct.inverse_comp_functor, HomotopyCategory.homToNerveMk_app_one, comp_app_assoc, Edge.map_tensorHom, HomotopyCategory.BinaryProduct.associativity'Iso_hom_app, SSet.horn.spineId_vertex_coe, tensor_map_apply_fst, HomotopyCategory.BinaryProduct.functor_obj, SSet.horn.spineId_arrow_coe, Edge.tensor_edge, cosk.faithful, SSet.Subcomplex.liftPath_arrow_coe, HomotopyCategory.BinaryProduct.square, HomotopyCategory.BinaryProduct.inverseCompFunctorIso_hom_app, HomotopyCategory.homToNerveMk_app_edge, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map, trunc_spine, cosk.full, HomotopyCategory.BinaryProduct.associativity, SSet.OneTruncation₂.nerveEquiv_symm_apply_obj, SSet.Subcomplex.liftPath_vertex_coe, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map, HomotopyCategory.BinaryProduct.right_unitality, cosk_reflective, CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map, Path.mk₂_vertex, SSet.OneTruncation₂.nerveHomEquiv_apply, HomotopyCategory.BinaryProduct.associativityIso_hom_app, HomotopyCategory.homToNerveMk_app_zero, Edge.map_whiskerRight, comp_app, SSet.truncation_spine, HomotopyCategory.homToNerveMk_comp, HomotopyCategory.BinaryProduct.functor_map, CategoryTheory.nerve.functorOfNerveMap_obj, CategoryTheory.nerve.nerveFunctor₂_map_functorOfNerveMap, HomotopyCategory.BinaryProduct.id_prod_mapHomotopyCategory_comp_inverse, SSet.Edge.toTruncated_id, sk.faithful, SSet.StrictSegal.instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal, HomotopyCategory.descOfTruncation_obj_mk, HomotopyCategory.BinaryProduct.inverse_obj, HomotopyCategory.homToNerveMk_comp_assoc, CategoryTheory.nerve.instFaithfulCatTruncatedOfNatNatNerveFunctor₂, SSet.Edge.toTruncated_edge, hasLimits
sk 📖	CompOp	3 math math: sk.full, sk_coreflective, sk.faithful
trunc 📖	CompOp	7 math math: Path.mk₂_arrow, SSet.horn.spineId_vertex_coe, SSet.horn.spineId_arrow_coe, SSet.Subcomplex.liftPath_arrow_coe, trunc_spine, SSet.Subcomplex.liftPath_vertex_coe, Path.mk₂_vertex
uliftFunctor 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types CategoryTheory.CategoryStruct.comp SSet.Truncated CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.Functor.obj	—	—
comp_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.NatTrans.app SSet.Truncated largeCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_app
cosk_reflective 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor SSet.Truncated largeCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp SSet SSet.largeCategory cosk SSet.truncation CategoryTheory.Functor.id CategoryTheory.Adjunction.counit SSet.coskAdj	—	CategoryTheory.SimplicialObject.Truncated.cosk_reflective CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self
hasColimits 📖	mathematical	—	CategoryTheory.Limits.HasColimits SSet.Truncated largeCategory	—	CategoryTheory.SimplicialObject.Truncated.instHasColimits CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self
hasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits SSet.Truncated largeCategory	—	CategoryTheory.SimplicialObject.Truncated.instHasLimits CategoryTheory.Limits.Types.hasLimitsOfSize UnivLE.self
hom_ext 📖	—	CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types	—	—	CategoryTheory.NatTrans.ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types	—	hom_ext
id_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types CategoryTheory.CategoryStruct.id SSet.Truncated CategoryTheory.Category.toCategoryStruct largeCategory CategoryTheory.Functor.obj	—	—
sk_coreflective 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor SSet.Truncated largeCategory CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp SSet SSet.largeCategory sk SSet.truncation CategoryTheory.Adjunction.unit SSet.skAdj	—	CategoryTheory.SimplicialObject.Truncated.sk_coreflective CategoryTheory.Limits.Types.hasColimit UnivLE.small univLE_of_max UnivLE.self

SSet.Truncated.cosk

Definitions

Name	Category	Theorems
fullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful SSet.Truncated SSet.Truncated.largeCategory SSet SSet.largeCategory SSet.Truncated.cosk	—	CategoryTheory.SimplicialObject.Truncated.cosk.faithful CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self
full 📖	mathematical	—	CategoryTheory.Functor.Full SSet.Truncated SSet.Truncated.largeCategory SSet SSet.largeCategory SSet.Truncated.cosk	—	CategoryTheory.SimplicialObject.Truncated.cosk.full CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self

SSet.Truncated.coskAdj

Definitions

Name	Category	Theorems
reflective 📖	CompOp	—

SSet.Truncated.sk

Definitions

Name	Category	Theorems
fullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful SSet.Truncated SSet.Truncated.largeCategory SSet SSet.largeCategory SSet.Truncated.sk	—	CategoryTheory.SimplicialObject.Truncated.sk.faithful CategoryTheory.Limits.Types.hasColimit UnivLE.small univLE_of_max UnivLE.self
full 📖	mathematical	—	CategoryTheory.Functor.Full SSet.Truncated SSet.Truncated.largeCategory SSet SSet.largeCategory SSet.Truncated.sk	—	CategoryTheory.SimplicialObject.Truncated.sk.full CategoryTheory.Limits.Types.hasColimit UnivLE.small univLE_of_max UnivLE.self

SSet.Truncated.skAdj

Definitions

Name	Category	Theorems
coreflective 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
SSet 📖	CompOp	279 math math: SSet.OneTruncation₂.nerveEquiv_apply, SSet.Subcomplex.lift_ι, SSet.stdSimplex.mem_nonDegenerate_iff_strictMono, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map, SSet.PtSimplex.RelStruct.δ_map_of_lt, SSet.Subcomplex.toRange_ι, SSet.Truncated.sk.full, SSet.ι₀_snd_assoc, SSet.Truncated.HomotopyCategory.descOfTruncation_comp, CategoryTheory.SimplicialThickening.SimplicialCategory.comp_id, SSet.modelCategoryQuillen.I_le_monomorphisms, SSet.instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk, SSet.horn.faceSingletonComplIso_inv_ι_assoc, SSet.hasColimits, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ, SSet.Subcomplex.fromPreimage_ι_assoc, SSet.Subcomplex.toSSetFunctor_map, SSet.iSup_subcomplexOfSimplex_prod_eq_top, SSet.stdSimplex.obj₀Equiv_symm_apply, SSet.OneTruncation₂.nerveHomEquiv_id, CategoryTheory.nerve.functorOfNerveMap_map, SSet.opFunctorCompOpFunctorIso_inv_app_app, SSet.modelCategoryQuillen.mono_of_cofibration, SSet.Subcomplex.range_eq_ofSimplex, SSet.PtSimplex.MulStruct.δ_map_of_gt, SSet.instHasDimensionLETensorUnitOfNatNat, SSet.tensorHom_app_apply, SSet.Truncated.sk_coreflective, CategoryTheory.nerveFunctor.faithful, SSet.hoFunctor.preservesTerminal', SSet.prodStdSimplex.instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat, SSet.Subcomplex.toImage_ι, SSet.horn.yonedaEquiv_ι, SSet.Finite.instIsFinitelyPresentableObjSimplexCategoryStdSimplex, instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex, SSet.Subcomplex.topIso_inv_app_coe, SSet.prodStdSimplex.orderHomOfSimplex_coe, SSet.Subcomplex.homOfLE_refl, SSet.opFunctorCompOpFunctorIso_hom_app_app, SSet.hasDimensionLT_prod, SSet.instIsStableUnderFilteredColimitsMonomorphisms, SSet.Subcomplex.toRange_ι_assoc, SSet.RelativeMorphism.Homotopy.h₀_assoc, SSet.prodStdSimplex.objEquiv_apply_fst, SSet.stdSimplex.map_id, SSet.Subcomplex.lift_ι_assoc, SSet.modelCategoryQuillen.fibrations_eq, SSet.modelCategoryQuillen.cofibrations_eq, SSet.opEquivalence_inverse, SSet.instFiniteTensorUnit, SSet.Edge.ofTruncated_edge, SSet.horn₂₂.sq, SSet.nonDegenerateEquivOfIso_symm_apply_coe, SSet.Subcomplex.image_id, SSet.stdSimplex.ext_iff, SSet.opFunctor_map, SSet.Subcomplex.toImage_ι_assoc, SSet.Subcomplex.topIso_inv_ι, SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, SSet.Subcomplex.ofSimplexProd_eq_range, SSet.stdSimplex.face_eq_ofSimplex, SSet.PtSimplex.RelStruct.δ_castSucc_map, SSet.stdSimplex.obj₀Equiv_apply, SSet.prodStdSimplex.objEquiv_δ_apply, SSet.horn.faceSingletonComplIso_inv_ι, SSet.Subcomplex.toSSetFunctor_obj, SSet.Subcomplex.instSubsingletonHomToSSetBot, SSet.instBalanced, SSet.prodStdSimplex.objEquiv_naturality, SSet.modelCategoryQuillen.instHasLiftingPropertyιHornHAddNatOfNatOfFibration, SSet.stdSimplex.spineId_arrow_apply_zero, SSet.comp_app_assoc, SSet.Subcomplex.eqToIso_hom, SSet.stdSimplex.range_δ, SSet.PtSimplex.RelStruct.δ_castSucc_map_assoc, SSet.PtSimplex.MulStruct.δ_succ_succ_map_assoc, SSet.id_app, SSet.instFiniteTensorObj, SSet.Augmented.stdSimplex_map_right, SSet.PtSimplex.MulStruct.δ_succ_succ_map, SSet.Subcomplex.homOfLE_comp_assoc, SSet.prodStdSimplex.objEquiv_apply_snd, SSet.Subcomplex.instEpiToImage, SSet.hoFunctor.unitHomEquiv_eq, SSet.Augmented.stdSimplex_obj_left, SSet.instIsStableUnderCoproductsMonomorphismsOfHasCoproductsType, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, SSet.instFiniteObjOppositeSimplexCategoryTensorObj, SSet.horn.spineId_map_hornInclusion, SSet.instFiniteCoprod, SSet.horn_obj, SSet.leftUnitor_inv_app_apply, SSet.ι₀_fst_assoc, SSet.ι₁_comp, SSet.Subcomplex.yonedaEquiv_coe, CategoryTheory.hoFunctor.preservesFiniteProducts, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj, SSet.Subcomplex.homOfLE_ι_assoc, SSet.whiskerRight_app_apply, SSet.rightUnitor_inv_app_apply, SSet.stdSimplex.face_obj, SSet.stdSimplex.nonDegenerateEquiv_apply_apply, SSet.modelCategoryQuillen.horn_ι_mem_J, SSet.stdSimplex.map_apply, SSet.ι₀_snd, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map, CategoryTheory.hoFunctor.instIsLeftAdjointSSetCatHoFunctor, SSet.Subcomplex.image_comp, SSet.horn₂₀.sq, SSet.stdSimplex.mem_face_iff, SSet.hoFunctor.preservesTerminal, CategoryTheory.SimplicialThickening.functor_map, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ, SSet.instIsStableUnderCobaseChangeMonomorphisms, SSet.ι₁_snd_assoc, SSet.horn.edge_coe, SSet.modelCategoryQuillen.cofibration_of_mono, SSet.OneTruncation₂.nerveEquiv_symm_apply_map, SSet.stdSimplex.isoNerve_hom_app_apply, SSet.stdSimplex.faceSingletonComplIso_hom_ι, SSet.instHasDimensionLETensorObjHAddNat, SSet.ι₁_app_fst, SSet.ι₁_snd, SSet.whiskerLeft_app_apply, SSet.comp_app, CategoryTheory.nerveFunctor_map, SSet.Subcomplex.prod_obj, SSet.comp_const, SSet.stdSimplex.instFiniteObjOppositeSimplexCategory, SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk, SSet.RelativeMorphism.comm_assoc, SSet.Subcomplex.instMonoToRange, SSet.modelCategoryQuillen.cofibration_iff, SSet.instHasDimensionLTTensorObjHAddNat, SSet.Subcomplex.homOfLE_ι, SSet.face_le_horn, CategoryTheory.hoFunctor.preservesBinaryProducts, SSet.Subcomplex.image_eq_range, SSet.RelativeMorphism.comm, SSet.PtSimplex.MulStruct.δ_map_of_lt, SSet.stdSimplex.instHasDimensionLEObjSimplexCategoryMk, SSet.stdSimplex.monotone_apply, SSet.horn.faceι_ι, SSet.Truncated.HomotopyCategory.homToNerveMk_app_one, SSet.prodStdSimplex.objEquiv_map_apply, SSet.stdSimplex.objEquiv_symm_mem_nonDegenerate_iff_mono, CategoryTheory.hoFunctor.isIso_prodComparison_stdSimplex, SSet.Subcomplex.homOfLE_comp, SSet.horn.edge₃_coe_down, CategoryTheory.SimplicialThickening.SimplicialCategory.assoc, SSet.Subcomplex.topIso_inv_ι_assoc, SSet.horn₂₁.isPushout, SSet.horn_eq_iSup, SSet.stdSimplex.obj₀Equiv_symm_mem_face_iff, SSet.range_eq_iSup_sigma_ι, SSet.Subcomplex.BicartSq.isPushout, SSet.Subcomplex.range_comp, SSet.prodStdSimplex.instFiniteTensorObjObjSimplexCategoryStdSimplexMk, SSet.stdSimplex.objEquiv_symm_comp, SSet.Subcomplex.eqToIso_inv, SSet.Subcomplex.prod_monotone, SSet.ι₀_comp_assoc, SSet.Subcomplex.instMonoι, SSet.ι₀_comp, SSet.opEquivalence_unitIso, SSet.Augmented.stdSimplex_obj_hom_app, SSet.horn.faceι_ι_assoc, SSet.RelativeMorphism.Homotopy.h₁_assoc, CategoryTheory.nerveFunctor.full, SSet.stdSimplex.yonedaEquiv_map, SSet.RelativeMorphism.Homotopy.ofEq_h, SSet.horn_obj_zero, SSet.horn.spineId_vertex_coe, SSet.rightUnitor_hom_app_apply, SSet.horn.multicoequalizerDiagram, SSet.horn.spineId_arrow_coe, SSet.iSup_range_eq_top_of_isColimit, SSet.stdSimplex.objEquiv_toOrderHom_apply, SSet.ι₁_fst, SSet.const_comp, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc, SSet.Truncated.cosk.faithful, SSet.Subcomplex.liftPath_arrow_coe, SSet.horn₂₀.isPushout, SSet.stdSimplex.ofSimplex_yonedaEquiv_δ, SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv, SSet.Quasicategory.hornFilling, SSet.stdSimplex.instFiniteObjSimplexCategory, SSet.stdSimplex.objMk_apply, SSet.Truncated.HomotopyCategory.homToNerveMk_app_edge, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map, SSet.RelativeMorphism.Homotopy.h₀, SSet.nonDegenerateEquivOfIso_apply_coe, SSet.modelCategoryQuillen.boundary_ι_mem_I, SSet.Augmented.stdSimplex_map_left, SSet.stdSimplex.faceSingletonComplIso_hom_ι_assoc, SSet.Finite.exists_epi_from_isCardinalPresentable, SSet.ι₀_fst, SSet.associator_hom_app_apply, SSet.Truncated.cosk.full, SSet.OneTruncation₂.nerveEquiv_symm_apply_obj, SSet.Subcomplex.liftPath_vertex_coe, SSet.modelCategoryQuillen.J_le_monomorphisms, CategoryTheory.hoFunctor.instIsIsoCatProdComparisonSSetHoFunctorNerve, SSet.boundary_eq_iSup, SSet.RelativeMorphism.Homotopy.h₁, SSet.stdSimplex.spineId_vertex, SSet.Subcomplex.range_tensorHom, SSet.Truncated.cosk_reflective, CategoryTheory.hoFunctor.preservesBinaryProduct, CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map, SSet.stdSimplex.face_inter_face, CategoryTheory.nerveFunctor_obj, SSet.stdSimplex.mem_nonDegenerate_iff_mono, SSet.Subcomplex.mono_homOfLE, SSet.horn₂₂.isPushout, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, SSet.yonedaEquiv_comp, SSet.stdSimplex.spineId_arrow_apply_one, SSet.Quasicategory.hornFilling', SSet.OneTruncation₂.nerveHomEquiv_apply, SSet.Subcomplex.instEpiToRange, SSet.instFiniteSigmaObjOfFinite, SSet.RelativeMorphism.Homotopy.rel, SSet.horn.primitiveEdge_coe_down, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ_assoc, SSet.Subcomplex.range_eq_top_iff, SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero, SSet.Subcomplex.fromPreimage_ι, SSet.stdSimplex.face_le_face_iff, SSet.Finite.instIsFinitelyPresentable, SSet.RelativeMorphism.Homotopy.refl_h, SSet.truncation_spine, SSet.PtSimplex.RelStruct.δ_succ_map, SSet.Truncated.HomotopyCategory.homToNerveMk_comp, CategoryTheory.SimplicialThickening.functor_id, SSet.modelCategoryQuillen.fibration_iff, SSet.hasDimensionLE_prod, SSet.ι₁_fst_assoc, SSet.hasLimits, SSet.Subcomplex.topIso_hom, SSet.Edge.toTruncated_id, SSet.horn.ι_ι_assoc, SSet.Truncated.sk.faithful, SSet.opEquivalence_counitIso, SSet.leftUnitor_hom_app_apply, SSet.stdSimplex.objEquiv_symm_apply, SSet.StrictSegal.instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal, SSet.KanComplex.hornFilling, SSet.PtSimplex.RelStruct.δ_map_of_gt, SSet.Truncated.HomotopyCategory.descOfTruncation_obj_mk, SSet.associator_inv_app_apply, SSet.stdSimplex.nonDegenerateEquiv_symm_apply_coe, SSet.horn.ι_ι, CategoryTheory.hoFunctor.isIso_prodComparison, CategoryTheory.SimplicialThickening.functor_obj_as, SSet.instIsRegularEpiCategory, CategoryTheory.instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map_assoc, SSet.horn.const_val_apply, CategoryTheory.nerveAdjunction.isIso_counit, SSet.horn₂₁.sq, CategoryTheory.SimplicialThickening.SimplicialCategory.id_comp, SSet.instFinitePullback, SSet.Truncated.HomotopyCategory.homToNerveMk_comp_assoc, CategoryTheory.SimplicialThickening.functor_comp, SSet.horn.primitiveTriangle_coe, SSet.stdSimplex.face_singleton_compl, SSet.ι₀_app_fst, SSet.Edge.toTruncated_edge, SSet.range_eq_iSup_of_isColimit, SSet.Subcomplex.instIsIsoToRangeOfMono, SSet.ι₁_comp_assoc, SSet.PtSimplex.RelStruct.δ_succ_map_assoc, SSet.opEquivalence_functor, SSet.stdSimplex.isoNerve_inv_app_apply, SSet.instFiniteInitial, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map, SSet.RelativeMorphism.Homotopy.rel_assoc

---

← Back to Index