universe.v

Require Import Coq.Unicode.Utf8.
Require Coq.Program.Equality.
Require Coq.Vectors.Vector.
Require Coq.Lists.List.

Import IfNotations.
Import List.ListNotations.
Import Vector.VectorNotations.

Section SET.
  Context {S: Set} {EL: S → Set}.

  Inductive sort :=
  | unit
  | Σ (A: S) (B: EL A → sort)
  | Π (A: S) (B: EL A → sort)
  .
  Arguments sort: clear implicits.

  Inductive El: sort → Set :=
  | tt: El unit
  | pair {A} {B: EL A → sort} (a: EL A): El (B a) → El (Σ A B)
  | Λ {A} {B: EL A → sort}: (∀ a, El (B a)) → El (Π A B)
  .
  Arguments El: clear implicits.
End SET.

Arguments sort: clear implicits.
Arguments El {S EL}.

Inductive U := TRV | SUCC (n: U).

Notation "n '+1'" := (SUCC n) (at level 1).

Module Univ.
  Record t := {
      sort: Set ;
      El: sort → Set ;
    }.
End Univ.

Fixpoint UNIV (u: U): Univ.t :=
  match u with
  | TRV => {| Univ.sort := Datatypes.Empty_set ; Univ.El x := match x with end |}
  | n' +1 => {|
              Univ.sort := sort (Univ.sort (UNIV n')) (Univ.El (UNIV n')) ;
              Univ.El := El ;
             |}
  end.

Definition SORT u := Univ.sort (UNIV u).
Definition EL {u}: SORT u → _ := Univ.El (UNIV u).

Coercion SORT: U >-> Sortclass.

Definition SET := SUCC TRV.