#lang racket
;; Starter code for A6Q5
;; May contain Unicode characters - download, don't cut/paste from browser
;; You must replace the ? with correct proof terms.

(provide not-exists-all-not answer1
         exists-not-not-all answer2
         not-pointwise-not-equal answer3)


(define not-exists-all-not
  '((∀ (X : Type) -> (∀ (P : (X -> Type)) ->
     ((¬ (∃ (x : X) (P x))) -> (∀ (x : X) -> (¬ (P x)))))) : Type))

(define answer1 '(? : not-exists-all-not))

(define exists-not-not-all
  '((∀ (X : Type) -> (∀ (P : (X -> Type)) ->
      ((∃ (x : X) (¬ (P x))) -> (¬ (∀ (x : X) -> (P x)))))) : Type))

(define answer2 '(? : exists-not-not-all))

(define not-pointwise-not-equal
  '(∀ (A : Type) (B : Type) (f : (A -> B)) (g : (A -> B)) ->
      ((∃ (x : A) (¬ ((f x) = (g x)))) -> (¬ (f = g)))))

(define answer3 '(? : not-pointwise-not-equal))