open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.Counterexamples.Sigma where

Σ is not ∃🔗

Defined normally, the image of a function $f:X\to Y$ is the subset of $Y$ given by the elements $y:Y$ for which there exists an element $x:X$ with $f(x)=y\text{.}$ In set theoretical notation: $\mathrm{im}(f)=\{y\in Y|\exists x\in X,f(x)=y\}\text{.}$

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: $\mathrm{image}(f)\simeq A\text{,}$ independent of $f\text{:}$

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¹:

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