and.agda

and.agda

{-
Inductive and (P Q : Prop) : Prop :=
  conj : P -> Q -> (and P Q).
-}

data and {A : Set} {a : A} {P Q : A → Set} : P a → Q a → (A → Set) where
  conj : P a → Q a → and (P a) (Q a)
{-
Sets.agda:4,27-30
Set₁ != Set
when checking that the expression P a has type _P_10 _a_9
-}

data _∧_ {A : Set} : {P Q : A → Set} → {a : A} → P a → Q a → Set₁ where                                                                      
  conj : ∀ {a : A} {p} {q} → p a ∧ q a 

data and (P Q : Set) : Set where
  conj : P -> Q -> and P Q