Library ZFfunext

Require Export basic.
Require Import ZF ZFpairs ZFrelations ZFnats.

Definition fcompat dom f g :=
  ∀ x, x ∈ dom -> cc_app f x == cc_app g x.
Instance fext_morph :
  Proper (eq_set ==> eq_set ==> eq_set ==> iff) fcompat.
Qed.

Lemma fext_lam : ∀ A B f g,
    ext_fun A f ->
    ext_fun B g ->
    (∀ x, x ∈ A -> x ∈ B) ->
    (∀ x, x ∈ A -> f x == g x) ->
    fcompat A (cc_lam A f) (cc_lam B g).

Lemma fcompat_typ_eq : ∀ A f f',
  is_cc_fun A f ->
  is_cc_fun A f' ->
  fcompat A f f' ->
  f == f'.

Section ExtendFamily.

  Variable I : set.

  Variable A F : set -> set.
  Hypothesis extA : ext_fun I A.
  Hypothesis extF : ext_fun I F.

  Hypothesis in_prod : ∀ x, x ∈ I -> is_cc_fun (A x) (F x).

  Definition fdirected :=
    ∀ x y, x ∈ I -> y ∈ I -> fcompat (A x ∩ A y) (F x) (F y).

  Hypothesis fcomp : fdirected.

  Lemma fdir :
    ∀ x0 x1 x z,
    x0 ∈ I ->
    x1 ∈ I ->
    x ∈ A x0 ->
    z ∈ cc_app (F x1) x ->
    z ∈ cc_app (F x0) x.

Lemma prd_union : is_cc_fun (sup I A) (sup I F).

Lemma prd_sup : ∀ x,
  x ∈ I ->
  fcompat (A x) (F x) (sup I F).

Lemma prd_sup_lub : ∀ g,
  (∀ x, x ∈ I -> fcompat (A x) (F x) g) ->
  fcompat (sup I A) (sup I F) g.

End ExtendFamily.