module 1Lab.Counterexamples.Sigma where

Σ is not ∃🔗

Defined normally, the image of a function is the subset of given by the elements for which there exists an element with In set theoretical notation:

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: independent of

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

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

  1. 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.↩︎