```-- 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)
```