Limits in the over category #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Declare instances for limits in the over category: If C has finite wide pullbacks, over B has
finite limits, and if C has arbitrary wide pullbacks then over B has limits.
@[protected, instance]
def
category_theory.over.category_theory.limits.has_pullbacks
{C : Type u}
[category_theory.category C]
{B : C}
[category_theory.limits.has_pullbacks C] :
Make sure we can derive pullbacks in over B.
@[protected, instance]
def
category_theory.over.category_theory.limits.has_equalizers
{C : Type u}
[category_theory.category C]
{B : C}
[category_theory.limits.has_equalizers C] :
Make sure we can derive equalizers in over B.
@[protected, instance]
@[protected, instance]