Library HFcoc

Require Import Setoid.
Require Export HFrelation.


Definition ext_fun dom F := eq_hf_fun dom F F.


Definition cc_lam (x:hf) (y:hf->hf) : hf :=
  union (repl x (fun x' => repl (y x') (fun y' => couple x' y'))).

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


Definition cc_app (x y:hf) : hf :=
  image (subset x (fun p => eq_hf (fst p) y)).

Instance cc_app_morph : morph2 cc_app.
Qed.


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


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

Lemma beta_morph : ∀ dom F,
  ext_fun (dep_func dom F)
    (fun f0 : hf => cc_lam dom (fun x' : hf => app f0 x')).
Hint Resolve beta_morph.

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

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

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


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

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

Lemma cc_impredicative_prod : ∀ dom F,
  eq_hf_fun dom F F ->
  (∀ x, x ∈ dom -> F x ∈ props) ->
  cc_prod dom F ∈ props.