Structures · Lean core
CoeSort
CoeSort α β is a coercion to a sort. β must be a universe, and this is
triggered when a : α appears in a place where a type is expected, like
(x : a) or a → a.
CoeSort instances apply to CoeOut as well.
- Defined in
- Init.Coe
- Shape
- 2 explicit arguments · adds coe
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Concrete types that are instances100
- Bool
- ModuleCat
- AlgebraicGeometry.Scheme
- AddCommGrpCat
- TopCat
- Rep
- CommGrpCat
- GrpCat
- AddGrpCat
- CategoryTheory.Skeleton
- CommRingCat
- AlgebraicGeometry.SheafedSpace
- CommRing.Pic
- AlgebraicGeometry.LocallyRingedSpace
- CategoryTheory.Under
- CategoryTheory.InducedCategory
- ContinuousGeneratedByCat
- AlgCat
- AlgebraicGeometry.PresheafedSpace
- CommMonCat
- ProfiniteGrp
- AddCommMonCat
- MonCat
- AddMonCat
- CompHausLike
- QuadraticModuleCat
- SemimoduleCat
- TopModuleCat
- CommAlgCat
- PartOrdEmb
- RingCat
- CommSemiRingCat
- HopfAlgCat
- BialgCat
- TopRep
- AddSemigrp
- Semigrp
- SemiRingCat
- CoalgCat
- CommBialgCat
- Sequential
- TopCommRingCat
- Preord
- Compactum
- CommHopfAlgCat
- CompactlyGenerated
- FinBddDistLat
- HeytAlg
- AlexDisc
- BddOrd
- BoolAlg
- AddMagmaCat
- ProfiniteAddGrp
- LinOrd
- Frm
- BddDistLat
- BoolRing
- FGModuleRepr
- FinTopCat
- MagmaCat
- FiniteGrp
- FiniteAddGrp
- Lat
- DistLat
- PartOrd
- FGModuleCat
- CategoryTheory.Mat
- CategoryTheory.InducedWideCategory
- CategoryTheory.Cat
- GeneratedByTopCat
- FiniteGaloisIntermediateField
- DiscreteQuotient
- FintypeCat
- SFinKer
- FDRep
- SemiNormedGrp
- CompHaus
- SemiNormedGrp₁
- UniformSpaceCat
- FinBoolAlg
- NonemptyFinLinOrd
- FinPartOrd
- SemilatInfCat
- CategoryTheory.Bicategory.InducedBicategory
- CompleteLat
- CpltSepUniformSpace
- CategoryTheory.EnrichedCat
- SemilatSupCat
- BddLat
- TwoP
- GrpWithZero
- ωCPO
- Bipointed
- Born
- MeasCat
- Pointed
- CategoryTheory.Grpd
- FirstOrder.Language.Theory.ModelType
- WideSubquiver
- CategoryTheory.Bundled
How is a type an instance?
Loading the hierarchy index…