-- Martin Escardo, 6th August 2015, 
-- modified 9 May to add the rewriting option only.

{- 
   We prove the axiom of description: for any set X and any
   p:X→Prop,
    
       (∃! p) = true → Σ(x:X).p(x)=true.
-}

{-# OPTIONS --without-K #-}
{-# OPTIONS --rewriting #-} -- Needed because prop.agda is now implemented using rewriting.

module description where

open import preliminaries
open import prop
open import proptrunc
open import logic 

-- First we need a Prop-valued equality to be able to define ∃!:

infix 34 _≡[_]_

_≡[_]_ : {X : U₀}  X  isSet X  X  Prop
x ≡[ s ] y =  x  y , s 

∃! : {X : U₀}  isSet X  (X  Prop)  Prop
∃! s p = (∃̇ p)  ∀̇ \x  ∀̇ \y  p x  p y  x ≡[ s ] y

description : (X : U₀) (s : isSet X) (p : X  Prop) 
             (∃! s p) holds  Σ \(x : X)  p x holds 
description X s p eu = ∥∥-rec h  x  x) e
 where
  P : X  U₀
  P x = p x holds
  e : (Σ \(x : X)  P x) 
  e = ∧-elim-L {∃̇ p} {∀̇ \x  ∀̇ \y  p x  p y  x ≡[ s ] y} eu 
  u : (x y : X)  P x  P y  x  y
  u = ∧-elim-R {∃̇ p} {∀̇ \x  ∀̇ \y  p x  p y  x ≡[ s ] y} eu
  h : isProp(Σ \(x : X)  P x)
  h (x , r) (y , s) = Σ-≡ (u x y r s) (holdsIsProp (p y) (transport P (u x y r s) r) s)

-- Perhaps the following formulation is more suggestive:

Description : (X : U₀) (s : isSet X) (p : X  Prop) 
             (∃! s p)  true  Σ \(x : X)  p x  true
Description X s p eu = (pr₁ d , holds→equal-true (pr₂ d))
 where
  d : Σ \(x : X)  (p x holds)
  d = description X s p (equal-true→holds eu)