Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Universe Polymorphism

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Universe Polymorphism


Chronological Thread 
  • From: Helmut Brandl <helmut.brandl AT gmx.net>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Universe Polymorphism
  • Date: Wed, 16 Nov 2022 21:02:05 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=helmut.brandl AT gmx.net; spf=Pass smtp.mailfrom=helmut.brandl AT gmx.net; spf=None smtp.helo=postmaster AT mout.gmx.net
  • Ironport-data: A9a23:euKWd6NC8Ro609PvrR22k8FynXyQoLVcMsEvi/4bfWQNrUon0TBVn WAcXGuDO/iIYmr1eoh0b4i1o0oFvsKAzoBgS3M5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/jgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5CZaQHNNwJcaDpOsfva8U035pwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGXsQSPJk/dJC3trINw0psQwIyZ+7 fohfWVlghCr34pawZq+TfRwwMsmPI/tMZ93VnNIl2iDS6x8HtaaHOOQv7e03x9o7ixKNfbTY 88EdXxldh3GbxlnNVIHTpQzgI9Eg1GgI2AI8wnO/cLb5UDtyD0h25+9NeDvZ92KRPhnjn63j 3jZqjGR7hYybYHDl2PcrBpAnNTnliTiHYkWCbeQ7e9vmFTVx2oJCRRQW0HTnBWioku5Rs4ZJ EkEvCwjscDe6XBHUPHXbUWd8HyjuSRBRot8T899yka90qzttlPx6nc/chZNb9kvtckTTDMs1 0OUk96BOdCJmOLMIZ563ujNxQ5eKRT5PkdeNX5VEVZtD83L8Nps00KnosNLTfbt5uAZDw0c1 BimgUDSbZ0whNQPzL+m/V2vb9mE+caQFVNdCun/dGup4wU8W5O/e5Cl7FLW9/koEWp0ZlyGo WRClM2OquYDEflhdRBhos1cRNlFBN7cYVUwZGKD+bF/rlxBHFb9J+htDMlWfhsBDyr9UWaBj LXvkQ1Q/oRPG3ChcLV6ZYm8Y+xzk/awS46+CqqLNIIVCnSUSONh1H4/DaJ39z+9+HXAbYlka P93jO7xUSdEUv0PIMSeHb9GgeBDKt8CKZP7HM2nkU3+j9JylVbMB+5NMV2SY/o/4b/MqQq9z jqsH5vi9vmra8WnOnO/2ddLczgidCFnbbir9ZA/XrPdc2JORjt9Y9ePmulJU9I+wMxoehLgp SzVtrlwkwak2hUq6GyiNhheVV8Ydc0l8S9mY3RyYAzANrpKSd/H0ZrzvqAfJdEPnNGPB9YtJ xXcU5XdUqZ8WX7c9i4DbJLwioVneV75zUiNJiepKnx3NZJpWwWDqJeucxrN5Rs+KHO9lfI/h Lm8iSLdY54IHDp5AOjsNfmA8lKWvFomotxUYXfmGNdoVXvJzJlLMA301/8+HNENI07Mxxycz AenPi0brujs/a4wqcfFtZmZnd3wT897Q05WNEjAzLOMLSKB1HGS8YxBd+epfD7mS2L//pu5V 9hV1/3RNP4mnk5AlphVSZJH7PsZyYP0hrl4yg9EIi36X26zAOk9HkjcjNh9iKJd45R45y20Y xur0ftHM+yrPMjFLgYgFDA9ZL7e6cBOyyjg1tVrEkDU/yQtwaGmV39VNByyiCBwCrt5HYcm4 OU5sv4t9A2NpUs2A+mCkxxr2TyAHl4YX4Ujk6MqMovhpw4o61NFOJLnGnDX5rOLYI5yKUUEG GKfq5fDoLV+/XD8VUQPO0LD59cAuqRWiit2lAcDA3+rhuv6guQG2UwN0DYvESVQ4BZ188NyH WlJMUdFKriE+gkwpclcXlKDHxNKKw2Z93fQlXoItjz9ZGu5WlPdKFYSPb62w3kY1GZHbx5n/ L2840T0YwbAJc3e8HM7Zh94lqbFU9d0yDznpOmmOMa0R78Bfjvvh/6VV1oi8hfIL5s4uxzam LNM4u11VKzcMBwQqY0dD62x9+wZaDKAFVx4bcBRxoE7NkCCR2jqwhmLEV67Re1VLf+T8UOYN d1nFvgSazuAjhSxvhIpLo9SBY8sh/M4xsswSpWyL048jravhD5IspXRyyvAuFEWU+heycYQF 4eAWA+BQ0qxhGRVkVDjtMNrGHS1SvhaaRze3NKayvQoFZUCgrs1LWU3j7+4lFSOEQ5d5xnPl hjyV6zX6O1DyIpXgIrnFJtYNTi0Md/eUOep8hi5ltZzMeP0LsbFsj0KpmndPwh5OaUbX/J1n ++vtOHb8VzkvrFsdUzkgLiESrd04PutUNptMs7YKGdQmQ2AUpTO5zoB42WJFoxbouhC58WIR xqKV+XoTIQ7A+xi/XxybzRSNz0/CK6tN6fpmn6bnsS2UxMY1VTKEcOj+XrXdlpkTy4vOaOvO j+s7rzqrppdoZ9XDRAJO+B+DtUqaBX/UK8hbJvquSPeEmCshUiYt6D/kQY7rwvGEWSADN2w9 KetqsISr/hukPqgIBBlX41OUtk/CXFgna8/e1Jb/dNq49x/4KjqMsxFWajqyLkN+sAx6H08T D7IfC0kBDmVsfFsb0Dn+Nq6NuuALrVmBzo6TwDFO2ubbjfwAo6caFekGuGM/F8uEgbeICqbx R3yN5E+0tVdAn2keArL2sGGvA==
  • Ironport-hdrordr: A9a23:aeCbz6/fKOQCUjLLpcVuk+DuI+orL9Y04lQ7vn2ZKCY7TiX8ra uTdZsgtCMc5Ax8ZJhfo6HiBEDwex3hHPdOiOF9AV7IZmnbUQWTXeNfxLfDhxv9Bib56ulR7q t4dbNiYeeAa2SS9fyKhTVRCLwbsb26GU2T9IDjJ/wBd2tXV50=
  • Ironport-phdr: A9a23:5cIh4hD4ZLrnbvjO6vGDUyQUKEkY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua8xygOXFtyAs7oE07OQ7/q7HzRYoN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB 89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9sI xi6twrcu8gZjYd/JKs91gbCrn9Ud+hL329lKkyfkhjm6sus4JJv9jlbtu48+cJHTaj0ZbkzQ 6ZCDDQhPWA15cnrugfGQACS+HYSUXgYnwRRDQTd4x70Qpn+si3htupgwyaaJtH5Tao1WTu58 ahmTgLjhTodOD449GHXjdFwjL5erRm8qRFz35LYbYeIP/d4Y6jTf84VRXBZU8hRSyNODY2yY ZYMAeQfOuhVtJPyq0cLrRakBQmgGOHixzlVjXH2x6061OEhHBnE0gM+G9IOtWnUrMnoP6oPS +C61q/IwijHb/hL3jr96JbHchQkofGRQbJ8a9HeyVM1GAPDk1qQrZfoPzyQ1uUCqWSb6fRvV f62hmMhtgp+rSShyN02hYnVmoIa1ErE9SNhzYooK9O1VEF1b9GrHpdMtCyXKZd7T8IgTm10u ys317MItJG0cSYKzJkq2h/SZv6EfoWM5h/uVfidLSt4iX97d7+ygQu5/0u4yuDkSMW4zUhGo jBbntXStH0BzQHf58qdRvdj4EutwTKC2gDJ5uxHJU04j7fXJpAuz7IqiJYevkLOFTLslkrsl q+ZbEAk9/Co6+v5ZrXmoYeRN4pzigHjLqQigMO/AeE3MwQUWWiU5/i82KXi/U3/XrpKkuU7n rfEvJzEP8gXuLC1Dg1P3oo+6RuzFSmq3MoAkXkCNl1FeRaHj4bzO1HJJfD1Ffe/jEqokDdu2 vDGIqftDY7XLnfZlrfuYLJ95lVTyAo2wtFT/ZRUBa8dIP7rXE/+r8TXDgUlPAys3+bnFNJ92 5sDVW6XGK+WLLvSsUOU5uIoO+SDeIgVuC/kJ/c54/7ukGQ2lEQGfaip2JsXcGq3Eu5nI0Wfe 3rsg80OHX0EvgokH6TWjwiJVicWbHKvVYo94Cs6AcSoF9TtXIeo1ZyM2CKmAtV8fGlABlTER Xflc4CZR7EGciuULstJnTkUE76sV9lyhlmVqAbmxu8/faLv8SoCuMe7vDAUz+jalBVosCdxE 9zYyWaGCWd9gmIPQTYymqF5u010jFmZguBjm/INM9tV6rtSVxsic4bGxrl6BtT3Rx6HdM2AT lqiatqjEXc3Q85ii8QWbRNFEs65xgvGwzLsBrYUk7KRA5lh8q/Y2mXtYcxnwnDK0IEuiklgR MZTZiW9nqAq0Q/VCsbSllmB0aancaNJxCnW6GKK1naDpmldVxNsF6rATTYZa1e+Qc3RwETEQ vfuDL0mNlEE0sueMu5Qbdavi1xaRfDlMdCYYmSrmm72CwzajrWLJJHnfWkQxkC/QAANjhwT8 HCaNAM/GjbpomTQCyZrHE7uZEWk+Pd3qXeyREs5hw+QaEgp272w8x8TzfuSLpFblrIJvCI8t 3N+Bl+709b+BN+Q4QxsYOQUYN8w5ktGyXOMrxZ0bdSrK6FvgEJbchwi5Rq0kU8tVcMZzo5w9 iBPrkI6M6+T3VJfeinN2JnxPueSMWzu5FW1bKWQ3FjC0dGQ86NJ6fIiqlylshv6cyhqu3hhz dRR1GORo5vQCw9HG5L8VkMq615wvbjcbi0V6IbEk3thLePn112Kk8JsH+Yjxhu6Kp1fPaeBC RO0GdcTAcSqAOMvix6vYw5Ob4UwvOYkesihcfWBwquiOu1tySmngWpw64d4ykuQ9iB4R4Ykx r49yuqDlkuCXjb41hK6t9zv3JpDbncUF3a+zi7tAMhQYLdzdMAFEzXmL8qyz9R4z5njPhwQv F6uA1YbxImjYxOUY1jV0ghAk0IavTSrlDC5wDp9jzwy5vDGhmqUmbukLUVBYDQDTXIqlVr2J Imok90WOSrgJxMkkheo/weyxqRWorh+M3iGRE5JeybsKGQxGqC0t7eEf4tO8MZy6H8RCr7jJ wnFDOSn8H54m2v5EmBTxS42bWSvs5T9xVlhjX6FaWx0pzzfcN1xwhHW4JrdQ+RQ13wIXnod6 3GfC16iMt2u5djRmY3Et7X0V2+lU4BPNyPxxIWMsAO04H0sBxCj1aPW+JWvAU0h3Cn32sM/H yXFqBPhfs/hza28PeZPcUx4Qlnx94Apf+M22pt1j5YW138Ag5yT9ndSimb/P+JQ3qfmZWYMT zoGkJbFpRLo00p5IjeV1pr0Az+Dl9B5aYDwMQZ0kmotqtpHA6CO4PlYkDtp9xCm+BnJb6E1n y9Bm6F3szhD3bxP5lZrlmLHWfgTBRUKYnCqzUzYqY348vkQPjjKE/D41VIiz4r4VvfY+F4aA SynPM54TWgqs41+KA6eiiSprNu+J5+JMJRL8UfJ9nWIx+lNdMBrz6BM33A4fzui+yVikbFzj AQyj87m+tLfeyMxuvvoWFkCaHX0f59Bqmur1PgD2J/Ljsb3Wc89f1dDFJrwEaDySW1U6q6hb V7RVmV78CjTGKKDT1/Frh448jSVScHtbCjfJWFFn4U4AkDDeQoF21hSBmxy25c9EkrCKNXJV kB/63hR41f5rkEJ0ed0L1zlVWyZog60azAyQZzZLRxM7wgE6V2HecqZpvl+GS1V5PjD5ESEN 3CbagJUDGoIRl3MBlbtOaOr7MXB9O7QD/S3Lv/Ha7GD4eJEUPLAyZWq24pgtzGCU6fHdmFlF OE+01FfUGpRHsPEh3MATjxRkS/RLoaaqBq65ixrv5W//fDsC2eNrcOED7pfN8kq+gjj2/7Zc bTK22AgdnACjMBppzeA0rUU0V8Mhjs7cjCsFe5FrivRVOfKnaQRCRcHaiR1Pc8O7qQm3wALN 9SI77G9nrN+kPMxDE9IEFL7ncT8L8wHJ2SgKBXNHk+NOLCuKjjbhcf6fenvLN8YxPURrBC2t TuBRgX7OS+fkjDySx21GeRLkT3dMxlO/oewblw+bAqrBMKjYRq9PthtiDQwyrBhnXLGO1kXN j1kel9MpLmdhcu9qvp6CypH42Y3dYFseg6c6PTEbJkTob1tDzgmz4qyD1w1zqsT6ixYFqUdp Q==
  • Ironport-sdr: 637541bf_PNxANW02bNOK58oS/D/2k4DlgtL9xcE44FZG4gY4uijgukE F8mTBvdhKiJ9bIFOdwPBe98oF1V+oLPRbiS3Xdw==
  • Ui-outboundreport: notjunk:1;M01:P0:fSaUzGuC6x4=;UFURl6A4DwP32gsLK0g35TO4Vsd dV+wGr+nOFHc/+K1Cz23jnMnWtvqgGrrVQzjNUrhCtahXLpUA73KKsbnFRAebZHt2iUGNSuJ0 aHk6A6cml8QZqLCd+euOZQPIMvUndQhj3lDXAMLKLNYdMCtxrraVnvqflh1WwpWtnZFBZOHEv WjHvN6qQVq6jBMjsbyc+FB+uosIxvDc8KJ/w+JcYoz7GdKFZtiNxr1p55OEsEeWmL894XiWtH j0UdkQt/E6lIA13utcU1zTibM3K5FFJgBgmqCKrzafaA3ByaSZUlAwQZVqZySMl/WQOm4B2/c oDmNbzNjbCvdq1aHQIet9GSl6L0wnzDIO2xTRw7iy4TXWYyuwPpyhSseKUJZI6lQurcqiZJsm gycY3szcK49RFZA50GVPuGAGDADSZIj1LRzXa7+j4PEwJf6df4XRsic+GeRIVtXzyqyfJGPft QdGWXUHDN1kly5B3t1FlzHVUweXWsdRpbq4s4FgSWsfgJoEhjXoIcSbamQgwGOknYZzkdBa0z gdveHrqYiLOLJgCzbH2c+wF1qY+V+e47bxIGmpOsOfFu29myf9JbrTh7B8olYilkrMFG7BJ1k ISL0fo9HayGa45YR8XYY7l2fRxK+MkGvCnpC2XP6Je/kVrbVcJncWCdZKMfjZG++aoN4QwH1K hpQEejw35WqvzIp8WHrI/94ZNZsE9cIre7l2k3adpGb9Ia5jEGjVF/C/0teIUPXixeniyFpe9 wKwM102EI68vBvFsftrmh0iaQBHjPmWYwvRva3tYZF0YgjIsT5XTAQMcXJsJuwYUU+7G9dpvF ZgwRMZpsCAH+Gu1hWyfj0GyZwMr3R3MpKA64AlmIY+drXGeFK/CPIncSaLflRmHuFMS7lJt9e k1/FopY/KhFX74oe3k/GVWLBDPUbwToy0JcdNWJi/+lPzMURltZ1gsbiDmwzbySMeVm/vRVna kuZ2vA==

I’d like to understand universes and universe polymorphism better. Therefore I have some questions:

The following term is well typed in coq:

Universe u.
Check forall A:Type@{u+1}, Type@{u}.

I.e. the argument type of a function type can live in a higher universe than the result type. If I try the same with an inductive type, I get an error.

Inductive lst (A: Type@{u+1}): Type@{u} :=
| nil: lst A
| cons: A -> lst A -> lst A.

Error: Universe inconsistency. Cannot enforce u = max(Set, u+1).

What is the theoretical background of this consistency error. The type of ‘lst’ is exactly the type I have checked above as well typed. I suspect that if it were well typed, then I could ‘hide’ an object from the universe ‘u+1’ in the list which resides in the universe ‘u’. Can anybody help to give a more precise explanation.

Regards
Helmut



Archive powered by MHonArc 2.6.19+.

Top of Page