forall exists

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
record  : Set where
  constructor tt

-- ∀ is a dependent function
-- The result type can depend on the value of the argument.

-- ∃ is a dependent pair
-- The type of the second part can depend on the value of the first.
data Σ (A : Set) (P : A  Set) : Set where
  _,_ : (x : A) (w : P x)  Σ A P

-- A syntax with a bound variable.
syntax Σ A (λ x  P) = [ x  A ] P

uncurry : {A R : Set} {P : A  Set}
         ((x : A)  P x  R)
         ([ x  A ] (P x)  R)
uncurry f (x , w) = f x w

curry : {A R : Set} {P : A  Set}
       ([ x  A ] (P x)  R)
       ((x : A)  P x  R)
curry f x w = f (x , w)

possible : {A R : Set} {P : A  Set}
          ([ x  A ] (P x  R))
          ((x : A)  P x)  R
possible (x , f) g = f (g x)

impossible : {A R : Set} {P : A  Set}
            (((x : A)  P x)  R)
            ([ x  A ] (P x  R))
impossible f = ({!!} , {!!})
-- There's no way to fill in the first hole, because we don't know if
-- A is inhabited. But even if it were, we couldn't necessarily go
-- from a proof for a single inhabitant to a proof for all inhabitants.

possible' : {R : Set} {P :   Set}
           (((x : )  P x)  R)
           ([ x   ] (P x  R))
possible' f = (tt , λ pf  f (λ _  pf))
-- It works here, but only because ⊤ has (definitionally) a single inhabitant,
-- so a proof for an element of ⊤ is a proof for all elements of ⊤.