include "basics/logic.ma".
+(********** predicates *********)
+
+definition predicate: Type[0] → Type[0]
+≝ λA.A→Prop.
+
(********** relations **********)
definition relation : Type[0] → Type[0]
≝ λA.A→A→Prop.
+definition relation2 : Type[0] → Type[0] → Type[0]
+≝ λA,B.A→B→Prop.
+
definition reflexive: ∀A.∀R :relation A.Prop
≝ λA.λR.∀x:A.R x x.