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