hm.agda

module scratch where

open import Data.Nat
open import Data.Product
open import Relation.Nullary

postulate Dom : Set

Formula : ℕ → Set₁
Formula zero    = Set
Formula (suc n) = Dom → Formula n

UI : ∀ {P : Formula 0} {Q : Formula 1} → (∀ a → P → Q a) → (P → ∀ a → Q a)
UI f p a = f a p

UE : ∀ {P : Formula 1} {t : Dom} → (∀ a → P a) → P t
UE {t = t} = λ x → x t

EI : ∀ {P : Formula 1} {t : Dom} → P t → ∃ λ a → P a
EI {t = t} = λ x → t , x

EE : ∀ {P : Formula 1} {Q : Formula 0} → (∀ a → P a → Q) → (∃ λ a → P a) → Q
EE f (a , p) = f a p

ex-7-49 : ∀ {φ : Formula 2} → (∀ ξ → ∀ ζ → φ ξ ζ) → (∀ ζ → ∀ ξ → φ ξ ζ)
ex-7-49 ∀ξ∀ζφ = λ ζ → λ ξ → UE {t = ζ} (UE {t = ξ} ∀ξ∀ζφ)

ex-7-50-1 : ∀ {P : Formula 1} → (¬ ¬ ∀ a → P a) → ∀ a → ¬ ¬ P a
ex-7-50-1 p = λ a → {!!}