Library ZFcoc

Require Export basic ZF ZFpairs ZFrelations ZFstable.
Require Import ZFgrothendieck.

Impredicativity of props

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

Lemma props_proof_irrelevance x P :
  P ∈ props -> x ∈ P -> x == empty.

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

Lemma cc_impredicative_arr : ∀ A B,
  B ∈ props ->
  cc_arr A B ∈ props.

Lemma cc_forall_intro A B :
  ext_fun A B ->
  (∀ x, x ∈ A -> empty ∈ B x) ->
  empty ∈ cc_prod A B.

Lemma cc_forall_elim A B x :
  empty ∈ cc_prod A B ->
  x ∈ A ->
  empty ∈ B x.

Definition cc_exists := sup.
Hint Unfold cc_exists.

Lemma cc_exists_typ A B :
  ext_fun A B ->
  (∀ x, x ∈ A -> B x ∈ props) ->
  cc_exists A B ∈ props.

Lemma cc_exists_intro A B x :
  ext_fun A B ->
  x ∈ A ->
  empty ∈ B x ->
  empty ∈ cc_exists A B.

Lemma cc_exists_elim A B :
  ext_fun A B ->
  empty ∈ cc_exists A B ->
  exists2 x, x ∈ A & empty ∈ B x.

mapping (meta-level) propositions to props back and forth

Definition P2p (P:Prop) := cond_set P (singl prf_trm).
Definition p2P p := prf_trm ∈ p.

Instance P2p_morph : Proper (iff ==> eq_set) P2p.
Qed.

Instance p2P_morph : Proper (eq_set ==> iff) p2P.
Qed.

Lemma P2p_typ : ∀ P, P2p P ∈ props.

Lemma P2p2P : ∀ P, p2P (P2p P) <-> P.

Lemma p2P2p : ∀ p, p ∈ props -> P2p (p2P p) == p.

Lemma P2p_forall A (B:set->Prop) :
   (∀ x x', x ∈ A -> x == x' -> (B x <-> B x')) ->
   P2p (∀ x, x ∈ A -> B x) == cc_prod A (fun x => P2p (B x)).

Lemma cc_prod_forall A B :
   ext_fun A B ->
   (∀ x, x ∈ A -> B x ∈ props) ->
   cc_prod A B == P2p (∀ x, x ∈ A -> p2P (B x)).

Lemma cc_arr_imp A B :
   B ∈ props ->
   cc_arr A B == P2p ((exists x, x ∈ A) -> p2P B).

Classical propositions: we also have a model for classical logic

Definition cl_props := subset props (fun P => ~~p2P P -> p2P P).

Lemma cc_cl_impredicative_prod : ∀ dom F,
  ext_fun dom F ->
  (∀ x, x ∈ dom -> F x ∈ cl_props) ->
  cc_prod dom F ∈ cl_props.

Lemma cl_props_classical P :
  P ∈ cl_props ->
  cc_arr (cc_arr P empty) empty ⊆ P.

Auxiliary stuff for strong normalization proof: every type contains the empty set.

Definition cc_dec x := singl empty ∪ x.

Instance cc_dec_morph : morph1 cc_dec.
Qed.

Lemma cc_dec_ax : ∀ x z,
  z ∈ cc_dec x <-> z == empty \/ z ∈ x.

Lemma cc_dec_prop :
    ∀ P, P ∈ cc_dec props -> cc_dec P ∈ props.

Lemma cc_dec_cl_prop :
    ∀ P, P ∈ cc_dec cl_props -> cc_dec P ∈ cl_props.

Correspondance between ZF universes and (Coq + TTColl) universes

Section Universe.

Hypothesis U : set.
Hypothesis Ugrot : grot_univ U.

Section Equiv_ZF_CIC_TTColl.

We assume now that U is a *ZF* universe (not just IZF), so it is closed by collection.

  Hypothesis coll_axU : ∀ A (R:set->set->Prop),
    A ∈ U ->
    (∀ x x' y y', in_set x A ->
     eq_set x x' -> eq_set y y' -> R x y -> R x' y') ->
    exists2 B, B ∈ U &
      ∀ x, in_set x A ->
        (exists2 y, y ∈ U & R x y) ->
        exists2 y, y ∈ B & R x y.

  Hypothesis sets : set.
  Hypothesis sets_incl_U : sets ⊆ U.

We prove that the model will validate TTColl (Ens.ttcoll). This formulation heavily uses the reification of propositions of the model as Coq's Prop elements.

Lemma cc_ttcoll A R :
  Proper (eq_set ==> eq_set ==> iff) R ->

  A ∈ U ->

  exists2 X, X ∈ U &

    exists2 f, f ∈ cc_arr X sets &

    ∀ x, x ∈ A ->
    (exists2 w, w ∈ sets & R x w) -> exists2 i, i ∈ X & R x (cc_app f i).

And now using the real connectives of props:

Lemma cc_ttcoll' : empty ∈

forall A : U,

cc_prod U (fun A =>

forall R : A->set->Prop,

cc_prod (cc_arr A (cc_arr sets props)) (fun R =>

exists X:U,

cc_exists U (fun X =>

exists g:X->set,

  cc_exists (cc_arr X sets) (fun g =>

    cc_prod A (fun i =>

(exists w:set, R i w) ->

cc_arr (cc_exists sets (fun w => cc_app (cc_app R i) w))

(exists j:X, R i (g j))

(cc_exists X (fun j => cc_app (cc_app R i) (cc_app g j)))))))).

End Equiv_ZF_CIC_TTColl.

End Universe.