module ExMid where

open import Data.Empty
open import Data.Unit
open import Data.Bool hiding (_∧_; _∨_)
open import Data.Bool.Properties
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality as PropEq
open import Relation.Binary.HeterogeneousEquality using (_≅_; refl; ≡-to-≅)
import Relation.Binary.EqReasoning as EqR

-- axiom of choice, with a restriction on domain

{-
ac : {A B : Set} → (S : A → Set) → (R : A → B → Set) → 
       (∀ x → S x → ∃ (λ y → R x y)) → 
         (∃ {(x : A) → S x → B} (λ f → ∀ x → (d : S x) → R x (f x d)))
ac S R g = ((λ x d → proj₁ (g x d)) , λ x d → proj₂ (g x d)) -}


ac : {A B : Set} → (R : A → B → Set) → 
       (∀ x → ∃ (λ y → R x y)) → 
         (∃ {A → B} (λ f → ∀ x → R x (f x)))
ac R g = ((λ x → proj₁ (g x)) , λ x → proj₂ (g x))

-- we need a language of propositions that talks about equality

data † (A : Set) : Set where
   TT  : † A
   FF  : † A
   _≐_ : A → A → † A
   _≘_ : Bool → Bool → † A
   _∧_ : † A → † A → † A
   _⇒_ : † A → † A → † A
   _∨_ : † A → † A → † A
    
⌈_⌉ : ∀ {A} → † A → Set
⌈ TT ⌉ = ⊤
⌈ FF ⌉ = ⊥
⌈ a ≐ b ⌉ = a ≡ b
⌈ a ≘ b ⌉ = a ≡ b
⌈ P ∧ Q ⌉ = ⌈ P ⌉ × ⌈ Q ⌉
⌈ P ⇒ Q ⌉ = ⌈ P ⌉ → ⌈ Q ⌉
⌈ P ∨ Q ⌉ = ⌈ P ⌉ ⊎ ⌈ Q ⌉

￢ : ∀ {A} → † A → † A
￢ P = P ⇒ FF

_⇔_ : ∀ {A} → † A → † A → Set
P ⇔ Q = ⌈ (P ⇒ Q) ∧ (Q ⇒ P) ⌉

lemma : ∀ {A}{P Q R : † A} → ⌈ P ⌉ → (P ∨ Q) ⇔ (P ∨ R)
lemma p = ((λ _ → inj₁ p) , (λ _ → inj₁ p))

  -- proof irrelevance!

postulate irr : ∀ {A} (P Q : † A) → (p : ⌈ P ⌉)(q : ⌈ Q ⌉) → (P ≡ Q) → p ≅ q

-- extensional equality

postulate ext : {A B : Set} → (f g : A → † B) → (∀ a → f a ⇔ g a) → f ≡ g

--

ff≢tt : false ≢ true
ff≢tt = not-¬ refl

cong-× : ∀ {A B} {x y : Σ A B} → proj₁ x ≡ proj₁ y → proj₂ x ≅ proj₂ y → x ≡ y
cong-× {A}{B} {(x₁ , x₂)} {(.x₁ , .x₂)} refl refl = refl

--

U : ∀ {A} → † A → Bool → † A 
U X b = X ∨ (b ≘ false)

V : ∀ {A} → † A → Bool → † A
V X b = X ∨ (b ≘ true)

UorV : ∀ A → † A → Set
UorV A X = Σ (Bool → † A) (λ P → ⌈ (P ≐ U X) ∨ (P ≐ V X) ⌉)

Φ :  ∀ {A X} → (P : UorV A X) → Bool → Set
Φ P b = ⌈ proj₁ P b ⌉

Φ-total : ∀ {A X} → (P : UorV A X) → ∃ (λ b → Φ P b)
Φ-total (P , inj₁ P≡UX) = (false , subst (λ Q → ⌈ Q false ⌉) (sym P≡UX) (inj₂ refl))
Φ-total (P , inj₂ P≡VX) = (true , subst (λ Q → ⌈ Q true ⌉) (sym P≡VX) (inj₂ refl))

Φ-fun : ∀ {A X} → ∃ {UorV A X → Bool} (λ f → ∀ P → Φ P (f P))
Φ-fun = ac Φ Φ-total 

-- here it goes..

U' : ∀ {A} X → UorV A X
U' X = (U X , inj₁ refl)

V' : ∀ {A} X → UorV A X
V' X = (V X , inj₂ refl)

ex_mid : ∀ {A} → (X : † A) → ⌈ X ∨ (￢ X) ⌉
ex_mid {A} X with Φ-fun {X = X}
... | (f , f⊆Φ) with f⊆Φ (U' X) | f⊆Φ (V' X)
...   | inj₁ pX      | _ =  inj₁ pX
...   | _            | inj₁ pX = inj₁ pX
...   | inj₂ fU'≡ff  | inj₂ fV'≡tt = inj₂ negX
  where negX : ⌈ (￢ X) ⌉
        negX pX = let U≡V : U X ≡ V X
                      U≡V = let UXb⇔VXb : ∀ b → U X b ⇔ V X b
                                UXb⇔VXb b = lemma {_}{X}{b ≘ false}{b ≘ true} pX
                            in ext (U X) (V X) UXb⇔VXb

                      P≡Q : ((U X ≐ U X) ∨ (U X ≐ V X)) ≡ ((V X ≐ U X) ∨ (V X ≐ V X))
                      P≡Q = let open EqR (PropEq.setoid († (Bool → † A)))
                            in begin
                                  (U X ≐ U X) ∨ (U X ≐ V X)
                               ≈⟨ cong (λ x → (U X ≐ U X) ∨ (U X ≐ x)) (sym U≡V) ⟩ 
                                  (U X ≐ U X) ∨ (U X ≐ U X)
                               ≈⟨ cong (λ x → (x ≐ U X) ∨ (x ≐ x)) U≡V ⟩ 
                                  (V X ≐ U X) ∨ (V X ≐ V X)
                               ∎

                      U'≡V' : U' X ≡ V' X
                      U'≡V' = cong-× U≡V 
                                (irr ((U X ≐ U X) ∨ (U X ≐ V X)) ((V X ≐ U X) ∨ (V X ≐ V X))
                                   (proj₂ (U' X)) (proj₂ (V' X)) P≡Q)

                      fU'≡fV' : f (U' X) ≡ f (V' X)
                      fU'≡fV' = cong f U'≡V'

                  in let open EqR (PropEq.setoid Bool)
                  in ff≢tt (begin 
                     false     ≈⟨ sym fU'≡ff   ⟩
                     f (U' X)  ≈⟨ fU'≡fV' ⟩
                     f (V' X)  ≈⟨ fV'≡tt ⟩
                     true ∎)