Structures · Category theory
CategoryTheory.ObjectProperty.Nonempty
Nonempty P is a typeclass saying there exists an object X : C that satisfies P.
- Shape
- One type argument · adds exists_prop
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by27
- CategoryTheory.ObjectProperty.arbitrary
- CategoryTheory.ObjectProperty.prop_arbitrary
- CategoryTheory.ObjectProperty.Nonempty.exists_prop
- CategoryTheory.ObjectProperty.exists_prop_of_nonempty
- CategoryTheory.ObjectProperty.nonempty_sup_left
- CategoryTheory.ObjectProperty.instNonemptyStrictMap
- CategoryTheory.ObjectProperty.instNonemptyStrictLimitsClosureStep
- CategoryTheory.ObjectProperty.instNonemptyTriangEnvelope
- CategoryTheory.ObjectProperty.instNonemptyStrictLimitsClosureIter
- CategoryTheory.ObjectProperty.nonempty_iSup
- CategoryTheory.ObjectProperty.Nonempty.mono
- CategoryTheory.ObjectProperty.instNonemptyLimitsClosure
- CategoryTheory.ObjectProperty.instNonemptyMap
- CategoryTheory.ObjectProperty.instNonemptyInd
- CategoryTheory.ObjectProperty.instNonemptyColimitsClosure
- CategoryTheory.ObjectProperty.instNonemptyFullSubcategoryOfNonempty
- CategoryTheory.ObjectProperty.instNonemptyUnopOfOpposite
- CategoryTheory.ObjectProperty.instNonemptyOppositeOp
- CategoryTheory.ObjectProperty.instNonemptyShiftOfIsStableUnderShiftBy
- CategoryTheory.ObjectProperty.nonempty_sup_right
- CategoryTheory.ObjectProperty.instNonemptyRetractClosure
- CategoryTheory.ObjectProperty.instNonemptyExtensionProduct
- CategoryTheory.ObjectProperty.instNonemptyExtensionProductIter
- CategoryTheory.ObjectProperty.IsStableUnderRetracts.instContainsZeroOfHasZeroObjectOfNonempty
- CategoryTheory.ObjectProperty.instNonemptyShiftClosure
- CategoryTheory.ObjectProperty.instIsTriangulatedTriangEnvelopeOfNonemptyOfIsTriangulated
- CategoryTheory.ObjectProperty.instNonemptyIsoClosure
Ancestors0
No ancestors.