Can a Prop show that all entries of a list equal Type@{U} for any U?

Question

In Coq, is it possible to write a predicate (list Type -> Prop) that is only provable if all entries of the list are of the form Type@{U}?

The predicate should accept Types from different universes within the same list. For example, [Type@{U1}; Type@{U2}] should be accepted, where U1 < U2. Other types, such as nat, should not be accepted in the list.

The closest I was able to get is to have the predicate verify that each entry of the list is a universe-like type that has some of the properties of Type@{U}:

• The universe-like types form a chain, where the previous one is embedded within the next.
• Set is at the start of the chain.
• Each universe-like type has an export function that can convert an inhabitant of the universe-like type, T: UT, into an inhabitant of T@{max}. That is, export: UT -> Type@{max}.

However, that predicate also accepts types which are not of the form Type%{U}, such as (Type * nat)%type.

Require Import List.

Import ListNotations.

Inductive TypeChain: forall (carrier: Type), (carrier -> Type) -> Type :=
| TypeChainSet: TypeChain Set (fun s: Set => s)
| TypeChainNext:
  forall prev_carrier prev_export,
  TypeChain prev_carrier prev_export ->
  forall carrier (export: carrier -> Type) (import: prev_carrier -> carrier),
  (forall p: prev_carrier, export (import p) = prev_export p) ->
  forall prev_embed,
  (export (prev_embed) = prev_carrier) ->
  TypeChain carrier export.

Inductive InTypeChain (T: Type):
    forall {carrier export}, TypeChain carrier export -> Prop :=
| InTypeChainTop: forall export (chain: TypeChain T export),
  InTypeChain T chain
| InTypeChainPrev:
  forall prev_carrier prev_export prev_chain,
  InTypeChain T prev_chain ->
  forall carrier export import export_imported prev_embed prev_embed_matches,
  InTypeChain T (TypeChainNext prev_carrier prev_export prev_chain carrier
                 export import export_imported prev_embed prev_embed_matches).

Definition ListContainsOnlyTypes (l: list Type) :=
exists carrier export (c: TypeChain carrier export),
  Forall (fun T => InTypeChain T c) l.

Module GoodExample.

Universe U1 U2.
Constraint U1 < U2.

Definition ChainU2: TypeChain Type@{U2} (fun T => T).
Proof.
  unshelve eapply (TypeChainNext Type@{U1}); auto.
  unshelve eapply (TypeChainNext Type@{Set}); auto.
  unshelve apply TypeChainSet.
Defined.

Example GoodListAccepted: ListContainsOnlyTypes [Type@{U1}; Set; Type@{U2}].
Proof.
  eexists.
  eexists.
  exists ChainU2.
  eauto 7 using InTypeChain.
Qed.

End GoodExample.

Module BadExample.

Definition BadChain: TypeChain (Type * nat) (fun T => fst T).
Proof.
  unshelve eapply (TypeChainNext Set); auto.
  - exact (fun s:Set => (s:Type, 0)).
  - exact (Set, 0).
  - apply TypeChainSet.
  - reflexivity.
  - reflexivity.
Defined.

Example BadListAccepted: ListContainsOnlyTypes [(Type * nat)%type; Set].
Proof.
  eexists.
  eexists.
  exists BadChain.
  eauto using InTypeChain.
Qed.

End BadExample.

Answer 1

As pointed out in the comments, universes are very underspecified in CIC, so that the kind of things you want to do is not easily feasible.

If you want to do "intensional" analysis of types, a good solution is often to consider codes rather than types. Here is a very naïve example:

Require Import List.
Import ListNotations.

Inductive code : Type :=
  | ty : code
  | ar : code -> code -> code
  | n : code.

Fixpoint El (c : code) : Type :=
  match c with
  | ty => Type
  | ar c1 c2 => El c1 -> El c2
  | n => nat
  end.

Inductive CodeChain : list code -> Prop :=
  | cnil : CodeChain []
  | ccons l : CodeChain l -> CodeChain (ty :: l).

Definition TypeChain (l : list Type) : Prop :=
  exists l', l = map El l' /\ CodeChain l'.

There are multiple difficulties here, however.

First, while CodeChain encodes the predicate you are looking for, TypeChain is somewhat too lose again, because eg we cannot derive falsity from TypeChain [nat*Type], while we can derive it from eg CodeChain [n]. Basically, applying El loses the intensional content you are looking for. So you should as much as possible reason on the codes rather than the types.

Second, because Coq cannot reason about universe levels is a first class way, you cannot specify in your codes that the ty constructor should be at a given level.

Third, and maybe the biggest limitation, this inductive presentation of codes does not scale to dependent types. Indeed, in such a setting you would want to write a constructor for dependent function type as ar : forall A : code, (El A -> code) -> code, but this means El and code need to be defined mutually. This is called an inductive-recursive definition, and is not available in Coq (but it is in Agda for instance).