Extensional Model of ZF via Tree Description

Require Export Quotient_CR Embeddings.

(* Quotient construction assuming tree description (TD) and proof irrelevance (PI) *)

Parameter tdelta : (Acz -> Prop) -> Acz.

Axiom TDesc1 :
forall P, (exists s, forall t, P t <-> Aeq t s) -> P (tdelta P).

Axiom TDesc2 :
forall P P', (forall s, P s <-> P' s) -> tdelta P = tdelta P'.

(* The normaliser yielding the quotient model can be defined *)

Definition N s :=
tdelta (Aeq s).

Axiom PI : forall s (H H' : N s = s), H = H'.

Fact CR1 :
forall s, Aeq s (N s).
Proof.
intros s. pattern (N s). apply TDesc1. now exists s.
Qed.

Lemma CR2 :
forall s t, Aeq s t -> N s = N t.
Proof.
intros s t H. apply TDesc2.
intros u. rewrite H. tauto.
Qed.

Instance Norm : Normalizer :=
@Build_Normalizer N CR1 CR2 PI.

(* This turns Acz into a model of intensional ZF *)

Instance ACZ : ZFStruct :=
@Build_ZFStruct ACZ' tdelta.

Instance Acz_ZF :
iZF ACZ.
Proof.
split; try apply Acz_ZF'.
- intros P [s H]. apply TDesc1.
exists s. intros u. rewrite (H u), Aeq_equiv.
split; now intros ->.
- apply TDesc2.
Qed.

(* The quotient model inherits the description operator *)

Definition desc (P : SET' -> Prop) :=
NS (tdelta (fun s => empred P s)).

Instance SET : ZFStruct :=
@Build_ZFStruct SETZF' desc.

(* Hence SET satisfies extensional ZF *)

Lemma descAx (P : SET -> Prop) X :
P X -> unique P -> P (desc P).
Proof.
intros H1 H2.
enough (empred P (tdelta (empred P))) by assumption.
apply TDesc1. exists (proj1_sig X).
intros t. split; intros H.
- now apply NS_eq_Aeq_p1, H2.
- symmetry in H. apply (empred_Aeq H).
hnf. now rewrite NS_p1_eq.
Qed.

Lemma descAx1 (P : SET -> Prop) :
iseqcl P -> P (desc P).
Proof.
intros [X H]. apply (@descAx P X).
- apply H. now apply set_ext.
- intros Y Y' H1 H2.
apply H, set_ext in H1.
apply H, set_ext in H2.
congruence.
Qed.

Lemma descAx2 (P P' : SET -> Prop) :
(forall x, P x <-> P' x) -> desc P = desc P'.
Proof.
intros H. apply Aeq_NS_eq, Aeq_ref', TDesc2.
intros s. apply H.
Qed.

Instance SET_ZF :
ZF SET.
Proof.
split; try apply set_ext.
split; try apply SETZF_ZF'.
- apply descAx1.
- apply descAx2.
Qed.

Hint Resolve Acz_ZF SET_ZF.

(* ACZ and SET agree on the notion of universe and strength *)

Definition ATS (s : ACZ) : SET :=
NS s.

Lemma ATS_mor s t :
s el t <-> ATS s el ATS t.
Proof.
split; intros H.
- now apply Ain_IN_NS.
- now apply IN_Ain_NS.
Qed.

Lemma ATS_sur s x :
x el ATS s -> exists t, t el s /\ ATS t == x.
Proof.
intros H. exists (proj1_sig x). split.
- now apply IN_Ain_p1_NS.
- apply set_ext. apply NS_p1_eq.
Qed.

Fact ATS_universe u :
universe u <-> universe (ATS u).
Proof.
apply h_universe.
- apply ATS_mor.
- apply ATS_sur.
Qed.

Fact ATS_strength s n:
strength n s <-> strength n (ATS s).
Proof.
apply h_strength.
- apply ATS_mor.
- apply ATS_sur.
Qed.