Bipointed sets

GAT signature

nouGAT

⦃ X : U
, x : X
, y : X
⦄

oneGAT

⋄
▷ U
▷ El 0
▷ El 1

Algebras and Homomorphisms

$\mathfrak{B}\operatorname-\mathsf{Alg}\;:=$

• $X\colon\mathsf{Set}$
• $x\colon X$
• $y\colon X$

---

$\mathfrak{B}\operatorname-\mathsf{Hom}\;(X_0,x_0,y_0)\;(X_1,x_1,y_1)\;:=$

• $X^M\colon X_0 \to X_1$
• $X^M(x_0) = x_1$
• $X^M(y_0) = y_1$

Initial Algebra

• $\mathbb{B} := \overline{\mathsf{Tm}}\;\mathfrak{B}\;(\mathsf{El}\;2)$
• $p := 1\colon \overline{\mathsf{Tm}}\;\mathfrak{B}\;(\mathsf{El}\;2)$
• $q := 0\colon \overline{\mathsf{Tm}}\;\mathfrak{B}\;(\mathsf{El}\;2)$

Displayed Algebras and Sections

$\mathfrak{B}\operatorname-\mathsf{DAlg}\;(X,x,y)\;:=$

• $X^D \colon X \to \mathsf{Set}$
• $X^D\;x$
• $X^D\;y$

---

$\mathfrak{B}\operatorname-\mathsf{Sect}\;(X,x,y)\;(X^D,x^D,y^D)\;:=$

• $X^S \colon (z \colon X) \to X^D\;z$
• $X^S\;x = x^D$
• $X^S\;y = y^D$