Require Export Axioms.

Section Basic_Constructions.
Context {S : ZF_Model}.

Global Instance big_union_is_definable :
  Is_Definable big_union.
Admitted.

Definition singleton u :=
  `{u, u}.
Notation "`{ u }" := (singleton u)
                       (at level 9, u at level 69, format "`{ u }").

Lemma in_singleton_iff u y :
  y ∈ `{u} ↔ y = u.
Proof. unfold singleton. rewrite in_unordered_pair_iff. tauto. Qed.

Instance singleton_is_definable :
  Is_Definable singleton.
Proof.

Admitted.

Record Set_Like :=
  build_set_like {
      set_like_type :> Type;
      set_like_encoding : Encoding_Of set_like_type;
      set_like_is_a_set : Is_A_Set set_like_encoding
    }.
Global Existing Instance set_like_encoding.
Global Existing Instance set_like_is_a_set.
Definition set_like_as_set (A : Set_Like) : S :=
  let H := set_like_is_a_set A in
  class_as_set (encoding_of A).
Canonical Structure canonical_set_like
          (A : Type)
          {encoding : Encoding_Of A}
          {is_a_set : Is_A_Set encoding} :
  Set_Like :=
  build_set_like A encoding is_a_set.
Global Instance encoding_of_set_like_is_definable (A : Set_Like) :
  let d := @definability_on_Class _ : ∀ n (type : Env_Type n),
          Definability_On (fun _ : type ⇒ Class) in
  Is_Definable (encoding_of A : Class).
Admitted.

Global Instance definability_on_Set_Like {n} (type : Env_Type n) :
  Definability_On (fun _ : type ⇒ Set_Like).
Admitted.

Existing Instance composition_with_env_tail_is_env_reduction.


Global Instance canonical_class_like_is_definable
       (A : Type) :
  Is_Definable (@canonical_class_like S A).
Proof. intros n type. intros n' type' r E HE. exact HE. Qed.

Global Instance set_like_encoding_is_definable :
  Is_Definable set_like_encoding.
Admitted.

Global Instance set_like_is_definable
       (A : Set_Like) :
  Is_Definable A.
Admitted.

Program Definition replacement
        (A : Set_Like) (f : A → S) (definable : Is_Definable f) : S :=
  relation_replacement
    (fun x y ⇒ ∃ z : A, f z = y ∧ (encode z : S) = x)
    _
    _
    (set_like_as_set A).
Next Obligation.
  intros x y y'.
  intros (z & <- & H).
  intros (z' & <- & <-).
  apply element_equality in H.
  rewrite <- (decode_encode z).
  rewrite <- (decode_encode z').
  rewrite H.
  reflexivity.
Qed.

Notation "`{ f | x : A }" := (replacement (canonical_set_like A)
                                          (fun x ⇒ f) _)
                               (at level 9, f at level 69, x ident).

Lemma in_replacement_iff
      (A : Type) {encoding : Encoding_Of A} {is_a_set : Is_A_Set encoding}
      (f : A → S) {definable : Is_Definable f} y :
  y ∈ `{ f x | x : A } ↔ ∃ x : A, y = f x.
Admitted.

Global Instance replacement_is_definable :
  Is_Definable replacement.
Admitted.

Opaque replacement.

Parameter separation :
  ∀ (A : S) (P : A → Prop),
    Is_Definable P → S.

Notation "`{ x ∈ A | P }" := (separation A (fun x ⇒ P) _)
                               (at level 9, x at level 69).
Notation "`{ x ⊆ A | P }" := (separation (𝒫 A) (fun x ⇒ P) _)
                               (at level 9, x at level 69).

Axiom in_separation_iff :
  ∀ A P definable x,
    x ∈ separation A P definable ↔ ∃ H : x ∈ A, P (element x).

Definition indexed_union
           (I : Set_Like)
           (F : I → S)
           (definable : Is_Definable F) :=
  big_union `{ F i | i : I }.
Notation "⋃ i : I , F" := (indexed_union _ (fun i : I ⇒ F) _)
                            (at level 200, i ident, right associativity).

Global Instance indexed_union_is_definable :
  Is_Definable indexed_union.
Admitted.

Lemma in_indexed_union_iff
      (I : Set_Like)
      (F : I → S) {HF : Is_Definable F} x :
  x ∈ (⋃ i : I, F i) ↔ ∃ i : I, x ∈ F i.
Proof.
  unfold indexed_union.
  rewrite in_big_union_iff.
  split.
Admitted.

Opaque indexed_union.

Definition union (A B : S) :=
  ⋃ C : `{A, B}, C.

Notation "A ∪ B" := (union A B) (at level 50).

Axiom in_union_iff : ∀ A B x, x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B.

