Library EnsUniv

Require Import basic.

In this file we show that Coq universes allows to build Grothendieck universes. We take two copies of the set type, and we embed the "big set" of all the "small sets" (that we call U), and we show that U is a Grothendieck universe.

Require Ens0.
Require Ens.

Level 1: small sets

Module S := Ens0.IZF_R.

Level 2 : big sets

Module B := Ens.IZF_R.

Notations for big sets

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

This definition implies that the universe of indexes of small sets is lower than (or equal to) the universes of indexes of large sets (Ens0.Tlo <= Ens.Tlo)

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

Soundness of lifting

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

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

Lemma lift_in : ∀ x y, S.in_set x y -> injU x ∈ injU y.

Lemma down_in : ∀ x y, injU x ∈ injU y -> S.in_set x y.

Lemma down_in_ex x y y' :
  y == injU y' ->
  x ∈ y ->
  exists2 x', x == injU x' & S.in_set x' y'.

With the following, the universe of small sets is lower than (or equal to) the universe of indexes of big sets (Ens0.Thi <= Ens.Tlo).

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

Lemma U_intro : ∀ x, injU x ∈ U.

Lemma U_elim : ∀ x, x ∈ U -> exists x', x == injU x'.

Lemma injU_elim : ∀ x y, x ∈ injU y -> x ∈ U.

Equivalence of all set-theoretical constructions

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

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

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

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

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

Lemma U_trans : ∀ x y, y ∈ x -> x ∈ U -> y ∈ U.

Lemma U_pair : ∀ x y, x ∈ U -> y ∈ U -> B.pair x y ∈ U.

Lemma U_power : ∀ x, x ∈ U -> B.power x ∈ U.

Lemma U_union : ∀ x, x ∈ U -> B.union x ∈ U.

Lemma U_repl : ∀ a R,
  Proper (B.eq_set ==>B.eq_set ==>iff) R ->
  a ∈ U ->
  (∀ x y y', x ∈ a -> y ∈ U -> y' ∈ U ->
   R x y -> R x y' -> y == y') ->
  exists2 b, b ∈ U & ∀ y, y ∈ U ->
                         (y ∈ b <-> exists2 x, x ∈ a & R x y).

If the small sets are closed under collection, then so is U.

Lemma U_coll : ∀ a R,
  Proper (B.eq_set ==>B.eq_set ==>iff) R ->
  a ∈ U ->
  (∀ x, x ∈ a -> exists2 y, y ∈ U & R x y) ->
  exists2 b, b ∈ U & ∀ x, x ∈ a -> exists2 y, y ∈ b & R x y.

Grothendieck universe

Record grot_univ (U:B.set) : Prop := {
  G_trans : ∀ x y, y ∈ x -> x ∈ U -> y ∈ U;
  G_pair : ∀ x y, x ∈ U -> y ∈ U -> B.pair x y ∈ U;
  G_power : ∀ x, x ∈ U -> B.power x ∈ U;
  G_union : ∀ x, x ∈ U -> B.union x ∈ U;
  G_repl : ∀ a R, Proper (B.eq_set ==>B.eq_set ==>iff) R ->
           a ∈ U ->
           (∀ x y y', x ∈ a -> y ∈ U -> y' ∈ U -> R x y -> R x y' -> y == y') ->
           exists2 b, b ∈ U & ∀ y, y ∈ U -> (y ∈ b <-> exists2 x, x ∈ a & R x y) }.

Lemma U_univ : grot_univ U.