Structures · Topology
SSet.Subcomplex.Pairing.IsProper
A pairing is proper when each type (II) simplex
is uniquely a 1-codimensional face of the corresponding (I)
simplex.
- Shape
- One type argument · adds isUniquelyCodimOneFace
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances1
- SSet.op
How is a type an instance?
Loading the hierarchy index…
Assumed by75
- SSet.Subcomplex.Pairing.RankFunction.Cell.horn
- SSet.Subcomplex.Pairing.RankFunction.sigmaHorn
- SSet.Subcomplex.Pairing.RankFunction.b
- SSet.Subcomplex.Pairing.isUniquelyCodimOneFace
- SSet.Subcomplex.Pairing.RankFunction.m
- SSet.Subcomplex.Pairing.RankFunction.Cell.map
- SSet.Subcomplex.Pairing.RankFunction.Cell.ιSigmaHorn
- SSet.Subcomplex.Pairing.RankFunction.Cell.index
- SSet.Subcomplex.Pairing.RankFunction.t
- SSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc
- SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn
- SSet.Subcomplex.Pairing.RankFunction.Cell.type₂
- SSet.Subcomplex.Pairing.RankFunction.mapN
- SSet.Subcomplex.Pairing.le
- SSet.Subcomplex.Pairing.RankFunction.Cell.type₁
- SSet.Subcomplex.Pairing.RankFunction.w
- SSet.Subcomplex.Pairing.RankFunction.Cell.ι_m
- SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b
- SSet.Subcomplex.Pairing.RankFunction.basicCell
- SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_app_apply
- SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_app
- SSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc_ι
- SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t
- SSet.Subcomplex.Pairing.dim_p
- SSet.Subcomplex.Pairing.WeakRankFunction.isRegular
- SSet.Subcomplex.Pairing.RankFunction.Cell.range_map
- SSet.Subcomplex.Pairing.RankFunction.isRegular
- SSet.Subcomplex.Pairing.RankFunction.Cell.subcomplex_not_le_image_horn
- SSet.Subcomplex.Pairing.RankFunction.relativeCellComplex
- SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_app
- SSet.Subcomplex.Pairing.RankFunction.Cell.image_horn_lt_subcomplex
- SSet.Subcomplex.Pairing.RankFunction.Cell.preimage_filtration_map
- SSet.Subcomplex.Pairing.AncestralRel.dim_le
- SSet.Subcomplex.Pairing.isRegular_iff_nonempty_weakRankFunction
- SSet.Subcomplex.Pairing.RankFunction.Cell.map_app_objEquiv_symm_δ_index
- SSet.Subcomplex.Pairing.WeakRankFunction.wf_ancestralRel
- SSet.Subcomplex.Pairing.RankFunction.Cell.ι_m_assoc
- SSet.Subcomplex.Pairing.isRegular_iff_nonempty_rankFunction
- SSet.Subcomplex.Pairing.RankFunction.range_homOfLE_app_union_range_b_app
- SSet.Subcomplex.Pairing.RankFunction.Cell.image_face_index_compl
- SSet.Subcomplex.Pairing.IsProper.isUniquelyCodimOneFace
- SSet.Subcomplex.Pairing.RankFunction.isPullback
- SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_assoc
- SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn_ι
- SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_assoc
- SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_app_apply
- SSet.Subcomplex.Pairing.RankFunction.mapN_type₁
- SSet.Subcomplex.Pairing.RankFunction.instMonoM
- SSet.Subcomplex.Pairing.RankFunction.exists_or_of_range_m_N
- SSet.Subcomplex.Pairing.RankFunction.Cell.type₁_dim
Ancestors0
No ancestors.