module 1Lab.Counterexamples.Sigma where

# Σ is not ∃🔗

Defined normally, the *image* of a function
$f:X→Y$
is the subset of
$Y$
given by the elements
$y:Y$
for which *there exists* an element
$x:X$
with
$f(x)=y.$
In set theoretical notation:
$im(f)={y∈Y∣∃x∈X,f(x)=y}.$

It is a commonly held misunderstanding that when translating such a
definition into type theory, both subsets and existential quantifiers
should be read as specific cases of the dependent sum, `Σ`

- perhaps using “subset” to mean
“`Σ`

for which the type family is valued in propositions”. Indeed, the first
projection out of these is an embedding, so this
translation is accurate **for subsets**.

However, let’s see what happens when we naïvely translate the definition of image above:

private variable ℓ : Level A B : Type ℓ image : (A → B) → Type _ image {A = A} {B = B} f = Σ[ y ∈ B ] Σ[ x ∈ A ] (f x ≡ y)

The definition above, which could be called “Curry-Howard image”, does not accurately represent the image of a function: $image(f)≃A,$ independent of $f:$

image≃domain : {f : A → B} → image f ≃ A image≃domain {f = f} = Iso→Equiv the-iso where the-iso : Iso _ _ the-iso .fst (y , x , p) = x the-iso .snd .is-iso.inv x = f x , x , refl the-iso .snd .is-iso.rinv x = refl the-iso .snd .is-iso.linv (y , x , p) i = p i , x , λ j → p (i ∧ j)

This is a direct cubical interpretation of the following argument,
which goes through in any theory with J^{1}:

First, observe that we can reorder

`Σ[ y ∈ B ] Σ[ x ∈ A ] (f x ≡ y)`

into`Σ[ x ∈ A ] Σ[ y ∈ B ] (f x ≡ y)`

. By path induction, the type`Σ[ y ∈ B ] (f x ≡ y)`

is contractible (it is a singleton), leaving us with something isomorphic to`Σ[ x ∈ A ] *`

, which is evidently isomorphic to`A`

.

Hence we have, for example, that the “image” of the canonical
function `Bool → ⊤`

is isomorphic to `Bool`

:

ignore-bool : Bool → ⊤ ignore-bool _ = tt woops : image ignore-bool ≃ Bool woops = image≃domain

In fact, note that if we reorder

`p i, x, λ j → p (i ∧ j)`

we get`x, p i, λ j → p (i ∧ j)`

, which is exactly the proof term which establishes contractibility of singletons.↩︎