Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Limits.WidePullbackShape

Type w → Type w

A wide pullback shape for any type J can be written simply as Option J.

Defined in
Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Cited by
94 results in Mathlib
Foundations
Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.Limits.WalkingCospan · cited by 496Limits.WalkingCospanCategoryTheory.Limits.WidePullbackShape.wideCospan · cited by 22WidePullbackShape.wideCos…CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver · cited by 16ConstructProducts.widePul…CategoryTheory.Limits.widePullbackShapeOp · cited by 11Limits.widePullbackShapeOpCategoryTheory.Limits.widePushoutShapeOp · cited by 11Limits.widePushoutShapeOpCategoryTheory.Over.ConstructProducts.conesEquivFunctor · cited by 10ConstructProducts.conesEq…CategoryTheory.Over.ConstructProducts.conesEquivInverse · cited by 9ConstructProducts.conesEq…CategoryTheory.Limits.widePullbackShapeUnop · cited by 9Limits.widePullbackShapeU…CategoryTheory.Limits.widePushoutShapeUnop · cited by 9Limits.widePushoutShapeUn…CategoryTheory.Limits.WidePullbackShape.mkCone · cited by 8WidePullbackShape.mkConeCategoryTheory.Limits.WidePullbackCone.base · cited by 7WidePullbackCone.baseCategoryTheory.Limits.WidePullbackCone.π · cited by 7WidePullbackCone.πCategoryTheory.Limits.HasWidePullbacks · cited by 6Limits.HasWidePullbacksCategoryTheory.Limits.widePullbackShapeOpEquiv · cited by 6Limits.widePullbackShapeO…CategoryTheory.Limits.widePushoutShapeOpEquiv · cited by 6Limits.widePushoutShapeOp…Limits.WidePullbackShapeCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by149

Results whose statement or proof uses this declaration.