coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Question about maximum operation for universe levels in Coq
Date: Wed, 22 Feb 2017 17:27:42 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f175.google.com
Ironport-phdr: 9a23:TsoCOxZsMPExe/Qwoy3Q/TP/LSx+4OfEezUN459isYplN5qZr82ybnLW6fgltlLVR4KTs6sC0LuL9fm+Ejxeqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjSwbLdyIRmssAnct8YajIhjJ60s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlTwKPCAl/m7JlsNwjbpboBO/qBx5347Ue5yeOP5ncq/AYd8WWW9NU8BMXCJDH4y8dZMCAOgPPehYoYfzpEYAowWiCgejH+7v1iZIi2Xq0aEmz+gsEwfL1xEgEdIUt3TUqc34OboIXuCu0aLG0C3Db/JK2Tfh9ofIaAshquyLUL1ra8be01MjFg3fglWLsYzlPi+V1vgTvGiB9OptTu2vi2s9pAFwpjij3Nsjio7Mho8MzF3P6Ct3wIEwJdKiSU57Z8apEJRRtyGGN4t2X9gtT3t0tyY9z70Lv4OwcisSyJk/2RLTd/iKf5KL7x/jTuqdPyp0iXN/dL6ihRu/8U6twfDmWMauylZFtC9Fn8HMtn8T0xzT7dCKSv5n8Ueg3TaDzhnT6v1YLUwtm6rXNpwsz74qmpoctkTDGSD2mEHog6OMakok/e2o5/zmYrXguJCcK5d5hh/iPqkqgMCyAuQ1PhIQU2SG+OmwzqDv8E/5TblSi/05iKjZsJTUJcQBoa65BhdY3Z055xmlFTun3s4UnWIfLFJEZBKHk5bmO0vVIP3jAve/hk6jkDZvx/zcIrLhBZDNImDZkLj9ZbZ991JcyA0rwN9D4JJUE6gNL+73Wk/sr9PVFQQ5Mgyxw+b/EtpxzIIeWWSVAq+YKqzeq1GI5vh8a9WLMaQSoX7WL+Uvr6rlimZ8klsAd4Go24EWYTa2BKI1DV+eZC/Gi8xJKn8LohYzVvei3FfEWHhMIW2qXr4g6ysgII2jBIbHAIuqherSj2+AApRKazUeWRi3GnDyetDBAq9UZQ==

I think the syntax is Type@{max(a,i)}, like in our HoTT library:
https://github.com/HoTT/HoTT/blob/master/theories/Modalities/Localization.v#L277

On Tue, Feb 21, 2017 at 3:56 PM, Erik Palmgren
<palmgren AT math.su.se>
wrote:
> 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