Require Import ZFpairs.

Definition is_relation x :=
  ∀ p, p ∈ x -> p == couple (fst p) (snd p).

Definition rel_app r x y := couple x y ∈ r.

Instance rel_app_morph :
  Proper (eq_set ==> eq_set ==> eq_set ==> iff) rel_app.
Qed.

Definition rel_domain r :=
  subset (union (union r)) (fun x => exists y, rel_app r x y).

Definition rel_image r :=
  subset (union (union r)) (fun y => exists x, rel_app r x y).

Instance rel_image_morph : morph1 rel_image.


Qed.

Lemma rel_image_ex : ∀ r x, x ∈ rel_domain r -> exists y, rel_app r x y.

Lemma rel_domain_intro : ∀ r x y, rel_app r x y -> x ∈ rel_domain r.

Lemma rel_image_intro : ∀ r x y, rel_app r x y -> y ∈ rel_image r.

Definition rel_comp f g :=
  subset (prodcart (rel_domain g) (rel_image f))
    (fun p => exists2 y, rel_app g (fst p) y & rel_app f y (snd p)).

Lemma rel_comp_intro : ∀ f g x y z,
  rel_app g x y -> rel_app f y z -> rel_app (rel_comp f g) x z.

Definition rel A B := power (prodcart A B).

Lemma rel_mono :
  Proper (incl_set ==> incl_set ==> incl_set) rel.

Instance rel_morph : morph2 rel.

Lemma app_typ1 : ∀ r x y A B, r ∈ rel A B -> rel_app r x y -> x ∈ A.

Lemma app_typ2 : ∀ r x y A B, r ∈ rel A B -> rel_app r x y -> y ∈ B.

Lemma rel_is_relation : ∀ f A B, f ∈ rel A B -> is_relation f.

Lemma rel_domain_incl : ∀ r A B, r ∈ rel A B -> rel_domain r ⊆ A.

Lemma rel_image_incl : ∀ r A B, r ∈ rel A B -> rel_image r ⊆ B.

Lemma relation_is_rel :
  ∀ r A B,
  is_relation r ->
  rel_domain r ⊆ A ->
  rel_image r ⊆ B ->
  r ∈ rel A B.

Definition inject_rel R A B :=
  subset (prodcart A B) (fun p => R (fst p) (snd p)).

Lemma inject_rel_is_rel : ∀ (R:set->set->Prop) A B,
  inject_rel R A B ∈ rel A B.

Lemma inject_rel_intro :
  ∀ (R:set->set->Prop) A B x y,
  ext_rel A R ->
  x ∈ A ->
  y ∈ B ->
  R x y ->
  rel_app (inject_rel R A B) x y.

Lemma inject_rel_elim :
  ∀ (R:set->set->Prop) A B x y,
  ext_rel A R ->
  rel_app (inject_rel R A B) x y ->
  x ∈ A /\ y ∈ B /\ R x y.

Definition is_function f :=
  is_relation f /\
  ∀ x y y', rel_app f x y -> rel_app f x y' -> y == y'.

Definition app f x :=
  union (subset (rel_image f) (fun y => rel_app f x y)).

Instance app_morph : morph2 app.

Lemma app_defined : ∀ f x y,
  is_function f -> rel_app f x y -> app f x == y.

Lemma app_elim : ∀ f x,
  is_function f -> x ∈ rel_domain f -> rel_app f x (app f x).

