include "basics/logic.ma".
+(********** preducates *********)
+
+definition predicate: Type[0] → Type[0]
+≝ λA.A→Prop.
+
(********** relations **********)
definition relation : Type[0] → Type[0]
≝ λA.A→A→Prop.
lemma injective_compose : ∀A,B,C,f,g.
injective A B f → injective B C g → injective A C (λx.g (f x)).
-/3/; qed.
+/3/; qed-.
(* extensional equality *)
+(* moved inside sets.ma
definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
-λA.λP,Q.∀a.iff (P a) (Q a).
+λA.λP,Q.∀a.iff (P a) (Q a). *)
definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
λA,B.λR,S.∀a.∀b.iff (R a b) (S a b).
definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
λA,B.λf,g.∀a.f a = g a.
+(*
notation " x \eqP y " non associative with precedence 45
for @{'eqP A $x $y}.
interpretation "functional extentional equality"
-'eqP A x y = (exteqP A x y).
+'eqP A x y = (exteqP A x y). *)
notation "x \eqR y" non associative with precedence 45
for @{'eqR ? ? x y}.