IsTerminal

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean

Statistics

Metric	Count
Definitions isInitialConst, isTerminalConst, IsTerminal, InitialMonoClass, IsInitial, equivOfIso, ofIso, ofUnique, ofUniqueHom, op, to, uniqueUpToIso, unop, IsTerminal, equivOfIso, from, ofIso, ofUnique, ofUniqueHom, op, uniqueUpToIso, unop, asEmptyCocone, asEmptyCone, coconeOfDiagramInitial, coconeOfDiagramTerminal, colimitOfDiagramInitial, colimitOfDiagramTerminal, coneOfDiagramInitial, coneOfDiagramTerminal, initialOpOfTerminal, initialUnopOfTerminal, isColimitChangeEmptyCocone, isColimitEmptyCoconeEquiv, isColimitEquivIsInitialOfIsEmpty, isInitialBot, isInitialEquivUnique, isLimitChangeEmptyCone, isLimitEmptyConeEquiv, isLimitEquivIsTerminalOfIsEmpty, isTerminalEquivUnique, isTerminalTop, limitOfDiagramInitial, limitOfDiagramTerminal, terminalOpOfInitial, terminalUnopOfInitial	46
Theorems isInitialConst_to_app, isTerminalConst_from_app, isInitial_mono_from, of_isInitial, of_isTerminal, isIso_ι_app_of_isTerminal, epi_to, hom_ext, isSplitEpi_to, mono_from, to_comp, to_self, uniqueUpToIso_hom, uniqueUpToIso_inv, isIso_π_app_of_isInitial, comp_from, from_self, hom_ext, isSplitMono_from, mono_from, uniqueUpToIso_hom, uniqueUpToIso_inv, asEmptyCocone_pt, asEmptyCocone_ι_app, asEmptyCone_pt, asEmptyCone_π_app, coconeOfDiagramInitial_pt, coconeOfDiagramInitial_ι_app, coconeOfDiagramTerminal_pt, coconeOfDiagramTerminal_ι_app, coneOfDiagramInitial_pt, coneOfDiagramInitial_π_app, coneOfDiagramTerminal_pt, coneOfDiagramTerminal_π_app, isIso_of_isInitial, isIso_of_isTerminal	36
Total	82

CategoryTheory.Functor

Definitions

Name	Category	Theorems
isInitialConst 📖	CompOp	1 math math: isInitialConst_to_app
isTerminalConst 📖	CompOp	5 math math: CategoryTheory.Presheaf.comp_χ_eq, CategoryTheory.Presheaf.isPullback_χ_truth, CategoryTheory.Presheaf.classifier_χ₀, isTerminalConst_from_app, CategoryTheory.Sheaf.isTerminalTerminal_from_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isInitialConst_to_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category const CategoryTheory.Limits.IsInitial.to isInitialConst	—	—
isTerminalConst_from_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category const CategoryTheory.Limits.IsTerminal.from isTerminalConst	—	—

CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram

Definitions

Name	Category	Theorems
IsTerminal 📖	CompData	1 math math: IsTerminal.instSubsingleton

CategoryTheory.Limits

Definitions

