Structures · Topology
SSet.Subcomplex.Pairing.IsRegular
A proper pairing is regular when the ancestrality relation is well founded.
- Shape
- One type argument · adds wf
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- CategoryTheory.MonoidalCategoryStruct.tensorObj
- SSet.op
How is a type an instance?
Loading the hierarchy index…
Assumed by15
- SSet.Subcomplex.Pairing.innerAnodyneExtensions
- SSet.Subcomplex.Pairing.rankFunction
- SSet.Subcomplex.Pairing.strongAnodyneExtensions
- SSet.Subcomplex.Pairing.anodyneExtensions
- SSet.Subcomplex.Pairing.wf
- SSet.Subcomplex.Pairing.strongInnerAnodyneExtensions
- SSet.Subcomplex.Pairing.IsRegular.wf
- SSet.Subcomplex.Pairing.rank
- SSet.Subcomplex.Pairing.instIsRegularOfIso
- SSet.Subcomplex.Pairing.rank_lt
- SSet.Subcomplex.Pairing.instNonemptyWeakRankFunctionNat
- SSet.Subcomplex.Pairing.instIsRegularOp
- SSet.Subcomplex.Pairing.instIsWellFoundedElemNIIAncestralRel
- SSet.Subcomplex.Pairing.IsRegular.toIsProper
- SSet.Subcomplex.Pairing.instNonemptyRankFunctionNat