module LogicQuestions where data _∧_ (A B : Set) : Set where _,_ : A → B → A ∧ B fst : {A B : Set} → A ∧ B → A fst (a , b) = a snd : {A B : Set} → A ∧ B → B snd (a , b) = b data _∨_ (A B : Set) : Set where left : A → A ∨ B right : B → A ∨ B ∨elim : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C ∨elim f g (left a) = f a ∨elim f g (right b) = g b data ⊥ : Set where ¬_ : Set → Set ¬ A = A → ⊥ magic : {A : Set} → ⊥ → A magic () dneg : {A : Set} → A → ¬ ¬ A dneg a = λ x → x a lem1 : {A B : Set} → A ∧ B → ¬ (¬ A ∨ ¬ B) lem1 = {!!} lem2 : {A B : Set} → A ∨ B → ¬ (¬ A ∧ ¬ B) lem2 = {!!} lem3 : {A B : Set} → A ∧ B → ¬ (A → ¬ B) lem3 = {!!} lem4 : {A B : Set} → (A → B) → ¬ (A ∧ ¬ B) lem4 = {!!} lem5 : {A B : Set} → A ∨ B → (¬ A → B) lem5 = {!!} data ∃ (A : Set)(B : A → Set) : Set where sig : (a : A) → B a → ∃ A B fst' : ∀{A B} → ∃ A B → A fst' (sig a b) = a snd' : ∀{A B}(p : ∃ A B) → B (fst' p) snd' (sig a b) = b lem6 : {A : Set}{B : A → Set} → ((x : A) → B x) → ¬ (∃ A λ a → ¬ (B a)) lem6 = {!!} lem7 : {A : Set}{B : A → Set} → (∃ A λ a → B a) → ¬ ((x : A) → ¬ (B x)) lem7 = {!!} AC : {A B : Set}{C : A → B → Set} → ((x : A) → ∃ B λ y → C x y) → ∃ (A → B) λ f → (x : A) → C x (f x) AC = {!!}