Name	Category	Theorems
InitialMonoClass 📖	CompData	7 math math: initial_mono_of_strict_initial_objects, initialMonoClass_of_coproductsDisjoint, InitialMonoClass.of_isTerminal, InitialMonoClass.of_terminal, HasZeroObject.initialMonoClass, InitialMonoClass.of_initial, InitialMonoClass.of_isInitial
IsInitial 📖	CompOp	8 math math: CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty, Types.initial_iff_empty, IsInitial.to_eq_descCoconeMorphism, AlgebraicGeometry.isInitial_iff_isEmpty, IsColimit.descCoconeMorphism_eq_isInitial_to, CoproductDisjoint.nonempty_isInitial_of_ne, Concrete.initial_of_empty_of_reflects, Concrete.initial_iff_empty_of_preserves_of_reflects
IsTerminal 📖	CompOp	9 math math: IsLimit.liftConeMorphism_eq_isTerminal_from, CategoryTheory.PreGaloisCategory.isGalois_iff_aux, TopCat.Presheaf.isSheaf_on_punit_iff_isTerminal, CategoryTheory.PreGaloisCategory.IsGalois.quotientByAutTerminal, SkyscraperPresheafFunctor.map'_app, IsTerminal.from_eq_liftConeMorphism, TopCat.Presheaf.isSheaf_iff_isTerminal_of_indiscrete, skyscraperPresheaf_map, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app
asEmptyCocone 📖	CompOp	3 math math: asEmptyCocone_pt, CategoryTheory.IsInitial.isVanKampenColimit, asEmptyCocone_ι_app
asEmptyCone 📖	CompOp	3 math math: CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift_hom, asEmptyCone_pt, asEmptyCone_π_app
coconeOfDiagramInitial 📖	CompOp	2 math math: coconeOfDiagramInitial_ι_app, coconeOfDiagramInitial_pt
coconeOfDiagramTerminal 📖	CompOp	3 math math: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc, coconeOfDiagramTerminal_ι_app, coconeOfDiagramTerminal_pt
colimitOfDiagramInitial 📖	CompOp	—
colimitOfDiagramTerminal 📖	CompOp	2 math math: CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit
coneOfDiagramInitial 📖	CompOp	2 math math: coneOfDiagramInitial_π_app, coneOfDiagramInitial_pt
coneOfDiagramTerminal 📖	CompOp	2 math math: coneOfDiagramTerminal_π_app, coneOfDiagramTerminal_pt
initialOpOfTerminal 📖	CompOp	—
initialUnopOfTerminal 📖	CompOp	—
isColimitChangeEmptyCocone 📖	CompOp	—
isColimitEmptyCoconeEquiv 📖	CompOp	—
isColimitEquivIsInitialOfIsEmpty 📖	CompOp	—
isInitialBot 📖	CompOp	—
isInitialEquivUnique 📖	CompOp	—
isLimitChangeEmptyCone 📖	CompOp	—
isLimitEmptyConeEquiv 📖	CompOp	—
isLimitEquivIsTerminalOfIsEmpty 📖	CompOp	—
isTerminalEquivUnique 📖	CompOp	—
isTerminalTop 📖	CompOp	1 math math: CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit
limitOfDiagramInitial 📖	CompOp	—
limitOfDiagramTerminal 📖	CompOp	—
terminalOpOfInitial 📖	CompOp	—
terminalUnopOfInitial 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asEmptyCocone_pt 📖	mathematical	—	Cocone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty asEmptyCocone	—	—
asEmptyCocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cocone.ι asEmptyCocone Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
asEmptyCone_pt 📖	mathematical	—	Cone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty asEmptyCone	—	—
asEmptyCone_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.empty Cone.π asEmptyCone Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
coconeOfDiagramInitial_pt 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	Cocone.pt coconeOfDiagramInitial CategoryTheory.Functor.obj	—	—
coconeOfDiagramInitial_ι_app 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cocone.ι coconeOfDiagramInitial CategoryTheory.inv CategoryTheory.Functor.map IsInitial.to	—	—
coconeOfDiagramTerminal_pt 📖	mathematical	—	Cocone.pt coconeOfDiagramTerminal CategoryTheory.Functor.obj	—	—
coconeOfDiagramTerminal_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cocone.ι coconeOfDiagramTerminal CategoryTheory.Functor.map IsTerminal.from	—	—
coneOfDiagramInitial_pt 📖	mathematical	—	Cone.pt coneOfDiagramInitial CategoryTheory.Functor.obj	—	—
coneOfDiagramInitial_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cone.π coneOfDiagramInitial CategoryTheory.Functor.map IsInitial.to	—	—
coneOfDiagramTerminal_pt 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	Cone.pt coneOfDiagramTerminal CategoryTheory.Functor.obj	—	—
coneOfDiagramTerminal_π_app 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cone.π coneOfDiagramTerminal CategoryTheory.inv CategoryTheory.Functor.map IsTerminal.from	—	—
isIso_of_isInitial 📖	mathematical	—	CategoryTheory.IsIso	—	IsInitial.to_comp IsInitial.to_self IsInitial.hom_ext
isIso_of_isTerminal 📖	mathematical	—	CategoryTheory.IsIso	—	IsTerminal.comp_from IsTerminal.from_self IsTerminal.hom_ext

CategoryTheory.Limits.InitialMonoClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isInitial_mono_from 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.IsInitial.to	—	—
of_isInitial 📖	mathematical	CategoryTheory.Mono CategoryTheory.Limits.IsInitial.to	CategoryTheory.Limits.InitialMonoClass	—	CategoryTheory.Limits.IsInitial.hom_ext CategoryTheory.mono_comp CategoryTheory.IsSplitMono.mono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom
of_isTerminal 📖	mathematical	—	CategoryTheory.Limits.InitialMonoClass	—	of_isInitial CategoryTheory.mono_of_mono_fac CategoryTheory.Limits.IsInitial.hom_ext

CategoryTheory.Limits.IsColimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_ι_app_of_isTerminal 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.Iso.isIso_hom

CategoryTheory.Limits.IsInitial

Definitions

