Martin Escardo 2011.


{-# 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


Paulin-Mohring's version of J.  See Dan Licata's blog post


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 =
   (singleton-has-only-one-element x s)
   (sym(singleton-has-only-one-element x t))


It is interesting that this doesn't need UIP.