Global Instance union_is_definable :
  Is_Definable union.
Admitted.

Opaque union.

Parameter intersection : S → S → S.
Notation "A ∩ B" := (intersection A B) (at level 40).
Axiom in_intersection_iff : ∀ A B x, x ∈ A ∩ B ↔ x ∈ A ∧ x ∈ B.

Global Instance canonical_set_like_is_definable
       {n} {type : Env_Type n}
       (A : type → Type)
       (E : ∀ env, Encoding_Of (A env))
       (HE : ∀ env, Is_A_Set (E env)) :
  Is_Definable_In_Env (fun env ⇒ canonical_set_like (A env)).
Admitted.

Definition replacement2
           (A : Set_Like)
           (B : A → Set_Like)
           {B_is_definable : Is_Definable B}
           (f : ∀ x, B x → S) (definable : Is_Definable f) :=
  ⋃ x : A, ⋃ y : B x, `{ f x y }.

Definition replacement3
        (A : Set_Like)
        (B : A → Set_Like)
        {B_is_definable : Is_Definable B}
        (C : ∀ x, B x → Set_Like)
        {C_is_definable : Is_Definable C}
        (f : ∀ x y, C x y → S) (definable : Is_Definable f) :=
  ⋃ x : A, ⋃ y : B x, ⋃ z : C x y, `{ f x y z }.

Notation "`{ f | x : A , y : B }" :=
  (replacement2 _ _ (fun (x : A) (y : B) ⇒ f) _)
    (at level 9, f at level 69, x ident, y ident).

Lemma in_replacement2_iff
      (A : Set_Like)
      (B : A → Set_Like)
      {B_is_definable : Is_Definable B}
      (f : ∀ x, B x → S) (definable : Is_Definable f)
      (z : S) :
  z ∈ `{ f x y | x : A, y : B x } ↔ ∃ (x : A) (y : B x), z = f x y.
Proof.
  unfold replacement2.
  repeat setoid_rewrite in_indexed_union_iff.
Admitted.

Lemma unordered_pairs_are_equal_impl' u v u' v' :
  `{u, v} = `{u', v'} →
  (u = u' ∨ u = v') ∧ (v = u' ∨ v = v').
Proof.
  intros H.
  repeat rewrite <- in_unordered_pair_iff.
  repeat rewrite <-H.
  repeat rewrite in_unordered_pair_iff.
  tauto.
Qed.

Lemma unordered_pair_symmetric u v :
  `{u, v} = `{v, u}.
Proof. apply extensionality. setoid_rewrite in_unordered_pair_iff. tauto. Qed.

Lemma unordered_pairs_are_equal_iff' u v u' v' :
  `{u, v} = `{u', v'} ↔
  ((u = u' ∨ u = v') ∧ (v = u' ∨ v = v')) ∧
  ((u' = u ∨ u' = v) ∧ (v' = u ∨ v' = v)).
Proof.
  split.
  - intros H. split.
    + apply unordered_pairs_are_equal_impl'. exact H.
    + apply unordered_pairs_are_equal_impl'. symmetry. exact H.
  - intuition subst; try reflexivity.
    apply unordered_pair_symmetric.
Qed.

Lemma unordered_pairs_are_equal_iff u v u' v' :
  `{u, v} = `{u', v'} ↔
  (u = u' ∧ v = v') ∨ (u = v' ∧ v = u').
Proof. pose (unordered_pairs_are_equal_iff' u v u' v'). intuition. Qed.

Definition Is_Injective {A B} (f : A → B) :=
  ∀ x x', f x = f x' → x = x'.

Require Import Coq.Logic.Epsilon.
Arguments element_property {_ _} _.

Definition build_encoding_from_injection {A : Type} (f : A → S)
  (injectivity : Is_Injective f) :
    Encoding_Of A.
Proof.
  set (carrier := build_class (fun y ⇒ ∃ x, y = f x)).
  unshelve eset (encode x := element (f x) : carrier). {
    ∃ x. reflexivity.
  }
  unshelve eset (decode (y : carrier) := epsilon _ (fun x ⇒ y = f x :> S)). {
    destruct (element_property y) as [x _]. exact (inhabits x).
  }
    
  refine (build_encoding A
                         carrier
                         encode
                         decode
                         _).
  - intros x. unfold decode, encode. cbn.
    apply injectivity. symmetry. apply epsilon_spec. ∃ x. reflexivity.
Defined.

Parameter description : ∀ {A : Type} (P : A → Prop) {H : ∃! x, P x}, A.
Axiom description_property :
  ∀ {A : Type} (P : A → Prop) {H : ∃! x, P x},
    P (@description _ P H).

Global Instance prod_is_definable :
  Is_Definable (prod : Type → Type → Type).
Proof.
Admitted.

Lemma encode_is_injective A {encoding : Encoding_Of A} :
  Is_Injective encode.
Admitted.

Program Instance product_encoding
        (A B : Type) {HA : Encoding_Of A} {HB : Encoding_Of B} :
  Encoding_Of (A × B) :=
  build_encoding_from_injection
    (fun xy ⇒ `{`{encode (fst xy)}, `{encode (fst xy), encode (snd xy)}})
    _.
