2
module Logic.Base where
11
data False : Set where
13
elim-False : {A : Set} -> False -> A
16
data _/\_ (P Q : Set) : Set where
17
/\-I : P -> Q -> P /\ Q
19
data _\/_ (P Q : Set) : Set where
23
elimD-\/ : {P Q : Set}(C : P \/ Q -> Set) ->
24
((p : P) -> C (\/-IL p)) ->
25
((q : Q) -> C (\/-IR q)) ->
27
elimD-\/ C left right (\/-IL p) = left p
28
elimD-\/ C left right (\/-IR q) = right q
30
elim-\/ : {P Q R : Set} -> (P -> R) -> (Q -> R) -> P \/ Q -> R
31
elim-\/ = elimD-\/ (\_ -> _)
36
data ∃ {A : Set}(P : A -> Set) : Set where
37
∃-I : (w : A) -> P w -> ∃ P
39
∏ : {A : Set}(P : A -> Set) -> Set
40
∏ {A} P = (x : A) -> P x