Set-theoretic semantics for sigma types

constructive-mathematicslogicproof-theorytype-theory

I'm trying to understand the set-theoretical semantics of sigma types. Suppose $\Gamma\vdash A : \text{type}$, $\Gamma.A\vdash B:\text{type}$, $\Gamma\vdash a:A$, $\Gamma\vdash b:B[1.a]$, $\Gamma\vdash p:\Sigma(A,B)$, $\Gamma\vdash \text{first}(p):A$, $\Gamma \vdash \text{second}(p):B[1.\text{first}(p)]$, $\Gamma\vdash \text{pair}(a,b):\Sigma(a,b)$.

By definition, $[\![\Sigma(A,B)]\!]=(S_\gamma)_{\gamma\in[\![{\Gamma}]\!]}$ where $S_\gamma=\{(x,y):x\in A_\gamma, y\in B_{(\gamma,x)}\}$; here $[\![A]\!]=(A_\gamma)_{\gamma\in [\![{\Gamma}]\!]}$ and $[\![{B}]\!]=(B_{(\gamma,x)})_{\gamma\in [\![{\Gamma}]\!], x\in A_\gamma}$.

I believe $[\![{\text{pair}(a,b)}]\!]: [\![{\Gamma}]\!]\to \amalg_{\gamma \in [\![{\Gamma}]\!]}\{(x,y):x\in A_\gamma, y\in B_{(\gamma,x)}\}$ can be defined by $\gamma\mapsto (\gamma,([\![{a}]\!](\gamma), [\![{b}]\!](\gamma)))$, where $[\![{a}]\!]:[\![{\Gamma}]\!]\to \amalg_{\gamma\in [\![{\Gamma}]\!]}A_\gamma$ is a map such that $[\![{a}]\!](\gamma)\in A_\gamma$ for every $\gamma\in [\![{\Gamma}]\!]$, and $[\![{b}]\!]:[\![{\Gamma}]\!]\to \amalg_{\gamma\in [\![{\Gamma}]\!]}B_{(\gamma,[\![{a}]\!](\gamma))}$ is a map such that $[\![{b}]\!](\gamma)\in B_{(\gamma,[\![{a}]\!](\gamma))}$ for every $\gamma\in [\![{\Gamma}]\!]$.

Next, I believe $[\![{\text{first}(p)}]\!]: [\![{\Gamma}]\!]\to \amalg_{\gamma\in [\![{\Gamma}]\!]}A_\gamma$ can be defined as $\gamma \mapsto (\gamma,\pi_1\pi_2[\![{p}]\!](\gamma))$ where $[\![{p}]\!]: [\![{\Gamma}]\!]\to \amalg_{\gamma\in [\![{\Gamma}]\!]}\{(\gamma,(x,y)):x\in A_\gamma, y\in B_{(\gamma,x)}\}$ and $\pi_1:R\times S\to R$ is the first projection while $\pi_2:R\times S\to S$ is the second projection.

I'm not sure about the definition of $[\![{\text{second}(p)}]\!]$. It should be a function $[\![{\Gamma}]\!]\to \amalg_{\gamma\in [\![{\Gamma}]\!]}B_{(\gamma,\pi_2\pi_1[\![{p}]\!](\gamma))}$. One natural way would be to define it as $\gamma\mapsto (\gamma,\pi_2\pi_2[\![{p}]\!](\gamma))$, but it's not clear whether $\pi_2\pi_2[\![{p}]\!](\gamma)$ lies in $B_{(\gamma,\pi_2\pi_1[\![{p}]\!](\gamma))}$; as far as I can tell, apriori it only lies in $B_{(\gamma,x)}$ for some $x\in A_\gamma$.

What's the right way to define $[\![{\text{second}(p)}]\!]$? And are my other definitions correct?

Best Answer

I think you're not being totally consistent in your treatment of things, and that might be making things more complicated than they need to be.

