Nat algebras

GAT signature

nouGAT

⦃ N : U
, z : N
, s : N ⇒ N
⦄

oneGAT

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

Algebras and Homomorphisms

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

• $N\colon\mathsf{Set}$
• $N$
• $N \to N$

---

$\mathfrak{N}\operatorname-\mathsf{Hom}\;(N_0,z_0,s_0)\;(N_1,z_1,s_1)\;:=$

• $N^M\colon N_0 \to N_1$
• $N^M(z_0) = z_1$
• $(n \colon N_0) \to N^M (s_0\;n) = s_1 (N^M\; n)$

Initial Algebra

• $\mathbb{N} := \overline{\mathsf{Tm}}\;\mathfrak{N}\;(\mathsf{El}\;2)$
• $zero := 1\colon \overline{\mathsf{Tm}}\;\mathfrak{N}\;(\mathsf{El}\;2)$
• $succ := \lambda \mathbf{t}.(0 @ \mathbf{t}) \colon \overline{\mathsf{Tm}}\;\mathfrak{N}\;(\mathsf{El}\;2) \to \overline{\mathsf{Tm}}\;\mathfrak{N}\;(\mathsf{El}\;2)$

Displayed Algebras and Sections

$\mathfrak{N}\operatorname-\mathsf{DAlg}\;(N,z,s)\;:=$

• $N^D \colon N \to \mathsf{Set}$
• $N^D\;z$
• $(n \colon N) \to N^D\;n \to N^D(s\;n)$

---

$\mathfrak{N}\operatorname-\mathsf{Sect}\;(N,z,s)\;(N^D,z^D,s^D)\;:=$

• $N^S \colon (n \colon N) \to N^D\;n$
• $N^S\;z = z^D$
• $(n \colon N) \to s^D(N^S\;n) = N^S(s\;n)$