nkaretnikov · April 4, 2016 22:41 · adamse · Apr 4, 2016
diff --git a/and.agda b/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
 -}
	{-
	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
	-}