Implication Details

Assumptions: cofiltered limits, extensive, terminal object

Conclusions: cocartesian cofiltered limits

Reason: Let C\mathcal{C} be an extensive category with cofiltered limits and a terminal object. Then the coproduct functor C×C≅C/1×C/1→C/(1+1)\mathcal{C} \times \mathcal{C} \cong \mathcal{C}/1 \times \mathcal{C}/1 \to \mathcal{C}/(1+1) is an equivalence. The forgetful functor C/A→C\mathcal{C}/A \to \mathcal{C} creates connected limits, and hence preserves cofiltered limits. For every X∈CX \in \mathcal{C} the functor (X,−):C→C×C(X,-) : \mathcal{C} \to \mathcal{C} \times \mathcal{C} also preserves cofiltered limits. The composition of these functors is X⊔−:C→CX \sqcup - : \mathcal{C} \to \mathcal{C} and therefore also preserves cofiltered limits.