Structures · Topology
CompHausLike.HasExplicitPullbacks
A typeclass describing the property that forming all explicit pullbacks 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 instances3
- True
- And
- TotallyDisconnectedSpace
How is a type an instance?
Loading the hierarchy index…
Assumed by34
- CompHausLike.preregular
- CompHausLike.LocallyConstant.functor
- CompHausLike.LocallyConstant.counit
- TopCat.toSheafCompHausLike
- CompHausLike.LocallyConstantModule.functor
- CompHausLike.LocallyConstant.unit
- CompHausLike.LocallyConstant.adjunction
- topCatToSheafCompHausLike
- CompHausLike.LocallyConstant.functor_map_hom_app
- CompHausLike.LocallyConstant.functor_obj_obj_obj
- CompHausLike.LocallyConstant.functor_obj_obj
- CompHausLike.LocallyConstant.counit_app_hom_app_hom_apply
- CompHausLike.precoherent
- CompHausLike.LocallyConstant.adjunction_unit
- CompHausLike.LocallyConstant.functor_obj_obj_map
- CompHausLike.LocallyConstant.counit.congr_simp
- CompHausLike.instHasPullbacksOfHasExplicitPullbacks
- CompHausLike.LocallyConstant.functorToPresheavesIso
- CompHausLike.LocallyConstantModule.functor_obj_obj_map_hom_apply_apply
- CompHausLike.LocallyConstant.functorIso
- topCatToSheafCompHausLike_obj
- CompHausLike.LocallyConstant.unitIso
- CompHausLike.LocallyConstantModule.functor_map_hom_app_hom_apply_apply
- CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks
- CompHausLike.HasExplicitPullbacks.hasProp
- CompHausLike.LocallyConstant.functor_map_hom
- CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction
- CompHausLike.LocallyConstant.adjunction_counit
- CompHausLike.LocallyConstant.adjunction_left_triangle
- TopCat.toSheafCompHausLike_obj_map
- TopCat.toSheafCompHausLike_obj_obj
- CompHausLike.LocallyConstantModule.functor_obj_obj_obj_carrier
- CompHausLike.LocallyConstant.unit_app
- topCatToSheafCompHausLike_map_hom_app
Ancestors0
No ancestors.