The Coq mailing list

[Amin Timany <amintimany AT gmail.com>]

Hi,

Another solution, if you are using 8.7beta1 or the development branch of Coq, 
is to enable cumulativity for inductive types. In this case, the inferred 
cumulativity (subtyping) relation for trees is as that every small tree is 
also a large one.

Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.

Set Printing Universes.

Inductive Tree : Type :=
  sup : forall A : Type, (A -> Tree) -> Tree.

Fixpoint emb' (s : Tree) :=
  let (A, f) := s in
  sup A (fun a => emb' (f a)).

Definition T := sup Tree emb’.

Considering the code above “Print Tree.” command prints:


Cumulative Inductive Tree@{Top.8} : Type@{Top.8+1} :=
    sup : forall A : Type@{Top.8},
          (A -> Tree@{Top.8}) -> Tree@{Top.8}
(* Top.8 |= 
   
   ~@{Top.8} <= ~@{Top.9} iff 
   Top.8 <= Top.9
    *)

For sup: Argument scopes are [type_scope function_scope]


Here “   ~@{Top.8} <= ~@{Top.9} iff  Top.8 <= Top.9” that any term of type 
Tree@{i} is also a term of type Tree@{j} whenever i <= j.

Regards,
Amin


> On 14 Sep 2017, at 12:36, Guillaume Melquiond 
> <guillaume.melquiond AT inria.fr>
>  wrote:
> 
> On 13/09/2017 10:26, Dominik Kirst wrote:
> 
>> When tagging the function type explicitly with two (unconstrained)
>> universe variables, the exact level of the codomain is kept variable and
>> the supremum becomes definable. Is this behaviour an intended minimisation?
> 
> I would not even qualify that behavior as minimization; it looks like
> plain inference.
> 
> For example, (fun x : Type => x) is inferred as (Type@{i} -> Type@{i}),
> not as (Type@{i} -> Type@{j} | i <= j), and this is intended.
> 
> So, if you want extra universes and constraints, just add them by hand:
> 
> Fixpoint emb'@{i j} (s : Tree@{i}) : Tree@{j} :=
>  let (A, f) := s in
>  sup A (fun a => emb' (f a)).
> 
> Best regards,
> 
> Guillaume