Skip to main content

Pointed sets

GAT signature​

⦃ X : U
, x : X
⦄

Algebras and Homomorphisms​

P-⁡Alg  :=\mathfrak{P}\operatorname-\mathsf{Alg}\;:=

  • X ⁣:SetX\colon\mathsf{Set}
  • XX

P-⁡Hom  (X0,x0)  (X1,x1)  :=\mathfrak{P}\operatorname-\mathsf{Hom}\;(X_0,x_0)\;(X_1,x_1)\;:=

  • XM ⁣:X0→X1X^M\colon X_0 \to X_1
  • XM(x0)=x1X^M(x_0) = x_1

Initial Algebra​

  • P:=Tm‾  P  (El  1)\mathbb{P} := \overline{\mathsf{Tm}}\;\mathfrak{P}\;(\mathsf{El}\;1)
  • p:=0 ⁣:Tm‾  P  (El  1)p := 0\colon \overline{\mathsf{Tm}}\;\mathfrak{P}\;(\mathsf{El}\;1)

Displayed Algebras and Sections​

P-⁡DAlg  (X,x)  :=\mathfrak{P}\operatorname-\mathsf{DAlg}\;(X,x)\;:=

  • XD ⁣:X→SetX^D \colon X \to \mathsf{Set}
  • XD  xX^D\;x

P-⁡Sect  (X,x)  (XD,xD)  :=\mathfrak{P}\operatorname-\mathsf{Sect}\;(X,x)\;(X^D,x^D)\;:=

  • XS ⁣:(z ⁣:X)→XD  zX^S \colon (z \colon X) \to X^D\;z
  • XS  x=xDX^S\;x = x^D