Parameter set : Type.
Parameter IN : set → set → Prop.
Infix ":e" := IN (at level 70).

Definition Subq (X Y:set) : Prop := ∀ z, z :e X → z :e Y.
Infix "c=" := Subq (at level 70).

Axioms

Extensionality
Axiom set_ext : ∀ X Y, X c= Y → Y c= X → X = Y.

Empty
Parameter empty : set.
Axiom emptyE : ∀ (x:set), ¬ x :e empty.

Unions
Parameter union : set → set.
Axiom unionAx : ∀ (x z:set), z :e union x ↔ ∃ y, y :e x ∧ z :e y.

Power Sets
Parameter power : set → set.
Axiom powerAx : ∀ (X:set), ∀ Y:set, Y c= X ↔ Y :e power X.

Specifications

Description Specification
Record DescrSpec : Type := mkDescr
{
  descr : (set → Prop) → set;
  descrAx : ∀ P:set → Prop, (∃! y, P y) → P (descr P)
}.

Separation Specification
Record SepSpec : Type := mkSep
{
  sep : set → (set → Prop) → set;
  sepAx : ∀ X P z, z :e sep X P ↔ z :e X ∧ P z
}.

Total Replacement Specification
Record TotReplSpec : Type := mkTotRepl
{
  repS : set → (set → set → Prop) → set;
  repSAx : ∀ X:set, ∀ P:set → set → Prop, (∀ x, x :e X → ∃! y, P x y) → ∀ y, y :e repS X P ↔ ∃ x, x :e X ∧ P x y
}.

Map Replacement Specification
Record MapReplSpec : Type := mkMapRepl
{
  repM : set → (set → set) → set;
  repMAx : ∀ X:set, ∀ F:set → set, ∀ y, y :e repM X F ↔ ∃ x, x :e X ∧ F x = y
}.

Partial Replacement Specification (No requirement that P is a *total* functional relation on X). This is the version Barras uses.
Record PartReplSpec : Type := mkPartRepl
{
  repP : set → (set → set → Prop) → set;
  repPAx : ∀ X:set, ∀ P:set → set → Prop, (∀ x, x :e X → ∀ y z, P x y → P x z → y = z) → ∀ y, y :e repP X P ↔ ∃ x, x :e X ∧ P x y
}.

TotRepl <-> Descr /\ MapRepl

Definition TotRepl_Descr : TotReplSpec → DescrSpec.
Defined.

Definition TotRepl_MapRepl : TotReplSpec → MapReplSpec.
Defined.

Definition Descr_MapRepl_TotRepl : DescrSpec → MapReplSpec → TotReplSpec.
Defined.

PartRepl <-> Sep /\ TotRepl

Definition PartRepl_Sep : PartReplSpec → SepSpec.
Defined.

Definition PartRepl_TotRepl : PartReplSpec → TotReplSpec.
Defined.

Definition Sep_TotRepl_PartRepl : SepSpec → TotReplSpec → PartReplSpec.
Defined.