Library universe

Notation "[univ]" := Type.

Notation "! x" := (notT x)%type (at level 75, right associativity).
Notation "T # U" := (T × U)%type (at level 80, right associativity).
Notation "T [+] U" := (T + U)%type (at level 80, right associativity).

Notation "{ a : T $ P }" := {a : T × P} (at level 0, a at level 99).

Notation "injL( a )" := (inl a) (at level 0).
Notation "injR( a )" := (inr a) (at level 0).
Notation "exI( a , b )" := (existT _ a b) (at level 0).