Next Obligation.
  intros [x y] [x' y']; cbn.
  intros H.
  enough (H1 : encode x = encode x' :> S ∧ encode y = encode y' :> S). {
    destruct H1 as [H2 H3].
    apply element_equality in H2. apply element_equality in H3.
    apply encode_is_injective in H2. apply encode_is_injective in H3.
    congruence.
  }
  unfold singleton in H. repeat rewrite unordered_pairs_are_equal_iff in H.
  intuition congruence.
Qed.

Instance unordered_pair_is_definable :
  Is_Definable unordered_pair.
Admitted.

Instance pair_is_definable A B {HA : Encoding_Of A} {HB : Encoding_Of B} :
  Is_Definable (@pair A B).
Proof.
Admitted.

Instance fst_is_definable A B {HA : Encoding_Of A} {HB : Encoding_Of B} :
  Is_Definable (@fst A B).
Proof.
Admitted.

Parameter ordinals : Class.
Parameter ordinal_successor : ordinals → ordinals.
Notation σ := ordinal_successor.
Parameter ordinal_limit : ∀ (A : S) {_ : A ⊆ ordinals}, ordinals.

Program Definition ordinal_zero : ordinals :=
  @ordinal_limit ∅ _.
Next Obligation. apply not_in_empty_set in H. contradiction. Qed.

Axiom ordinals_is_transitive :
  ∀ α : ordinals, ∀ β : α, β ∈ ordinals.
Global Existing Instance ordinals_is_transitive.

Definition Is_Successor_Ordinal (α : ordinals) :=
  ∃ β : ordinals, α = σ β.
Definition Is_Limit_Ordinal (α : ordinals) :=
  ¬ Is_Successor_Ordinal α.

Axiom ordinal_induction :
  ∀ P : ordinals → Prop,
    (∀ α : ordinals, P α → P (ordinal_successor α)) →
    (∀ λ : ordinals, Is_Limit_Ordinal λ → (∀ α : λ, P (element α)) → P λ) →
    ∀ α, P α.

Parameter ordinal_recursion :
  ∀ (f : S → S) {Hf : Is_Definable f},
  ∀ (g : S → S) {Hg : Is_Definable g},
    ordinals → S.

Global Instance ordinal_recursion_is_definable :
  Is_Definable ordinal_recursion.
Admitted.

Axiom ordinal_recursion_on_successor :
  ∀ (f : S → S) (Hf : Is_Definable f),
  ∀ (g : S → S) (Hg : Is_Definable g),
  ∀ α,
    ordinal_recursion f g (ordinal_successor α) =
    f (ordinal_recursion f g α).
Axiom ordinal_recursion_on_limit :
  ∀ (f : S → S) (Hf : Is_Definable f),
  ∀ (g : S → S) (Hg : Is_Definable g),
  ∀ λ,
    Is_Limit_Ordinal λ →
    ordinal_recursion f g λ =
    g `{ordinal_recursion f g (element α) | α : λ}.

Axiom numerals : Encoding_Of nat.
Existing Instance numerals.


End Basic_Constructions.

Notation "`{ u }" := (singleton u)
                       (at level 9, u at level 69, format "`{ u }").
Notation "`{ f | x : A }" := (replacement (canonical_set_like A)
                                          (fun x ⇒ f) _)
                               (at level 9, f at level 69, x ident).
Notation "`{ x ∈ A | P }" := (separation A (fun x ⇒ P) _)
                               (at level 9, x at level 69).
Notation "`{ x ⊆ A | P }" := (separation (𝒫 A) (fun x ⇒ P) _)
                               (at level 9, x at level 69).
Notation "⋃ i : I , F" := (indexed_union (canonical_set_like I) (fun i ⇒ F) _)
                            (at level 200, i ident, right associativity).
Notation "A ∪ B" := (union A B) (at level 50).
Notation "A ∩ B" := (intersection A B) (at level 40).
Notation "`{ f | x : A , y : B }" :=
  (replacement2 (canonical_set_like A)
                (fun x ⇒ canonical_set_like B)
                (fun (x : A) (y : B) ⇒ f)
                _)
    (at level 9, f at level 69, x ident, y ident).