Martin Escardo 2011.

\begin{code}

{-# OPTIONS --without-K #-}

module Singleton where

open import SetsAndFunctions
open import CurryHoward
open import Equality

singleton : {X : Set} → X → Set
singleton {X} x = Σ \(x' : X) → x ≡ x'

singleton-incl : {X : Set} → (x : X) → singleton x
singleton-incl x = x , refl

singleton-map : {X Y : Set} →

(f : X → Y) → {x : X} → singleton x → singleton(f x)

singleton-map f (x , refl) = f x , refl

\end{code}

Paulin-Mohring's version of J.  See Dan Licata's blog post
http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/

\begin{code}

J' : {X : Set} → (x : X) → (C : singleton x → Prp) →

C(singleton-incl x) → ∀(s : singleton x) → C s

J' x c s (.x , refl) = s

singleton-has-only-one-element : {X : Set} →

∀(x : X) → ∀(s : singleton x) → s ≡ singleton-incl x

singleton-has-only-one-element x = J' x (λ s → s ≡ (singleton-incl x)) refl

singleton-has-only-one-element' : {X : Set} →

∀(x : X) → ∀(s t : singleton x) → s ≡ t

singleton-has-only-one-element' x s t =
trans
(singleton-has-only-one-element x s)
(sym(singleton-has-only-one-element x t))

\end{code}

It is interesting that this doesn't need UIP.