\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{cartesian product}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{limits_and_colimits}{}\paragraph*{{Limits and colimits}}\label{limits_and_colimits}

[[!include infinity-limits - contents]]

\hypertarget{monoidal_categories}{}\paragraph*{{Monoidal categories}}\label{monoidal_categories}

[[!include monoidal categories - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{Definition}{Definition}\dotfill \pageref*{Definition} \linebreak
\noindent\hyperlink{in_sets}{In Sets}\dotfill \pageref*{in_sets} \linebreak
\noindent\hyperlink{InAGeneraCategory}{In a general category}\dotfill \pageref*{InAGeneraCategory} \linebreak
\noindent\hyperlink{as_a_functor}{As a functor}\dotfill \pageref*{as_a_functor} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{products_of_sets}{Products of sets}\dotfill \pageref*{products_of_sets} \linebreak
\noindent\hyperlink{further_examples}{Further examples}\dotfill \pageref*{further_examples} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{relation_to_type_theory}{Relation to type theory}\dotfill \pageref*{relation_to_type_theory} \linebreak
\noindent\hyperlink{foundational_status}{Foundational status}\dotfill \pageref*{foundational_status} \linebreak
\noindent\hyperlink{related_entries}{Related entries}\dotfill \pageref*{related_entries} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

In the strict sense of the word, a \emph{cartesian product} is a [[product]] in [[Set]], the [[category]] of [[sets]]. Hence for $S_1$ and $S_2$ two [[sets]], their cartesian product is the set denoted $S_1\times S_2$ whose [[elements]] are [[ordered pairs]] of elements in $S_1$ and $S_2$, respectively.

The abstract concept of such [[products]] generalizes from [[Set]] to any other [[category]] (as a special case of a category-theoretic \emph{[[limit]]}), only that in general products of any given [[objects]] may or may not actually exist in that category.

(If they all exist, then one speaks of a [[cartesian monoidal category]]. Especially if the category is also a [[monoidal category]] with respect to some other [[tensor product]], then one says ``Cartesian product'' to distinguish the two. For instance one speaks of the cartesian product on [[Cat]] and on [[2Cat]] in contrast to the [[Gray tensor product]].)

A product [[created limit|created]] by the [[forgetful functor]] of a [[concrete category]], especially in [[algebra]], is often called a [[direct product]] (for instance a [[direct product of groups]]).

\hypertarget{Definition}{}\subsection*{{Definition}}\label{Definition}

\hypertarget{in_sets}{}\subsubsection*{{In Sets}}\label{in_sets}

Given any family $(A_i)_{i:I}$ of sets, the \textbf{cartesian product} $\prod_i A_i$ of the family is the set of all [[functions]] $f$ from the index set $I$ with $f_j$ in $A_j$ for each $j$ in $I$.

As stated, the [[target]] of such a function depends on the argument, which is natural in dependent [[type theory]]; but if you don't like this, then define $\prod_i A_i$ to be the set of those functions $f$ from $I$ to the [[disjoint union]] $\biguplus_i A_i$ such that $f_j \in A_j$ (treating $A_j$ as a [[subset]] of $\biguplus_i A_i$ as usual) for each $j$ in $I$.

In traditional forms of [[set theory]], one can also take the target of $f$ to be the [[union]] $\bigcup_i A_i$ or even the class of all objects (equivalently, leave it unspecified).

\hypertarget{InAGeneraCategory}{}\subsubsection*{{In a general category}}\label{InAGeneraCategory}

Given any [[category]] $\mathcal{C}$, and any set $\{X_i\}_{i \in I}$ of its [[objects]], then the product of all these objects is, if it exists, an object denoted

\begin{displaymath}
\underset{i \in I}{\prod} X_i
  \in 
  \mathcal{C}
\end{displaymath}
and equipped with [[morphisms]]

\begin{displaymath}
p_i \;\colon\; \left(\underset{i \in I}{\prod} X_i\right)
   \longrightarrow 
  X_i
\end{displaymath}
(the \emph{[[projections]]}), for each $i \in I$, such that it is [[universal property|universal with this property]], i.e. such that given any other object $Q \in \mathcal{C}$ with morphisms

\begin{displaymath}
Q \overset{f_i}{\longrightarrow}  X_i
\end{displaymath}
for $i \in I$, then there is a \emph{unique} morphism

\begin{displaymath}
(f_i)_{i \in I}
  \;\colon\; 
  Q \longrightarrow \underset{i \in I}{\prod} X_i
\end{displaymath}
which factors the $f_i$ through the $p_i$, i.e. such that all these [[commuting diagram|diagrams commute]]:

\begin{displaymath}
\itexarray{
    Q 
    \\  
    {}^{\mathllap{(f_i)_{i \in I}}}\downarrow & \searrow^{\mathrlap{f_i}}
    \\
    \underset{i \in I}{\prod} X_i &\underset{p_i}{\longrightarrow}& X_i
  }
\end{displaymath}
for all $i \in I$.

The case of a binary products it is also denoted by ``$(-)\times(-)$'':

\begin{displaymath}
\itexarray{
    && Q
    \\
    & \swarrow &\downarrow^{\mathrlap{\exists !}}& \searrow
    \\
    X_1 &\overset{p_1}{\longleftarrow}& X_1 \times X_2 &\overset{p_2}{\longrightarrow}& X_2
  }
  \,.
\end{displaymath}
An important special case is a [[power]] of an object $X$, where (referring to notation above) we take all $X_i$ to be $X$ and form

\begin{displaymath}
X^I = \prod_{i \in I} X
\end{displaymath}
Referring to notation above, if we take $Q = X$ and all $f_i: Q \to X_i$ to be the [[identity morphism]] $1_X: X \to X$, then the map

\begin{displaymath}
(f_i)_{i \in I} = (1_X)_{i \in I}: X \to X^I
\end{displaymath}
is called the \emph{[[diagonal morphism]]}, typically denoted by $\delta_X$ or $\Delta_X$. For example, we have a diagonal map

\begin{displaymath}
\delta_X: X \to X \times X
\end{displaymath}
for binary products.

\hypertarget{as_a_functor}{}\subsubsection*{{As a functor}}\label{as_a_functor}

If a [[category]] $C$ admits $I$-fold products (products over an indexing set $I$), then a product [[functor]]

\begin{displaymath}
\prod_I = \prod_{i \in I}: C^I \to C
\end{displaymath}
can be defined, taking a collection of [[objects]] $(c_i)_{i \in I}$ to their product, and taking a collection of [[morphisms]] $(f_i: c_i \to d_i)_{i \in I}$ to a morphism

\begin{displaymath}
\prod_{i \in I} f_i: \prod_{i \in I} c_i \to \prod_{i \in I} d_i
\end{displaymath}
defined to be $(f_i \circ p_i: \prod_{i \in I} c_i \to d_i)_{i \in I}$, using the notation above. (N.B.: the [[Cat|category of (small) categories]] has itself small products, and the notation $C^I$ makes reference to this fact. With some care, we can remove the restriction to [[small categories]].)

As a [[functor]], $\prod_I: C^I \to C$ is [[right adjoint]] to the diagonal functor $\Delta: C \to C^I$. The [[adjunction unit|unit of the adjunction]] $1_C \to \prod \Delta$, at the component $c \in Ob(C)$, is the [[diagonal morphism]]

\begin{displaymath}
\delta_c: c \to c^I
\end{displaymath}
and the [[counit]] $\Delta \prod \to 1_{C^I}$ is the $I$-tuple of projection maps:

\begin{displaymath}
p_i: \prod_{i \in I} c_i \to c_i
\end{displaymath}
Following the yoga of [[adjunctions]], we can write the ``tupling'' $(f_i)_{i \in I}: Q \to \prod_{i \in X_i}$ in terms of the product functor and the unit/diagonal map:

\begin{displaymath}
(f_i)_{i \in I} = \left(Q \stackrel{\delta_Q}{\to} \prod_{i \in I} Q \stackrel{\prod_{i \in I} f_i}{\to} \prod_{i \in I} X_i\right)
\end{displaymath}
while in the other direction, as stated in the [[universal property]] above, we can retrieve the components $f_i: Q \to X_i$ of a general map $f: Q \to \prod_{i \in I} X_i$ in terms of the diagonal functor and the counit/projection maps. It boils down to saying

\begin{displaymath}
f_i = \left(Q \stackrel{f}{\to} \prod_{i \in I} X_i \stackrel{p_i}{\to} X_i\right)
\end{displaymath}
\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

\hypertarget{products_of_sets}{}\subsubsection*{{Products of sets}}\label{products_of_sets}

Given [[sets]] $A$ and $B$, the cartesian product of the binary family $(A,B)$ is written $A \times B$; its elements $(a,b)$ are called \textbf{[[ordered pairs]]}. (In [[set theory]], one often makes a special definition for this case, defining

\begin{displaymath}
(a,b) = \{\{a\},\{a,b\}\}
\end{displaymath}
rather than as a function so that ordered pairs can then be used in the definition of function. From a structural perspective, however, this is unnecessary.)

Given sets $A_1$ through $A_n$, the cartesian product of the $n$-ary family $(A_1,\ldots,A_n)$ is written $\prod_{i=1}^n A_i$; its elements $(a_1,\ldots,a_n)$ are called \textbf{ordered $n$-[[tuples]]}.

Given sets $A_1$, $A_2$, etc, the cartesian product of the countably infinitary family $(A_1,A_2,\ldots)$ is written $\prod_{i=1}^\infty A_i$; its elements $(a_1,a_2,\ldots,)$ are called \textbf{infinite [[sequences]]}.

Given a set $A$, the cartesian product of the unary family $(A)$ may be identified with $A$ itself; that is, we identify the \textbf{ordered [[singleton]]} $(a)$ with $a$.

The cartesian product of the empty family $()$ is the [[point]], a set whose only element is the \textbf{[[empty list]]} $()$; we often call this set $1$ (or $\pt$, when we're Urs) and write its element as $*$.

\hypertarget{further_examples}{}\subsubsection*{{Further examples}}\label{further_examples}

\begin{itemize}%
\item In categories of [[algebras]], products are constructed in the ``obvious'' manner; see for example [[direct product group]].

\end{itemize}
For [[algebraic categories]] like [[Grp]], where the objects are sets equipped with (globally defined) specified operations that satisfy specified universally quantified identities, products are always constructed in the way you'd expect, viz. by taking products at the level of the underlying sets and endowing them with operations defined in the evident pointwise fashion, just like the way it works in $Grp$. More commentary on this in more general contexts will be given below.

\begin{itemize}%
\item For a non-example: the category of [[fields]] does not admit products, even though some might consider that an algebraic example (in some loose or informal sense).


\item In categories of topological type, products are again constructed in a common sense manner; see for instance [[product topological space]] for a prototype.



\end{itemize}
For [[topological categories]], which include examples like [[Top]] and [[Preord]], products (e.g. [[product topological spaces]]) are always constructed in the way one expects, by taking products at the level of the underlying sets and endowing them with an initial lift structure; e.g., in the case of $Top$, the smallest or initial topology for which the projection maps are continuous.

This principle continues to hold even for \emph{infinitary} products, where the correct structure might not be obvious without guidance from categorical considerations. For example, for topological spaces, for an infinite product $\prod_{i \in I} X_i$, we use the [[product topology]], and not say the [[box topology]] which might be the first thing one would try.

\begin{itemize}%
\item In any [[presheaf category]], i.e., a category of type $Set^C$ where $C$ is a [[small category]], products are calculated in obvious pointwise fashion, where $(F \times G)(c) = F(c) \times G(c)$ with the pointwise product projection maps. This even works if $C$ is [[large category|large]] (making $Set^C$ `very large').


\item If $D$ has products and $C \hookrightarrow D$ is a [[reflective subcategory]], products in $C$ exist and are calculated as they are in $D$. For example, this applies to any [[Grothendieck topos]], as a category of [[sheaves]] on a [[site]] forming a reflective subcategory of a category of presheaves (on the underlying category of the site).

\begin{itemize}%
\item For instance, the category [[Pos]] of [[posets]] is a reflective subcategory of [[Preord]].
\item Any [[locally presentable category]] can be exhibited as a reflective subcategory of a presheaf topos; as such we know how to calculate products there.

\end{itemize}

\item Generalizing the last example still further, if $U: A \to X$ is a [[monadic functor]], then products and more generally [[limits]] in $A$ are created (or [[reflected limit|reflected]]) from products/limits in $X$. In other words, products of algebras over a [[monad]] $T: X \to X$ are given by products in $X$, equipped with the evident ``pointwise'' $T$-algebra structure.


\item If $D$ has products and $i: C \hookrightarrow D$ is a \emph{[[coreflective subcategory|coreflective]]} subcategory, where $i$ has a right adjoint (co-reflector) $r$, then products in $C$ can be formed by taking products in $D$ and then applying $r$.

\begin{itemize}%
\item For example, the category $CG$ of [[compactly generated spaces]] is coreflective in [[Top]]. The product in $CG$ does not coincide in general with the topological product: one may have to add to the product topology still more sets, just enough to ensure that the topology is compactly generated.

\end{itemize}

\item Products in $C^{op}$ are given by [[coproducts]] in $C$.

\begin{itemize}%
\item In some cases, this formal tautology gives the only sensible way to construct products. For example, to form products $X \times Y$ in the category [[Loc]] of [[locales]], one must take the formal dual of the coproduct (denoted $\mathcal{O}(X) \otimes \mathcal{O}(Y)$) in the category of [[frames]].


\item Similarly, the product of two [[affine schemes]] is the formal dual of the coproduct of their corresponding coordinate rings, again given by a tensor product.



\end{itemize}

\item Relative to a [[symmetric monoidal category]] $C$ with monoidal product $\otimes$, products in the category of [[cocommutative comonoids]] are given by the tensor product $X \otimes Y$ in the underlying smc category.

\begin{itemize}%
\item For instance, this is how products of [[cocommutative coalgebras]] are formed. This applies for instance to cocommutative [[Hopf algebras]].
\item In a [[cartesian bicategory]] such as $Rel$, the accompanying category of objects and \emph{maps} (= left adjoint 1-cells) coincides with the category of cocommutative comonoids and comonoid maps between them (which is $Set$ in the case of $Rel$). Thus, at the level of objects, the usual tensor product in $Rel$ coincides with the cartesian product in $Set$.

\end{itemize}

\item For categories $C$ enriched in the category of [[commutative monoids]], [[finite products]] are [[biproducts]] and hence coincide with coproducts in a controlled fashion (via [[matrices]]). However, this is usually not the case for infinite products. For such examples, finite products are [[absolute limits]].


\item In the category [[SupLat]] of [[sup-lattices]], arbitrary products coincide with coproducts (and in fact the functor $X \mapsto X^{op}$ that takes a sup-lattice to its posetal opposite is part of a perfect duality $SupLat^{op} \to SupLat$, taking a sup-lattice map $f: X \to Y$ to $g^{op}: Y^{op} \to X^{op}$ where $f \dashv g$). This example descends to $Rel$ itself, so we conclude that products in $Rel$ are actually given by coproducts in $Rel$ which in turn are given by coproducts in $Set$.


\item [[product of simplices]]


\item In the [[Cat]] the cartesian product is the [[product of categories]].


\item If either [[projection]] out of a Cartesian product is regarded as a ([[fiber bundle|fiber]]) [[bundle]] map, it is called a \emph{[[trivial fiber bundle]]}.



\end{itemize}
\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

\hypertarget{relation_to_type_theory}{}\subsubsection*{{Relation to type theory}}\label{relation_to_type_theory}

Under the [[relation between category theory and type theory]] products in a category correspond to [[product types]] in [[type theory]].

[[!include product natural deduction - table]]

\hypertarget{foundational_status}{}\subsubsection*{{Foundational status}}\label{foundational_status}

In [[material set theory]], the existence of binary cartesian products follows from the [[axiom of pairing]] and the axiom of [[weak replacement]] (which is very weak). In [[structural set theory]], their existence generally must be stated as an axiom: the \textbf{axiom of products}. See [[ordered pair]] for more details.

\hypertarget{related_entries}{}\subsection*{{Related entries}}\label{related_entries}

\begin{itemize}%
\item [[cartesian monoidal category]]


\item [[finite product]]


\item [[tensor product]]


\item [[sum]]


\item [[external product]]


\item [[restricted product]]


\item [[product type]]


\item [[base change]]

\begin{itemize}%
\item [[dependent sum]], [[dependent product]]


\item [[dependent sum type]], [[dependent product type]]



\end{itemize}


\end{itemize}
category: foundational axiom

[[!redirects cartesian product]] [[!redirects cartesian products]] [[!redirects Cartesian product]] [[!redirects Cartesian products]] [[!redirects product set]] [[!redirects product sets]] [[!redirects product of sets]] [[!redirects products of sets]]

[[!redirects axiom of cartesian products]] [[!redirects axiom of Cartesian products]] [[!redirects axiom of products]]

[[!redirects product]] [[!redirects products]]



\end{document}