Name	Category	Theorems
equivOfIso 📖	CompOp	—
ofIso 📖	CompOp	—
ofUnique 📖	CompOp	—
ofUniqueHom 📖	CompOp	—
op 📖	CompOp	—
to 📖	CompOp	59 math math: SSet.RelativeMorphism.botEquiv_symm_apply_map, CategoryTheory.Limits.InitialMonoClass.isInitial_mono_from, CategoryTheory.WithInitial.opEquiv_unitIso_inv_app, CategoryTheory.Under.forgetMapInitial_inv_app, CategoryTheory.WithInitial.liftToInitialUnique_hom_app, CategoryTheory.Under.equivalenceOfIsInitial_counitIso, CategoryTheory.StructuredArrow.IsUniversal.uniq, CategoryTheory.Limits.CoproductDisjoint.isPullback_of_isInitial, CategoryTheory.Limits.initialIsoIsInitial_hom, CategoryTheory.WithInitial.opEquiv_counitIso_hom_app, SSet.Homotopy.h₁_assoc, CategoryTheory.WithTerminal.opEquiv_counitIso_inv_app, CategoryTheory.Limits.coneOfDiagramInitial_π_app, CategoryTheory.WithTerminal.opEquiv_unitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_counitIso_hom_app, CategoryTheory.initial_mono, to_eq_descCoconeMorphism, to_self, CategoryTheory.WithInitial.liftStar_lift_map, CategoryTheory.WithInitial.inclLiftToInitial_inv_app, CategoryTheory.WithInitial.mkCommaObject_hom_app, CategoryTheory.Limits.initialIsoIsInitial_inv, SSet.Homotopy.h₀, CategoryTheory.WithInitial.starIsoInitial_inv, SSet.RelativeMorphism.botEquiv_apply, CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial, to_comp, CategoryTheory.Under.forgetMapInitial_hom_app, CategoryTheory.WithInitial.equivComma_functor_obj_hom_app, CategoryTheory.Limits.IsColimit.descCoconeMorphism_eq_isInitial_to, CategoryTheory.Under.equivalenceOfIsInitial_unitIso, CategoryTheory.Limits.coconeOfDiagramInitial_ι_app, AlgebraicGeometry.emptyIsInitial_to, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, CategoryTheory.CosimplicialObject.augmentOfIsInitial_hom_app, CategoryTheory.WithInitial.opEquiv_counitIso_inv_app, SSet.Homotopy.h₀_assoc, CategoryTheory.WithInitial.inclLiftToInitial_hom_app, SSet.Homotopy.h₁, CategoryTheory.Limits.isInitialMul_inv, uniqueUpToIso_inv, CategoryTheory.zeroMul_inv, CategoryTheory.IsPushout.of_is_coproduct, CategoryTheory.Functor.isInitialConst_to_app, uniqueUpToIso_hom, CategoryTheory.Limits.mulIsInitial_inv, CategoryTheory.WithInitial.starIsoInitial_hom, CategoryTheory.WithInitial.liftToInitial_map, CategoryTheory.Under.equivalenceOfIsInitial_inverse_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, CategoryTheory.Under.mkIdInitial_to_right, CategoryTheory.Under.equivalenceOfIsInitial_inverse_obj, CategoryTheory.IsPushout.of_is_coproduct', CategoryTheory.WithInitial.opEquiv_inverse_map, CategoryTheory.WithInitial.liftToInitialUnique_inv_app, CategoryTheory.WithInitial.opEquiv_unitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_unitIso_inv_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app, CategoryTheory.WithTerminal.opEquiv_functor_map
uniqueUpToIso 📖	CompOp	2 math math: uniqueUpToIso_inv, uniqueUpToIso_hom
unop 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_to 📖	mathematical	—	CategoryTheory.Epi	—	CategoryTheory.IsSplitEpi.epi isSplitEpi_to
hom_ext 📖	—	—	—	—	CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.instIsEmptyDiscrete PEmpty.instIsEmpty
isSplitEpi_to 📖	mathematical	—	CategoryTheory.IsSplitEpi	—	CategoryTheory.IsSplitEpi.mk' hom_ext
mono_from 📖	mathematical	—	CategoryTheory.Mono	—	hom_ext CategoryTheory.Limits.InitialMonoClass.isInitial_mono_from
to_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct to	—	hom_ext
to_self 📖	mathematical	—	to CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	hom_ext
uniqueUpToIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom uniqueUpToIso to	—	—
uniqueUpToIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv uniqueUpToIso to	—	—

CategoryTheory.Limits.IsLimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_π_app_of_isInitial 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	CategoryTheory.Iso.isIso_hom

CategoryTheory.Limits.IsTerminal

Definitions