You start out talking about things like $(B(γ,x))_{γ \in [Γ], x \in A}$, which is an object of the $\mathsf{Fam}(\mathsf{Set})$ fibration. However, you proceed to talk about 'elements' in terms of $\coprod_{γ\in[Γ]}B_{\cdots}$, which is the total space of $B$, suggesting you have shifted to the codomain fibration, and are thinking about the image of $B$ under the equivalence between $\mathsf{Fam}(\mathsf{Set})$ and $\mathsf{Set}^→$. It's probably simpler to stay in just one of these fibrations. So, I'll stick with $\mathsf{Fam}(\mathsf{Set})$, since it more directly matches an expected, "set theoretic semantics."

The way this works is as follows:

  • The objects of $\mathsf{Fam}(\mathsf{Set})$ are pairs of a set $I$ and a family of sets $(F_i)_{i \in I}$
  • An arrow $f : (I,F) → (J,G)$ is a pair of a function $g : I → J$ and a family of functions $(h_{i} : F_i → G_{g(i)})_{i\in I}$
  • There's a functor $π_0 : \mathsf{Fam}(\mathsf{Set}) → \mathsf{Set}$ that throws away the family part
  • Most of the time we can work in a single fiber $\mathsf{Fam}(\mathsf{Set})_I$, whose objects always have $I$ as the index set, and where arrows always have $g = 1_I$. So, effectively, this is the category whose objects are families $(F_i)_{i \in I}$ and arrows are $(h_i : F_i → G_i)_{i \in I}$
  • The terminal object in each fiber is a family of singleton sets.
  • So categorical elements $(x : 1 → F_i)_{i \in I}$ correspond to a family of set theoretic elements $(x_i \in F_i)_{i \in I}$
  • Contexts $Γ$ are interpreted as sets $[Γ]$ of values
  • Types $Γ ⊢ A\ \mathsf{type}$ interpret to families $([\![A]\!]_γ)_{γ \in [Γ]}$
  • Context extension $Γ.A$ interprets to the disjoint union (see below) $\displaystyle \sum_{γ \in [Γ]}[\![A]\!]_γ$
  • Terms $Γ ⊢ a : A$ interpret to families of elements $([\![a]\!]_γ)_{γ \in [Γ]}$
  • Substitutions $Γ ⊢ Δ$ interpret to functions $[σ] : [Γ] → [Δ]$ and substituting transports between fibers, e.g. $(F_δ)_{δ\in [Δ]}$ to $(F_{σ(γ)})_{γ \in [Γ]}$

As you said, $$[\![Σ(A,B)]\!]_{γ\inΓ} = \{ (x, y) : x \in A_γ, y \in B_{(γ,x)} \}$$

For $\mathsf{pair}$, we are given $[\![a]\!]_γ \in A_γ$ and $[\![b]\!]_γ \in B_{γ,[\![a]\!]_γ}$, and need to provide $[\![\mathsf{pair}(a,b)]\!]_γ \in [\![Σ(A,B)]\!]_γ$, which is just:

$$[\![\mathsf{pair}(a,b)]\!]_γ = ([\![a]\!]_γ, [\![b]\!]_γ) \in \{ (x, y) : x \in A_γ, y \in B_{(γ,x)} \}$$

This corresponds to what you wrote via the equivalence above.

$\mathsf{first}(p)_γ$ is essentially what you wrote, except that $[\![Σ(A,B)]\!]_γ$ is not (generally) a set theoretic product. It is the disjoint union, often written $\displaystyle\sum_{x \in A_γ}B_{(γ,x)}$. Obviously this notation looks just like the type theoretic one, and probably inspired the latter. Anyhow, it still has $π_1$, and lets us define:

$$[\![\mathsf{first}(p)]\!]_γ = π_1([\![p]\!]_γ)$$

which should be equivalent to what you wrote without the extra coproduct stuff. Finally, as you might expect, we have:

$$[\![\mathsf{second}(p)]\!]_γ = π_2([\![p]\!]_γ)$$

The reason this works is that for $p \in \displaystyle \sum_{x\in A} B_x$, it is the case that $π_2(p) \in B_{π_1(p)}$. This is due to the definition of the set above.

$$(a,b) \in \{(x,y) : x \in A_γ, y \in B_{(γ,x)} \} ⇒ b \in B_{(γ,a)}$$

And this is what distinguishes it from the product.

Related Question