Definition func A B :=
  subset (rel A B)
    (fun r =>
       (∀ x, x ∈ A -> exists2 y, y ∈ B & rel_app r x y) /\
       (∀ x y y', rel_app r x y -> rel_app r x y' -> y == y')).

Instance func_mono :
  Proper (eq_set ==> incl_set ==> incl_set) func.


Qed.

Instance func_morph : morph2 func.

Lemma func_rel_incl : ∀ A B, func A B ⊆ rel A B.

Lemma func_is_function : ∀ f A B, f ∈ func A B -> is_function f.

Lemma fun_domain_func : ∀ f A B, f ∈ func A B -> rel_domain f == A.

Lemma app_typ :
  ∀ f x A B, f ∈ func A B -> x ∈ A -> app f x ∈ B.

Lemma func_narrow : ∀ f A B B',
  f ∈ func A B ->
  (∀ x, x ∈ A -> app f x ∈ B') ->
  f ∈ func A B'.

Definition lam_rel (F:set->set) A B := inject_rel (fun x y => F x == y) A B.

Lemma lam_rel_is_func : ∀ A B f,
  ext_fun A f ->
  (∀ x, x ∈ A -> f x ∈ B) ->
  lam_rel f A B ∈ func A B.

Lemma beta_rel_eq : ∀ f x A B,
  ext_fun A f ->
  x ∈ A -> (∀ x, x ∈ A -> f x ∈ B) -> app (lam_rel f A B) x == f x.

Definition lam A F := replf A (fun x => couple x (F x)).

Lemma fun_elt_is_ext : ∀ A f,
  ext_fun A f ->
  ext_fun A (fun x => couple x (f x)).
Hint Resolve fun_elt_is_ext.

Lemma lam_is_function : ∀ A f, ext_fun A f -> is_function (lam A f).

Lemma lam_is_func : ∀ A B f,
  ext_fun A f ->
  (∀ x, x ∈ A -> f x ∈ B) ->
  lam A f ∈ func A B.

Lemma beta_eq : ∀ f x A,
  ext_fun A f -> x ∈ A -> app (lam A f) x == f x.

Definition dep_image (A:set) (B:set->set) := replf A B.

Lemma dep_image_ext :
  ∀ x1 x2 f1 f2,
  x1 == x2 ->
  eq_fun x1 f1 f2 ->
  dep_image x1 f1 == dep_image x2 f2.

Definition dep_func (A:set) (B:set->set) :=
  subset (func A (union (dep_image A B)))
    (fun f => ∀ x, x ∈ A -> app f x ∈ B x).

Lemma dep_func_ext :
  ∀ x1 x2 f1 f2,
  x1 == x2 ->
  eq_fun x1 f1 f2 ->
  dep_func x1 f1 == dep_func x2 f2.

Lemma dep_func_mono : ∀ A A' F F',
  ext_fun A F ->
  ext_fun A' F' ->
  A == A' ->
  (∀ x, x ∈ A -> F x ⊆ F' x) ->
  dep_func A F ⊆ dep_func A' F'.

Lemma dep_func_intro : ∀ f dom F,
  ext_fun dom f ->
  ext_fun dom F ->
  (∀ x, x ∈ dom -> f x ∈ F x) ->
  lam dom f ∈ dep_func dom F.

Lemma func_eta : ∀ f A B,
  f ∈ func A B ->
  f == lam A (fun x => app f x).

Lemma dep_func_eta : ∀ f dom F,
  f ∈ dep_func dom F ->
  f == lam dom (fun x => app f x).

Lemma dep_func_incl_func : ∀ A B,
  dep_func A B ⊆ func A (union (dep_image A B)).

Lemma dep_func_elim :
  ∀ f x A B, f ∈ dep_func A B -> x ∈ A -> app f x ∈ B x.

Definition is_cc_fun A f :=
  ∀ c, c ∈ f -> c == couple (fst c) (snd c) /\ fst c ∈ A.

Instance is_cc_fun_morph : Proper (eq_set ==> eq_set ==> iff) is_cc_fun.
Qed.

Definition cc_lam (x:set) (y:set->set) : set :=
  sup x (fun x' => replf (y x') (fun y' => couple x' y')).

Instance cc_lam_morph : Proper (eq_set ==> (eq_set ==> eq_set) ==> eq_set) cc_lam.

Qed.

Lemma cc_lam_def dom f z :
  ext_fun dom f ->
  (z ∈ cc_lam dom f <->
   exists2 x, x ∈ dom & exists2 y, y ∈ f x & z == couple x y).

Lemma is_cc_fun_lam A F :
  ext_fun A F ->
  is_cc_fun A (cc_lam A F).

Lemma cc_lam_ext :
  ∀ x1 x2 f1 f2,
  x1 == x2 ->
  eq_fun x1 f1 f2 ->
  cc_lam x1 f1 == cc_lam x2 f2.

Lemma cc_impredicative_lam : ∀ dom F,
  ext_fun dom F ->
  (∀ x, x ∈ dom -> F x == empty) ->
  cc_lam dom F == empty.

Definition cc_app (x y:set) : set :=
  rel_image (subset x (fun p => fst p == y)).

Instance cc_app_morph : morph2 cc_app.
Qed.

Lemma couple_in_app : ∀ x z f,
  couple x z ∈ f <-> z ∈ cc_app f x.

Lemma cc_app_empty : ∀ x, cc_app empty x == empty.

Lemma cc_beta_eq : ∀ dom F x,
  ext_fun dom F ->
  x ∈ dom ->
  cc_app (cc_lam dom F) x == F x.

Lemma cc_eta_eq' : ∀ dom f,
  is_cc_fun dom f ->
  f == cc_lam dom (fun x => cc_app f x).

Definition cc_prod (x:set) (y:set->set) : set :=
  replf (dep_func x y)
    (fun f => cc_lam x (fun x' => app f x')).

Lemma cc_prod_ext :
  ∀ x1 x2 f1 f2,
  x1 == x2 ->
  eq_fun x1 f1 f2 ->
  cc_prod x1 f1 == cc_prod x2 f2.

Instance cc_prod_morph : Proper (eq_set ==> (eq_set ==> eq_set) ==> eq_set) cc_prod.
Qed.

Lemma cc_prod_fun1 : ∀ A x,
  ext_fun A (fun f => cc_lam x (fun x' => app f x')).
Hint Resolve cc_prod_fun1.

Lemma cc_prod_is_cc_fun : ∀ A B f,
  f ∈ cc_prod A B -> is_cc_fun A f.
Hint Resolve cc_prod_is_cc_fun.

Definition cc_arr A B := cc_prod A (fun _ => B).

Instance cc_arr_morph : morph2 cc_arr.
Qed.

Lemma cc_prod_intro : ∀ dom f F,
  ext_fun dom f ->
  ext_fun dom F ->
  (∀ x, x ∈ dom -> f x ∈ F x) ->
  cc_lam dom f ∈ cc_prod dom F.

Lemma cc_prod_elim : ∀ dom f x F,
  f ∈ cc_prod dom F ->
  x ∈ dom ->
  cc_app f x ∈ F x.

Lemma cc_app_typ f v A B B' :
  f ∈ cc_prod A B ->
  B' == B v ->
  v ∈ A ->
  cc_app f v ∈ B'.

Lemma cc_arr_intro : ∀ A B F,
  ext_fun A F ->
  (∀ x, x ∈ A -> F x ∈ B) ->
  cc_lam A F ∈ cc_arr A B.

Lemma cc_arr_elim : ∀ f x A B,
  f ∈ cc_arr A B ->
  x ∈ A ->
  cc_app f x ∈ B.

Lemma cc_eta_eq: ∀ dom F f,
  f ∈ cc_prod dom F ->
  f == cc_lam dom (fun x => cc_app f x).

Lemma cc_prod_covariant : ∀ dom dom' F G,
  ext_fun dom' G ->
  dom == dom' ->
  (∀ x, x ∈ dom -> F x ⊆ G x) ->
  cc_prod dom F ⊆ cc_prod dom' G.

Lemma cc_prod_intro' : ∀ (dom dom': set) (f F : set -> set),
       ext_fun dom f ->
       ext_fun dom' F ->
       dom == dom' ->
       (∀ x : set, x ∈ dom -> f x ∈ F x) ->
       cc_lam dom f ∈ cc_prod dom' F.