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.