Added a rule for what eta looks like at the coproduct, just in terms …

…of the diagram not with any proof term artifacts.

notes_week3.tex

@@ -150,7 +150,16 @@ \subsection{Coproduct}
 {} & C & {}
 \end{tikzcd}
 \]
-where given a map $M:A+B\to C$ such that $M\circ \inl \equiv P$ and $M\circ \inr \equiv Q$, the map is in fact equivalent to $M\equiv \{P,Q\}$, so the $\eta$ rule makes the center cell commute.
+where given a map $M:A+B\to C$ such that $M\circ \inl \equiv P$ and $M\circ
+\inr \equiv Q$, the map is in fact equivalent to $M\equiv \{P,Q\}$, so the
+$\eta$ rule makes the center cell commute. In other words,
+\[
+\infer[\eta+]
+      {M=\{P,Q\} : A+B \to C}
+      {M : A + B \to C & M \circ \inl = P : A \to C & M \circ \inr = Q : B \to C}
+\]
+
+
 
 Just as we have done for $\eta{\wedge}$, we can rewrite the $\eta{\vee}$ rule by explicitly naming $P:Q\to C$ and $Q:B\to C$ as follows
 \[