coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question about maximum operation for universe levels in Coq

From: Erik Palmgren <palmgren AT math.su.se>
To: coq-club AT inria.fr
Subject: [Coq-Club] Question about maximum operation for universe levels in Coq
Date: Tue, 21 Feb 2017 15:56:14 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=palmgren AT math.su.se; spf=Pass smtp.mailfrom=palmgren AT math.su.se; spf=None smtp.helo=postmaster AT mail-prod-route04.it.su.se
Ironport-phdr: 9a23:ZojPcx12Fox0PAbBsmDT+DRfVm0co7zxezQtwd8Zse0SKPad9pjvdHbS+e9qxAeQG96KtrQd16GI4ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMhDexe65+IRq5oQjQssQdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LptRRT1iikIKiQ5/XnKhMJugqJVoBGvqRJxzIHbYo6aKPVwc7jBfd4ZX2dNQtpdWiJDD466coABD/ABPeFdr4TlqFUOtxq+BQqxD+310DBIgnr23aIg0+s/FwHNwQstH8oUv3TQqdX1O70SXv6zzKTTyDXMde9W2Tfn5IjTbxAtu+qMUqxpfMfX1EIhFBvFg02SpIHnJT+ZyOoAvmuB4+duV++jkXMrpg9trjS328shhJXFipgLxl3K9yh12ps5KNykREJhf9KoDpRduieHPIVsWMwiWXtnuCMix70Gp5G7eC8KxYwixxHFavyHd5GE4gr5VOaWPDh0nWhleLWihxau70es1uLxWtO10FZWtCZFicTMumoW1xPN8sSHS/198Vm92TuX1Q3e6PtILV46mKfYMZIszLw9moAOvUnNAiP6gED2g7WXdkUg9Oio8ePnYrD+q5+ELYB0jgT+Mqs0msOhB+Q1KQ0OUHKH+eS8zrHj5lD5TK9RjvIoiqXZqozVJdwHpq6lBA9Yypos6xGmDzu/zNsYmWQHI0ledRKcj4npPknOL+riAfe+hVSsijZryOrcMr3vGJWeZkTExbzmZPN271NW4As119FWoZxOWZ8bJ/emd1Xwt5TgBxs8PBa5xa6zENx504wEVGSnB6aFMOXJrBmT67R8cKG3eIYJtWOleLAe7Pn0gCphlA==

Hello

I wonder whether there is a way to take the
maximum of two universe levels in Coq just
as there is in Agda? Thus making it possible to write
something like:

Theorem Foo(A:Type@{i})(B:Type@{j}):
∃ C:Type@{max i j}, ... .

Thanks in advance!

Erik Palmgren

[Coq-Club] setoid rewriting, partial application and relfexivity, Vadim Zaliva, 02/17/2017
- Re: [Coq-Club] setoid rewriting, partial application and relfexivity, Vadim Zaliva, 02/17/2017
  - Re: [Coq-Club] setoid rewriting, partial application and relfexivity, John Wiegley, 02/17/2017
    - Re: [Coq-Club] setoid rewriting, partial application and relfexivity, Vadim Zaliva, 02/18/2017
      - [Coq-Club] Question about maximum operation for universe levels in Coq, Erik Palmgren, 02/21/2017
        
        Re: [Coq-Club] Question about maximum operation for universe levels in Coq, Bas Spitters, 02/22/2017