Constructing binary product from pullbacks and terminal object.
If a category has pullbacks and a terminal object, then it has binary products.
TODO: provide the dual result.
def
has_binary_products_of_terminal_and_pullbacks
(C : Type u)
[𝒞 : category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_pullbacks C] :
Any category with pullbacks and terminal object has binary products.
Equations
- has_binary_products_of_terminal_and_pullbacks C = {has_limit := λ (F : category_theory.discrete category_theory.limits.walking_pair ⥤ C), {cone := {X := category_theory.limits.pullback (category_theory.limits.terminal.from (F.obj category_theory.limits.walking_pair.left)) (category_theory.limits.terminal.from (F.obj category_theory.limits.walking_pair.right)) (category_theory.limits.has_limit_of_has_limits_of_shape (category_theory.limits.cospan (category_theory.limits.terminal.from (F.obj category_theory.limits.walking_pair.left)) (category_theory.limits.terminal.from (F.obj category_theory.limits.walking_pair.right)))), π := category_theory.discrete.nat_trans (λ (x : category_theory.discrete category_theory.limits.walking_pair), category_theory.limits.walking_pair.cases_on x category_theory.limits.pullback.fst category_theory.limits.pullback.snd)}, is_limit := {lift := λ (c : category_theory.limits.cone F), category_theory.limits.pullback.lift (c.π.app category_theory.limits.walking_pair.left) (c.π.app category_theory.limits.walking_pair.right) _, fac' := _, uniq' := _}}}