Total Products

Let ℰ → ℬ → ℰ ℬ \mathcal{E}\to\mathcal{B} be a Displayed category with ℬ ℬ \mathcal{B} Cartesian. We say that ℰ ℰ \mathcal{E} has total products if the Total Category ∫ ℰ ℰ \int\mathcal{E} is itself Cartesian.

In displayed terms, this means that for a , b : ℬ : 𝑎 𝑏 ℬ a,b:\mathcal{B} and x : ℰ a , y : ℰ b : 𝑥 subscript ℰ 𝑎 𝑦 : subscript ℰ 𝑏 x:\mathcal{E}_{a},y:\mathcal{E}_{b} , we have a product x × y : ℰ a × b : 𝑥 𝑦 subscript ℰ 𝑎 𝑏 x\times y:\mathcal{E}_{a\times b} where the projections are appropriately displayed over the projections in ℬ ℬ \mathcal{B} .