• definition
  • a category $\mathcal{C}$ is cartesian if
    • for any two objects $A$ and $B$ they have a product
    • and $\mathcal{C}$ has a terminal object $1$
• equivalently, for any finite set $I$ and and $I$-indexed family $A_{(-)}: I \to \mathcal{C}$ of objects, there’s a product $\Pi_{i \in I} A_{i}$ in $\mathcal{C}$
• cartesian functor
  • a functor between two cartesian categories is said to be cartesian if it preserve the product and terminal object
  • which means, for two objects in the domain category, their product in the domain category is sent to codomain category and behave as the product of …