202507231607

Tags : Homotopy Type Theory

Cocones

---

Given a span $\mathcal{D}=A\stackrel{f}{\leftarrow }C\stackrel{g}{\to }B$ and a type $D$, a cocone under $\mathcal{D}$ with nadir $D$ consists of functions $i:A\to D$ and $j:B\to D$ and a homotopy $h:{\prod }_{c:C}(i(f(c))=j(g(c))):$

And we denote ${\text{cocone}}_{\mathcal{D}}(D)$ to be the type of all such cocones:

$${\text{cocone}}_{\mathcal{D}}(D):\equiv \sum _{(i:A\to D)}\sum _{(j:B\to D)}\prod _{(c:C)}i(f(c))=j(g(c))$$

---

References

• Cones and Cocones
• Identity Type