Library ZFcoc

Require Import Setoid.
Require Export ZF ZFpairs ZFrelations.
Import IZF.



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

Lemma cc_lam_fun1 : forall x x',
  ext_fun x (fun y' => couple x' y').

Lemma cc_lam_fun2 : forall x y,
  ext_fun x y ->
  ext_fun x
    (fun x' => replf (y x') (fun y' => couple x' y')).
Hint Resolve cc_lam_fun1 cc_lam_fun2.

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

Lemma cc_impredicative_lam : forall dom F,
  ext_fun dom F ->
  (forall x, x \in 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 cc_beta_eq:
  forall dom F x,
  ext_fun dom F ->
  x \in dom ->
  cc_app (cc_lam dom F) x == 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_fun1 : forall A x,
  ext_fun A (fun f => cc_lam x (fun x' => app f x')).
Hint Resolve cc_prod_fun1.

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

Lemma cc_prod_intro : forall dom f F,
  ext_fun dom f ->
  ext_fun dom F ->
  (forall x, x \in dom -> f x \in F x) ->
  cc_lam dom f \in cc_prod dom F.

Lemma cc_prod_elim : forall dom f x F,
  f \in cc_prod dom F ->
  x \in dom ->
  cc_app f x \in F x.

Lemma cc_eta_eq: forall dom F f,
  f \in cc_prod dom F ->
  f == cc_lam dom (fun x => cc_app f x).

Lemma cc_prod_covariant : forall dom F G,
  ext_fun dom G ->
  (forall x, x \in dom -> F x \incl G x) ->
  cc_prod dom F \incl cc_prod dom G.


Definition prf_trm := empty.
Definition props := power (singl prf_trm).

Lemma cc_impredicative_prod : forall dom F,
  (forall x, x \in dom -> F x \in props) ->
  cc_prod dom F \in props.