Even-Odd algebras

GAT signature

nouGAT

⦃ E : U
, O : U
, z : E
, se : E ⇒ O
, so : O ⇒ E
⦄

oneGAT

⋄
▷ U
▷ U
▷ El 1
▷ Π 2 (El 2)
▷ Π 2 (El 4)

Algebras and Homomorphisms

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

• $E\colon\mathsf{Set}$
• $O\colon\mathsf{Set}$
• $z\colon E$
• $se\colon E \to O$
• $so\colon O \to E$

---

$\mathfrak{EO}\operatorname-\mathsf{Hom}\;(E_0,O_0,z_0,se_0,so_0)\;(E_1,O_1,z_1,se_1,so_1)\;:=$

• $E^M\colon E_0 \to E_1$
• $O^M\colon O_0 \to O_1$
• $E^M(z_0) = z_1$
• $(n \colon E_0) \to O^M (se_0\;n) = se_1 (E^M\; n)$
• $(n \colon O_0) \to E^M (so_0\;n) = so_1 (O^M\; n)$

Initial Algebra

• $\mathbb{E} := \overline{\mathsf{Tm}}\;\mathfrak{EO}\;(\mathsf{El}\;4)$
• $\mathbb{O} := \overline{\mathsf{Tm}}\;\mathfrak{EO}\;(\mathsf{El}\;3)$
• $zero := 2\colon \overline{\mathsf{Tm}}\;\mathfrak{EO}\;(\mathsf{El}\;4)$
• $succ_e := \lambda \mathbf{t}.(1 @ \mathbf{t}) \colon \overline{\mathsf{Tm}}\;\mathfrak{EO}\;(\mathsf{El}\;4) \to \overline{\mathsf{Tm}}\;\mathfrak{EO}\;(\mathsf{El}\;3)$
• $succ_o := \lambda \mathbf{t}.(0 @ \mathbf{t}) \colon \overline{\mathsf{Tm}}\;\mathfrak{EO}\;(\mathsf{El}\;3) \to \overline{\mathsf{Tm}}\;\mathfrak{EO}\;(\mathsf{El}\;4)$

Displayed Algebras and Sections

$\mathfrak{EO}\operatorname-\mathsf{DAlg}\;(E,O,z,se,so)\;:=$

• $E^D \colon E \to \mathsf{Set}$
• $O^D \colon O \to \mathsf{Set}$
• $E^D\;z$
• $(n \colon E) \to E^D\;n \to O^D(se\;n)$
• $(n \colon O) \to O^D\;n \to E^D(so\;n)$

---

$\mathfrak{EO}\operatorname-\mathsf{Sect}\;(E,O,z,se,so)\;(E^D,O^D,z^D,se^D,so^D)\;:=$

• $E^S \colon (n \colon E) \to E^D\;n$
• $O^S \colon (n \colon O) \to O^D\;n$
• $E^S\;z = z^D$
• $(n \colon E) \to se^D(E^S\;n) = O^S(se\;n)$
• $(n \colon O) \to so^D(O^S\;n) = E^S(so\;n)$