Defining a type with a single value

Question

In here: http://www.cse.chalmers.se/~coquand/equality.pdf on slide 23 they define a very interesting type, iscontr A. I think it translates to:

record iscontr {A : Set} : Set where
  constructor _exists_unique
  field
    a : A
    singleton : (x : A) -> a == x

I don't see the subtle point they are making. They claim that at first it may seem that this is just a proof of A being inhabited with multiple, but (path) connected values - and this is exactly what I see here; but in fact, they claim, it is a proof of having a single inhabitant in type A.

Given that iscontr is introduced before even J is introduced (and is actually used to give an alternative definition of the induction axiom, J), this fact must be stemming from things other than induction.

Ok, at first I thought that to inhabit this type means to produce a function that can map any value of type A - including those that are not canonical (eg introduced by axioms) (remember, we can't do the usual pattern matching here, because we don't have the induction axiom yet). This would mean that somehow no new values can be added to A, even using axioms. This fact is a clear indication to me that we are pretty much bound to introduce an inhabitant of type iscontr through an axiom (which is what they do for type (x,α) on some following slide). But I don't see how this precludes existence of multiple values of type A, enumerated in the singleton function to produce a a == x for each.

(Also, I won't understand examples from toposes, groupoids, etc; so would be great to see an explanation through plain reasoning based on axioms introduced prior to slide 23)

Answer 1

Perhaps the best way to convince you that is-contr A really means that A has a single inhabitant is to show an equivalence between any contractible type and the unit type, as mentioned previously in the comments. For this, I'll need few definitions:

We already have contractibility, but let me use this pocket version instead:

is-contr : ∀ {a} (A : Set a) → Set _
is-contr A = Σ A λ a → ∀ x → a ≡ x

Next up: equivalence. I'm going to use the is-equiv version that is used throughout the HoTT book:

-- Homotopies.
infix  1 _~_

_~_ : ∀ {a b} {A : Set a} {B : A → Set b}
  (f g : ∀ a → B a) → Set _
f ~ g = ∀ x → f x ≡ g x

-- Equivalence.
is-equiv : ∀ {a b} {A : Set a} {B : Set b}
  (f : A → B) → Set _
is-equiv {A = A} {B = B} f
  = (Σ (B → A) λ g → f ∘ g ~ id)
  × (Σ (B → A) λ h → h ∘ f ~ id)

And finally:

_≃_ : ∀ {a b} (A : Set a) (B : Set b) → Set _
A ≃ B = Σ (A → B) is-equiv

So, a function f is an equivalence if it has both a left and a right inverse.

This should remind you the usual definition of equivalence (isomorphism) as a pair of functions f and g such that f ∘ g ~ id and g ∘ f ~ id, and indeed, it is logically equivalent to the definition above (see the comments to this answer for proof).

Anyways, we can now formulate the final statement:

contr-≃⊤ : ∀ {a} {A : Set a} → is-contr A → A ≃ ⊤

The proof is rather simple:

contr-≃⊤ : ∀ {a} {A : Set a} → is-contr A → A ≃ ⊤
contr-≃⊤ (a , p)
  = (λ _ → tt)
  , ((λ _ → a) , (λ _ → refl))
  , ((λ _ → a) , p)

So, our left and right inverse is just a constant function to the selected element (from is-contr A).

Connectedness, as defined in HoTT book (I hope the unicode characters show up for you)

is-conn : ∀ {a} (A : Set a) → Set _
is-conn A = Σ A λ a → ∀ x → ∥ a ≡ x ∥

cannot, in fact, be used to prove this equivalence. This can be best seen when you eta expand p in the contr-≃⊤ proof:

contr-≃⊤ (a , p)
  = (λ _ → tt)
  , ((λ _ → a) , (λ _ → refl))
  , ((λ _ → a) , (λ x → p x))

We need to know the actual path from a to x (i.e. p x : a ≡ x) to be able to prove this. However, ∥ a ≡ x ∥ is much weaker - it tells us only that such path exists but doesn't tell us what the path looks like.

---

This is also the reason why type theories have theorem of choice (instead of axiom). The constructive nature of existential quantification makes the proof trivial. If you, however, erase any information about actual inhabitants and leave only the fact, that one such exists, you get the usual axiom of choice. If you want, check out the chapters 3.7 and 3.8 in the HoTT book.