The Clowder Project

1. If $P_{1}=\mathsf{t}$, then $p^{1}_{1}=p^{1}_{2}=\text{id}_{\mathsf{t}}$, and there’s indeed a unique morphism from $P_{1}$ to $\mathsf{t}$ making the diagram commute, namely $\text{id}_{\mathsf{t}}$;
2. If $P_{1}=\mathsf{f}$, then $p^{1}_{1}=p^{1}_{2}$ are given by the unique morphism from $\mathsf{f}$ to $\mathsf{t}$, and there’s indeed a unique morphism from $P_{1}$ to $\mathsf{t}$ making the diagram commute, namely the unique morphism from $\mathsf{f}$ to $\mathsf{t}$;
3. If $P_{2}=\mathsf{t}$, then there is no morphism $p^{2}_{2}$.
4. If $P_{2}=\mathsf{f}$, then $p^{2}_{1}$ is the unique morphism from $\mathsf{f}$ to $\mathsf{t}$ while $p^{2}_{2}=\text{id}_{\mathsf{f}}$, and there’s indeed a unique morphism from $P_{2}$ to $\mathsf{f}$ making the diagram commute, namely $\text{id}_{\mathsf{f}}$;
5. The proof for $P_{3}$ is similar to the one for $P_{2}$;
6. If $P_{4}=\mathsf{t}$, then there is no morphism $p^{4}_{1}$ or $p^{4}_{2}$.
7. If $P_{4}=\mathsf{f}$, then $p^{4}_{1}=p^{4}_{2}=\text{id}_{\mathsf{f}}$, and there’s indeed a unique morphism from $P_{4}$ to $\mathsf{f}$ making the diagram commute, namely $\text{id}_{\mathsf{f}}$.

natural in $A,B,C\in \{ \mathsf{t},\mathsf{f}\} $. Indeed:

• For $\webleft (A,B,C\webright )=\webleft (\mathsf{t},\mathsf{t},\mathsf{t}\webright )$, we have
  \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{t},\mathsf{t}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright )\\ & = \webleft\{ \text{id}_{\mathsf{true}}\webright\} \\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright )\webright ). \end{align*}

• For $\webleft (A,B,C\webright )=\webleft (\mathsf{t},\mathsf{t},\mathsf{f}\webright )$, we have
  \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{t},\mathsf{f}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright )\\ & = \text{Ø}\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright )\webright ). \end{align*}

• For $\webleft (A,B,C\webright )=\webleft (\mathsf{t},\mathsf{f},\mathsf{t}\webright )$, we have
  \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{f},\mathsf{t}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \text{pt}\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\webright ). \end{align*}

• For $\webleft (A,B,C\webright )=\webleft (\mathsf{t},\mathsf{f},\mathsf{f}\webright )$, we have
  \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{f},\mathsf{f}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \webleft\{ \text{id}_{\mathsf{false}}\webright\} \\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\webright ). \end{align*}

• For $\webleft (A,B,C\webright )=\webleft (\mathsf{f},\mathsf{t},\mathsf{t}\webright )$, we have
  \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{t},\mathsf{t}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \text{pt}\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright )\webright ). \end{align*}

• For $\webleft (A,B,C\webright )=\webleft (\mathsf{f},\mathsf{t},\mathsf{f}\webright )$, we have
  \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{t},\mathsf{f}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \webleft\{ \text{id}_{\mathsf{false}}\webright\} \\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright )\webright ). \end{align*}

• For $\webleft (A,B,C\webright )=\webleft (\mathsf{f},\mathsf{f},\mathsf{t}\webright )$, we have
  \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{f},\mathsf{t}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \text{pt}\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\webright ). \end{align*}

• For $\webleft (A,B,C\webright )=\webleft (\mathsf{f},\mathsf{f},\mathsf{f}\webright )$, we have
  \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{f},\mathsf{f}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & = \webleft\{ \text{id}_{\mathsf{false}}\webright\} \\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\webright ). \end{align*}