Theorems · Definition · category theory
CategoryTheory.Limits.Types.equalizerLimit
{Y Z : Type u} → {g h : Y ⟶ Z} → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.parallelPair g h)Show that the subtype {x : Y // g x = h x} is an equalizer for the pair (g,h).
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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.Cone.ptproof · cited by 1,298
- CategoryTheory.Limits.WalkingParallelPairstatement · cited by 781
- CategoryTheory.Limits.parallelPairstatement · cited by 766
- TypeCat.ofHomproof · cited by 389
- CategoryTheory.Limits.Fork.ιproof · cited by 162
- CategoryTheory.Limits.Forkproof · cited by 85
- CategoryTheory.Limits.Fork.ofιproof · cited by 66
- CategoryTheory.Limits.LimitConestatement · cited by 25
- CategoryTheory.Limits.Fork.IsLimit.mk'proof · cited by 1
Cited by2
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.Types.equalizerIsoproof · cited by 7
- CategoryTheory.Limits.Types.equalizerIso_inv_comp_ιproof · cited by 3