Theorems · Definition · category theory
CategoryTheory.Limits.Types.pullbackLimitCone
{X Y Z : Type u} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.cospan f g)The explicit pullback in the category of types, bundled up as a LimitCone
for given f and g.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- CategoryTheory.Limits.WalkingPairstatement · cited by 1,319
- CategoryTheory.Limits.Cone.ptproof · cited by 1,298
- CategoryTheory.Limits.WalkingCospanstatement · cited by 496
- CategoryTheory.Limits.cospanstatement · cited by 467
- TypeCat.ofHomproof · cited by 389
- CategoryTheory.Limits.PullbackConeproof · cited by 136
- CategoryTheory.Limits.PullbackCone.fstproof · cited by 118
- CategoryTheory.Limits.PullbackCone.sndproof · cited by 113
- CategoryTheory.Limits.LimitConestatement · cited by 25
Cited by9
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObjproof · cited by 7
- CategoryTheory.Limits.Types.isPullback_iffproof · cited by 4
- CategoryTheory.Limits.Types.ext_of_isPullbackproof · cited by 2
- CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_fstproof · cited by 2
- CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_sndproof · cited by 2
- CategoryTheory.Limits.PullbackCone.isLimitEquivBijectiveproof · cited by 1
- TypeCat.TransitiveRelation.ofIsTransproof · cited by 0
- CategoryTheory.Limits.Types.pullbackLimitCone_conestatement and proof · cited by 0
- CategoryTheory.Limits.Types.pullbackLimitCone_isLimitstatement and proof · cited by 0