Library EnsUniv

Require Import Setoid.


Require Ens0.
Require Ens.
Module S := Ens0.IZF. Module B := Ens.IZF.
Fixpoint injU (a:S.set) : B.set :=
  match a with
    S.sup X f => B.sup X (fun i => injU (f i))
  end.

Definition U : B.set := B.sup S.set injU.

Notation "x \in y" := (B.in_set x y) (at level 60).
Notation "x == y" := (B.eq_set x y) (at level 70).

Lemma U_elim : forall x, x \in U -> exists x', x == injU x'.

Lemma U_intro : forall x, injU x \in U.

Lemma injU_elim : forall x y, x \in injU y -> x \in U.

Lemma lift_eq : forall x y, S.eq_set x y -> injU x == injU y.

Lemma down_eq : forall x y, injU x == injU y -> S.eq_set x y.

Lemma lift_in : forall x y, S.in_set x y -> injU x \in injU y.

Lemma down_in : forall x y, injU x \in injU y -> S.in_set x y.

Lemma subset_equiv : forall x P Q,
  (forall x y, y == injU x -> (P x <-> Q y)) ->
  injU (S.subset x P) == B.subset (injU x) Q.

Lemma power_equiv : forall x, B.power (injU x) == injU (S.power x).

Lemma pair_equiv : forall x y,
  B.pair (injU x) (injU y) == injU (S.pair x y).

Lemma union_equiv : forall x, B.union (injU x) == injU (S.union x).

Lemma repl1_equiv : forall x f a F,
  a == injU x ->
  (forall x x', proj1_sig x' == injU (proj1_sig x) -> F x' == injU (f x)) ->
  B.repl1 a F == injU (S.repl1 x f).

Record grot_univ (U:B.set) : Prop := {
  G_trans : forall x y, y \in x -> x \in U -> y \in U;
  G_pair : forall x y, x \in U -> y \in U -> B.pair x y \in U;
  G_power : forall x, x \in U -> B.power x \in U;
  G_union_repl : forall I F,
                 (forall x x', proj1_sig x == proj1_sig x' -> F x == F x') ->
                 I \in U ->
                 (forall x, F x \in U) ->
                 B.union (B.repl1 I F) \in U }.

Lemma U_univ : grot_univ U.