202505131705

Sigma Types respect Universal Properties

Dependent Pair Types are a generalization of Product Type and also respect a genralized version of the universal property.

Given a type $X$ , a type families $A : X \to U$ and $P : \prod_{(x : X)} A (x) \to U$ . Then we have the function.

(x : X \prod a : A (x) \sum P (x, a)) \to (g : \prod_{(x : X)} A (x) \sum (x : X) \prod P (x, g (x)))

Not that if $P (x, a) :\equiv B (x)$ for some family $B : X \to U$ then this just becomes the case of product types and dependent functions.

The function is $f \to (pr_{1} \circ f, pr_{2} \circ f)$

Lemma

The above is a Equivalence

As before we define the quasi-inverse to send $(g, h)$ to $λ x . (g (x), h (x))$ so our round trip composite is again

\lambda x.(\text{pr}_{1}(f(x)), \text{pr}_{2}(f(x)))\

(pr_{1} (f (x)), pr_{2} (f (x))) = f (x)

And by function extensionality we get our answer. For the other direction we get the same judgemental equality.

This result is interesting because these functions in the “types as propositions” interpretation are precisely the Type Theoretic Axiom of Choice.

🏠 No Place Like ~