Name	Category	Theorems
equivOfIso 📖	CompOp	—
from 📖	CompOp	76 math math: CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerve_hom_app, CategoryTheory.Limits.IsLimit.liftConeMorphism_eq_isTerminal_from, CategoryTheory.WithInitial.opEquiv_unitIso_inv_app, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, CategoryTheory.Sheaf.isPullback_χ_truth, CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal, CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_χ₀, CategoryTheory.Over.forgetMapTerminal_hom_app, CategoryTheory.Over.equivalenceOfIsTerminal_counitIso, CategoryTheory.IsSubterminal.mono_isTerminal_from, CategoryTheory.WithInitial.opEquiv_functor_map, CategoryTheory.Presheaf.comp_χ_eq, CategoryTheory.WithInitial.opEquiv_counitIso_hom_app, CategoryTheory.Limits.coneOfDiagramTerminal_π_app, CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve_hom_left, CategoryTheory.WithTerminal.opEquiv_counitIso_inv_app, CategoryTheory.WithTerminal.opEquiv_unitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_counitIso_hom_app, CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve_inv_left, CategoryTheory.WithTerminal.liftToTerminal_map, CategoryTheory.IsPullback.of_is_product', CategoryTheory.SimplicialObject.augmentOfIsTerminal_hom_app, CategoryTheory.Over.equivalenceOfIsTerminal_inverse_map, CategoryTheory.Over.forgetMapTerminal_inv_app, uniqueUpToIso_hom, CategoryTheory.Classifier.isTerminalFrom_eq_χ₀, CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerve_inv_app, CategoryTheory.WithTerminal.liftToTerminalUnique_inv_app, CategoryTheory.WithTerminal.lift_map_liftStar, CategoryTheory.WithTerminal.inclLiftToTerminal_inv_app, CategoryTheory.Limits.Types.isTerminalPUnit_from_apply, CategoryTheory.Over.equivalenceOfIsTerminal_inverse_obj, CategoryTheory.WithTerminal.equivComma_functor_obj_hom_app, CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_inv_π_assoc, CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_hom_π_assoc, CategoryTheory.Sheaf.classifier_χ₀, CategoryTheory.WithTerminal.starIsoTerminal_inv, CategoryTheory.Limits.FormalCoproduct.instHasWidePullbackFinHAddNatOfNatRightMkFromIsTerminalInclLeftHom, CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_hom_π, CategoryTheory.Limits.coconeOfDiagramTerminal_ι_app, CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve_hom_right, comp_from, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, CategoryTheory.WithTerminal.starIsoTerminal_hom, CategoryTheory.Limits.FormalCoproduct.instHasLimitWidePullbackShapeToTypeSimplexCategoryOrderHomFinHAddNatLenOfNatWideCospanObjInclFromIsTerminalIncl, CategoryTheory.Limits.terminalIsoIsTerminal_hom, CategoryTheory.WithInitial.opEquiv_counitIso_inv_app, uniqueUpToIso_inv, CategoryTheory.Presheaf.isPullback_χ_truth, CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_inv_π, CategoryTheory.WithTerminal.mkCommaObject_hom_app, CategoryTheory.Over.equivalenceOfIsTerminal_unitIso, CategoryTheory.WithTerminal.inclLiftToTerminal_hom_app, AlgebraicGeometry.Scheme.emptyTo_c_app, CategoryTheory.Subobject.Classifier.isTerminalFrom_eq_χ₀, from_self, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, CategoryTheory.CostructuredArrow.IsUniversal.uniq, CategoryTheory.Limits.terminalIsoIsTerminal_inv, CategoryTheory.Presheaf.classifier_χ₀, SkyscraperPresheafFunctor.map'_app, CategoryTheory.SemiCartesianMonoidalCategory.fst_def, CategoryTheory.Over.mkIdTerminal_from_left, CategoryTheory.Functor.isTerminalConst_from_app, CategoryTheory.constantPresheafAdj_counit_app_app, CategoryTheory.WithInitial.opEquiv_unitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_unitIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map, from_eq_liftConeMorphism, CategoryTheory.WithTerminal.liftToTerminalUnique_hom_app, CategoryTheory.IsPullback.of_is_product, CategoryTheory.SemiCartesianMonoidalCategory.snd_def, skyscraperPresheaf_map, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app, CategoryTheory.WithTerminal.opEquiv_inverse_map, CategoryTheory.Sheaf.isTerminalTerminal_from_hom
ofIso 📖	CompOp	—
ofUnique 📖	CompOp	—
ofUniqueHom 📖	CompOp	—
op 📖	CompOp	—
uniqueUpToIso 📖	CompOp	2 math math: uniqueUpToIso_hom, uniqueUpToIso_inv
unop 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_from 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct from	—	hom_ext
from_self 📖	mathematical	—	from CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	hom_ext
hom_ext 📖	—	—	—	—	CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.instIsEmptyDiscrete PEmpty.instIsEmpty
isSplitMono_from 📖	mathematical	—	CategoryTheory.IsSplitMono	—	CategoryTheory.IsSplitMono.mk' hom_ext
mono_from 📖	mathematical	—	CategoryTheory.Mono	—	CategoryTheory.IsSplitMono.mono isSplitMono_from
uniqueUpToIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom uniqueUpToIso from	—	—
uniqueUpToIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv uniqueUpToIso from	—	—

---

← Back to Index