Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page