demorgan.agda

-- empty type
data ⊥ : Set where

-- can't prove this so we introduce it as an axiom
postulate
    stab : ∀{A : Set} -> ((A -> ⊥) -> ⊥) -> A

-- if you give me an x of type X and an inhabitant of P x, then I have proof that there exists an inhabitant of P x
data ∃ {X : Set} (P : X -> Set) : Set where
    intro-∃ : ∀(x : X) -> P x -> ∃ P

-- lambda syntax
deMorgan4<-' : ∀{U : Set} {P : U -> Set} -> ((∀(x : U) -> P x) -> ⊥) -> ∃ (λ x -> P x -> ⊥)
deMorgan4<-' = λ f -> stab (λ h -> f (λ z -> stab (λ g -> h (intro-∃ z g))))

-- easier to figure out
deMorgan4<- : ∀{U : Set} {P : U -> Set} -> ((∀(x : U) -> P x) -> ⊥) -> ∃ (λ x -> P x -> ⊥)
deMorgan4<- {U} {P} f = stab x
    where x : (∃ (λ x → P x → ⊥) → ⊥) → ⊥
          x h = f y
            where y : ∀(x : U) -> P x
                  y z = stab u
                    where u : (P z -> ⊥) -> ⊥
                          u g = h (intro-∃ z g)