202505071605

Tags : Homotopy Type Theory

Higher Groupoids Structure of Coproducts

---

Consider the type $A+B$ which is ‘presented’ by the injections $\text{inl}:A\to A+B$ and $\text{inr}:B\to A+B$, since we expect the sum type to have copies of $A$ and $B$ we would like the following:

$$\begin{array}{rl}(\text{inl}(a)=\text{inl}(a^{\prime }))& \simeq (a=a^{\prime })\\ (\text{inr}(b)=\text{inr}(b^{\prime }))& \simeq (b=b^{\prime })\\ (\text{inr}(a)=\text{inl}(b))& \simeq 0\end{array}$$

To prove this, we fix an element $a_0:A$ and look at the type family:

$$(x\mapsto (\text{inl}(a_0)=x)):A+B\to \mathcal{U}$$

And a similar argument would characterize the type family $(x\mapsto (\text{inr}(b_0)=x))$.

To make the analysis easier, we shall first define the type family $\text{code}:A+B\to \mathcal{U}$ as follows:

$$\begin{array}{rl}\text{code}(\text{inl}(a))& :\equiv (a_0=a)\\ \text{code}(\text{inr}(b))& :\equiv 0\end{array}$$

This will make proving statements about the above easier and it has the following property:

$$\prod _{(x:A+B)}(\text{inl}(a_0)=x)\simeq \text{code}(x)$$

To prove so we first define

$$\text{encode}:\prod _{(x:A+B)}\prod _{(p:\text{inl}(a_0)=x)}\text{code}(x)$$

that is simple, we can think of $\text{code}$ as a non-dependent function to the universe and get

$$\text{encode}(x,p):\equiv {\text{transport}}^{\text{code}}(p,{\text{refl}}_{a_0})$$

Now we define

$$\text{decode}:\prod _{x:A+B}\prod _{c:\text{code}(x)}\text{inl}(a_0)=x$$

To define this, we use the elimination rule of $A+B$ and divide it into cases:

• Case 1: $x=\text{inl}(a)$, this means $\text{code}(x)=(a_0=a)$ so we can simply apply ${\text{ap}}_{\text{inl}}(c)$ and get the answer.
• In the second case, since $c$ is the empty type, its elimination rule gives us the element.

We now show that $\text{encode}(x,-)$ and $\text{decode}(x,-)$ are quasi inverses for all $x$, I will write them as ${\text{encode}}_x$ becuase I like this notion better.

$$\begin{array}{rl}{\text{decode}}_x({\text{encode}}_x(p))& \equiv {\text{decode}}_{\text{inl}(a_0)}({\text{encode}}_{\text{inl}(a_0)}({\text{refl}}_{\text{inl}(a_0)}))\\ & \equiv {\text{decode}}_{\text{inl}(a_0)}({\text{transport}}^{\text{code}}({\text{refl}}_{\text{inl}(a_0)},{\text{relf}}_{a_0}))\\ & \equiv {\text{decode}}_{\text{inl}(a_0)}({\text{refl}}_{a_0})\\ & \equiv {\text{ap}}_{\text{inl}}({\text{refl}}_{a_0})\equiv {\text{refl}}_{\text{inl}(a_0)}\equiv p\end{array}$$

Now for the other direction, we again divided based on cases, when $x=\text{inl}(a)$ and $\text{inr}(b)$, for the first case we hae $c:a_0=a$

$$\begin{array}{rl}{\text{encode}}_{\text{inl}(a_0)}({\text{decode}}_{\text{inl}(a_0)}(c))& \equiv {\text{encode}}_{\text{inl}(a_0)}({\text{ap}}_{\text{inl}}(c))\\ & \equiv {\text{transport}}^{\text{code}}({\text{ap}}_{\text{inl}}(c),{\text{refl}}_{a_0})\\ & \equiv {\text{transport}}^{a\mapsto a_0=a}(c,{\text{refl}}_{a_0})\\ & \equiv {\text{refl}}_{a_0}\cdot c\equiv c\end{array}$$

And for the other case we can have whatever we want.

Transports can be defined in a fairly straightforward way:

$$\begin{array}{r}{\text{transport}}^{A+B}(p,\text{inl}(a)):\equiv \text{inl}({\text{transport}}^A(p,a))\\ {\text{transport}}^{A+B}(p,\text{inr}(b)):\equiv \text{inr}({\text{transport}}^B(p,b))\end{array}$$

where the type family $A+B$ is defined from type families $A,B:X\to \mathcal{U}$ as $(A+B)(x)=A(x)+B(x)$.

---

References

• Sum Types
• Transport
• Functions as Equivalences