Structures · Topology
CompHausLike.HasProp
This wraps the predicate P : TopCat → Prop in a typeclass.
- Shape
- 2 explicit arguments · adds hasProp
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- True
- And
- TotallyDisconnectedSpace
- ExtremallyDisconnected
How is a type an instance?
Loading the hierarchy index…
Assumed by42
- CompHausLike.of
- CompHausLike.ofHom
- CompHausLike.LocallyConstant.fiber
- CompHausLike.LocallyConstant.sigmaIncl
- CompHausLike.sigmaComparison
- CompHausLike.LocallyConstant.counitApp
- CompHausLike.LocallyConstant.counitAppApp
- CompHausLike.isTerminalPUnit
- CompHausLike.LocallyConstant.sigmaIso
- CompHausLike.LocallyConstant.counit
- CompHausLike.LocallyConstant.incl_of_counitAppApp
- CompHausLike.LocallyConstant.presheaf_ext
- CompHausLike.LocallyConstant.unit
- CompHausLike.LocallyConstant.sigmaComparison_comp_sigmaIso
- CompHausLike.LocallyConstant.counitAppAppImage
- CompHausLike.LocallyConstant.adjunction
- CompHausLike.hom_ofHom
- CompHausLike.LocallyConstant.componentHom
- CompHausLike.LocallyConstant.counit_app_hom_app_hom_apply
- CompHausLike.isIsoSigmaComparison
- CompHausLike.cartesianMonoidalCategory
- CompHausLike.productIsLimit
- CompHausLike.coproductIsColimit
- CompHausLike.ofHom_comp
- CompHausLike.LocallyConstant.adjunction_unit
- CompHausLike.coe_of
- CompHausLike.LocallyConstant.counit.congr_simp
- CompHausLike.LocallyConstant.counitAppApp.congr_simp
- CompHausLike.LocallyConstant.counitApp_app
- CompHausLike.sigmaComparison_eq_comp_isos
- CompHausLike.LocallyConstant.unitIso
- CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction
- CompHausLike.LocallyConstant.counitApp.congr_simp
- CompHausLike.LocallyConstant.adjunction_counit
- CompHausLike.LocallyConstant.adjunction_left_triangle
- CompHausLike.HasProp.hasProp
- CompHausLike.LocallyConstant.incl_comap
- CompHausLike.instHasPropSigma
- CompHausLike.LocallyConstant.unit_app
- CompHausLike.coproductCocone
- CompHausLike.productCone
- CompHausLike.ofHom_id
Ancestors0
No ancestors.