Skip to content

Instantly share code, notes, and snippets.

@krtx
Last active May 30, 2018 18:10
Show Gist options
  • Save krtx/6ca821713c2c7bf3d5acade21f442402 to your computer and use it in GitHub Desktop.
Save krtx/6ca821713c2c7bf3d5acade21f442402 to your computer and use it in GitHub Desktop.
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 → {!!}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment