Structures · Category theory
CategoryTheory.Limits.HasStrictTerminalObjects
We say C has strict terminal objects if every terminal object is strict, i.e. given any
morphism f : I ⟶ A where I is terminal, then f is an isomorphism.
Strictly speaking, this says that any terminal object must be strict, rather than that strict
terminal objects exist.
- Shape
- One type argument · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances1
- CommRingCat
How is a type an instance?
Loading the hierarchy index…
Assumed by22
- CategoryTheory.underEquivOfIsTerminal
- CategoryTheory.MorphismProperty.underEquivOfIsTerminal
- CategoryTheory.Limits.IsTerminal.isIso_from
- CategoryTheory.Limits.IsTerminal.strict_hom_ext
- CategoryTheory.Limits.IsTerminal.subsingleton_to
- CategoryTheory.Limits.HasStrictTerminalObjects.out
- CategoryTheory.Limits.terminal.strict_hom_ext
- CategoryTheory.MorphismProperty.underEquivOfIsTerminal_functor
- CategoryTheory.underEquivOfIsTerminal_functor
- CategoryTheory.MorphismProperty.underEquivOfIsTerminal_unitIso
- CategoryTheory.Limits.terminal.strict_hom_ext_iff
- CategoryTheory.underEquivOfIsTerminal_unitIso
- CategoryTheory.Limits.terminal_isIso_from
- CategoryTheory.underEquivOfIsTerminal_counitIso
- AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenImmersion_aux
- CategoryTheory.Limits.terminal.subsingleton_to
- AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenImmersion
- CategoryTheory.MorphismProperty.underEquivOfIsTerminal_counitIso
- CategoryTheory.Limits.limit_π_isIso_of_is_strict_terminal
- CategoryTheory.underEquivOfIsTerminal_inverse
- CategoryTheory.MorphismProperty.underEquivOfIsTerminal_inverse
- CategoryTheory.Limits.IsTerminal.ofStrict
Ancestors0
No ancestors.