Structures · Topology
CompHausLike.HasExplicitFiniteCoproducts
A typeclass describing the property that forming all finite disjoint unions is stable under the
property P.
- Shape
- One type argument · 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 by54
- CompHausLike.LocallyConstant.functor
- CompHausLike.sigmaComparison
- CompHausLike.LocallyConstant.counitApp
- CompHausLike.LocallyConstant.counitAppApp
- CompHausLike.LocallyConstant.sigmaIso
- CompHausLike.LocallyConstant.counit
- TopCat.toSheafCompHausLike
- CompHausLike.LocallyConstant.incl_of_counitAppApp
- CompHausLike.LocallyConstant.presheaf_ext
- CompHausLike.LocallyConstantModule.functor
- CompHausLike.LocallyConstant.unit
- CompHausLike.LocallyConstant.sigmaComparison_comp_sigmaIso
- CompHausLike.LocallyConstant.adjunction
- topCatToSheafCompHausLike
- CompHausLike.LocallyConstant.functor_map_hom_app
- CompHausLike.LocallyConstant.functor_obj_obj_obj
- CompHausLike.hasPullbacksOfInclusions
- CompHausLike.LocallyConstant.functor_obj_obj
- CompHausLike.LocallyConstant.counit_app_hom_app_hom_apply
- CompHausLike.finitaryExtensive
- CompHausLike.precoherent
- CompHausLike.isIsoSigmaComparison
- CompHausLike.LocallyConstant.adjunction_unit
- CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions
- CompHausLike.LocallyConstant.functor_obj_obj_map
- CompHausLike.instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite
- CompHausLike.LocallyConstant.counit.congr_simp
- CompHausLike.LocallyConstant.counitAppApp.congr_simp
- CompHausLike.LocallyConstant.counitApp_app
- CompHausLike.LocallyConstant.functorToPresheavesIso
- CompHausLike.sigmaComparison_eq_comp_isos
- CompHausLike.LocallyConstantModule.functor_obj_obj_map_hom_apply_apply
- CompHausLike.LocallyConstant.functorIso
- CompHausLike.instHasFiniteCoproductsOfHasExplicitFiniteCoproducts
- topCatToSheafCompHausLike_obj
- CompHausLike.instHasPullbacksOfInclusionsOfHasExplicitPullbacksOfInclusions
- CompHausLike.instPreservesFiniteCoproductsTopCatCompHausLikeToTopOfHasExplicitFiniteCoproducts
- CompHausLike.LocallyConstant.unitIso
- CompHausLike.LocallyConstantModule.functor_map_hom_app_hom_apply_apply
- CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks
- CompHausLike.instPreservesPullbacksOfInclusionsTopCatCompHausLikeToTopOfHasExplicitPullbacksOfInclusions
- CompHausLike.LocallyConstant.functor_map_hom
- CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction
- CompHausLike.LocallyConstant.counitApp.congr_simp
- CompHausLike.LocallyConstant.adjunction_counit
- CompHausLike.LocallyConstant.adjunction_left_triangle
- TopCat.toSheafCompHausLike_obj_map
- TopCat.toSheafCompHausLike_obj_obj
- CompHausLike.instHasPropSigma
- CompHausLike.LocallyConstantModule.functor_obj_obj_obj_carrier
Ancestors0
No ancestors.