{"entities":{"Q1177937":{"pageid":1188686,"ns":120,"title":"Item:Q1177937","lastrevid":66508869,"modified":"2026-04-12T10:32:10Z","type":"item","id":"Q1177937","labels":{"en":{"language":"en","value":"Type checking with universes"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 22508"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$4F5EB06D-6F01-4FE0-B943-81FBCEB27496","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5a2cc9fd320cc2f083ce6bf0aa083910fec8d09f","datavalue":{"value":{"text":"Type checking with universes","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1177937$C3FD846C-F433-4EAB-8D5F-EEA4D523D0A9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"07b090698a0aed9f5e074dfa3f8715af2f43ac03","datavalue":{"value":"0737.68013","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177937$A9F0A5C7-1DA1-47F0-A050-C9CD4DA357D0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ff9c9d2163aa238166e3923fb34e7b1ec6843f18","datavalue":{"value":"10.1016/0304-3975(90)90108-T","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177937$456738E5-B6BE-42D1-8903-8B05C4E2DE2F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c54adbdcdd8e58c67c424995e904ed84263f16dd","datavalue":{"value":{"entity-type":"item","numeric-id":724929,"id":"Q724929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$1C6332A9-7243-498F-B009-39DD16BBE466","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d3463bc6040ec10eedd8bc84c369dcec260e8f52","datavalue":{"value":{"entity-type":"item","numeric-id":688570,"id":"Q688570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$6ADC24CB-1075-4F7A-9D0A-F3793D75DC27","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$F1205EA4-1085-411A-9AE2-F704C3D152DB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1422b5e3113eee9dc98f0455d275631058399b8b","datavalue":{"value":{"time":"+1992-06-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1177937$B39A4A55-5BFC-41DF-932B-7B2DF45FCBA4","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"24e70340e23e0bc0c4da6904fa2cc8bbf4875868","datavalue":{"value":"The calculus of constructions (CC) was introduced by \\textit{T. Coquand} and \\textit{G. Huet} [Lect. Notes Comput. Sci. 203, 151-184 (1985; Zbl 0581.03007)]as a comprehensive basis for the formalization of constructive mathematics. The generalized calculus of constructions (\\(CC^ \\omega\\)) was introduced by \\textit{T. Coquand} [An analysis of Girard's paradox, Proc. Symp. on Logic in Computer Science (1986)]by extending the basic CC with a full cumulative hierarchy of type universes (a universe being a type that is closed under the type-forming operations of the calculus: the formation of products and strong sums indexed by a type of that universe level).]   The authors study the type checking and well-typedness problems for four variants of \\(CC^ \\omega\\). The paper is organized in seven sections, the first being an introduction. \\(CC^ \\omega\\) is presented in Section 2 and some of its important properties are recalled. An operational presentation of the calculus with the property that at ost one rule of inference applies to a term is given in Section 3. The significance of this presentation is that it provides a normal form for typing derivations that is exploited by the type synthesis algorithm. In Section 4 a schematic type synthesis algorithm is presented that given a valid context \\(\\Gamma\\) and a term \\(M\\), yields schematic description of the set of possible types for \\(M\\) with respect to \\(\\Gamma\\). It is also shown that the well-typedness and type checking problems for \\(CC^ \\omega\\) are effectively solved. These two problems are also studied in Section 5 for the extension of \\(CC^ \\omega\\) with an ``anonymous'' universe. In Section 6 the authors extend both the basic calculus and the calculus with anonymous universes to admit definitions in the form of \\(\\delta\\)- reductions. This extension leads to a notion of universe polimorphism analogous to the type polymorphism of \\(ML\\). Related research is discussed in the final section. It is also mentioned that \\textit{Z. Luo}, \\textit{R. Pollak} and \\textit{P. Taylor} [How to use lego: A preliminary user's manual, Technical Report LFCS-TN-27, Edinburg (1989)]\\ have implemented the algorithms of this paper in the Lego proof checker.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177937$A1FC3F42-A75A-43F2-A95E-C536B89332F8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177937$F9FD7C00-C81F-41F5-93B4-A12A1749DE61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8e3f40e3cc87753c4e0b7d7ce4bdc00805f626f","datavalue":{"value":"68N01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177937$D985C298-C155-4F1B-B9E5-0AD4413F81E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177937$8841AD97-6542-43F7-9A43-A13B84BD6C25","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"66053f3b19ec7113fd9d2312f0ebf2fc64f7c217","datavalue":{"value":"22508","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177937$65AE9551-4FDD-49D0-9646-54C186DA1F83","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aacdd9e6b1e081b5de4688ca768accb91a2c66bc","datavalue":{"value":"calculus of constructions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177937$9BC16AC7-051F-497B-93CD-9E92CB8B2B67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb8ff27bbbd9959dc9d199dde836f711285242b5","datavalue":{"value":"universes","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177937$FD9E1827-923C-4CA0-B247-056A92C41CBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ba5620c65b3b1616ab8ae31e5468b0e08272974","datavalue":{"value":"type checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177937$DA67BB6D-EDDC-4210-9594-083F461C124A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c01ae62e349131352babc696431ec8f00680fae4","datavalue":{"value":"well-typedness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177937$CF2B4005-0F95-479F-AA13-6E00E5356C17","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"6157837de11f2e28fe479554c99ef4c02d4ee00e","datavalue":{"value":{"entity-type":"item","numeric-id":172108,"id":"Q172108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$251C2ADC-D46D-40E2-B0DC-6E5E558AF77B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$EBC1CA0D-AD03-4BD5-BB60-24E1E213FEFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$399742C7-A9AC-4F28-983D-447F66988F03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$FA204B29-72B8-4C31-B469-828CDAC45285","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"55d1796d289926821ff098bc5ea53615142e836d","datavalue":{"value":{"entity-type":"item","numeric-id":21664,"id":"Q21664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$8D246386-96EC-438E-9BB4-4B110A6275D0","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$401C44AF-A997-4533-AB62-378DFBA81737","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"956c663a8c65ca7a493106b21f9b04a9a741383f","datavalue":{"value":{"entity-type":"item","numeric-id":1155602,"id":"Q1155602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$2AAC296A-6163-4F37-8298-384B1749B356","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4dae46d0a0bd58b96aa9d6a447fa758a54a7c4df","datavalue":{"value":{"entity-type":"item","numeric-id":1104071,"id":"Q1104071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$E3054D28-3ABB-44EA-8279-6BF9EAB1B267","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1448c91f0e7d84246a3f31dfa33129cf3bc2f12d","datavalue":{"value":{"entity-type":"item","numeric-id":4742765,"id":"Q4742765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$22425ECE-B9C2-45EA-AF4F-07D5599BEF9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d97a81fd7ad71815ea23de5bd9d2e05422152d02","datavalue":{"value":{"entity-type":"item","numeric-id":3673081,"id":"Q3673081"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$F609D3DC-725A-480C-B239-82A0A211AB08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29a1f1b83769fefedef94f42bd5222af507a657b","datavalue":{"value":{"entity-type":"item","numeric-id":3703866,"id":"Q3703866"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$C4790E65-C433-4EFB-B172-73817C2C8980","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$9D15FB7B-CEC3-4519-B03D-5A2A6B3E49A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77590281ffe78a0ca3be018504763d107cefa630","datavalue":{"value":{"entity-type":"item","numeric-id":4721631,"id":"Q4721631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$499779A5-7E2D-4814-9A53-9E8F3FEF1F93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c36e4ce17cede867a82574cebccb1c77ad33605d","datavalue":{"value":{"entity-type":"item","numeric-id":5752573,"id":"Q5752573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$82305224-288D-4835-8287-2DD4F3C89FEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b4fd1001f8f3efb16cb5718beff41343a27a9462","datavalue":{"value":{"entity-type":"item","numeric-id":790091,"id":"Q790091"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$F87B6BD7-DC9D-486F-BC15-5090081AEEC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7dd3b8732001a65e8422e49da191945e9664f035","datavalue":{"value":{"entity-type":"item","numeric-id":2639838,"id":"Q2639838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$88CAFF8E-7C21-4632-8ABB-D59295261C3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e04882dd0098e511c274267f86b00f5c3a4c9815","datavalue":{"value":{"entity-type":"item","numeric-id":3211296,"id":"Q3211296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$510ECF53-8C6E-41F2-A797-5904477F9627","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae94f828af67e50fecbc9e4b645ed6964977b9db","datavalue":{"value":{"entity-type":"item","numeric-id":4099613,"id":"Q4099613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$73EB6889-38CA-47AA-ACDB-76E8367151CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86f69e4e3c6e6db6273645f322c23116e1ad1c80","datavalue":{"value":{"entity-type":"item","numeric-id":3343983,"id":"Q3343983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$19FD8F21-C0CD-40C6-A720-7F4E154AFF1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b0ec3118c55b6f3ab232f29debefc8c9d383a9","datavalue":{"value":{"entity-type":"item","numeric-id":3688389,"id":"Q3688389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$AFEE5CEF-AF3E-4D5A-9588-5DD98DC37C13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"436d4ddccf9258c9f31fa193f202f774ffec18b8","datavalue":{"value":{"entity-type":"item","numeric-id":1250704,"id":"Q1250704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$156B52BE-1201-4740-ACB1-FDACB615046E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3ed33d75210f4b470fc995229f8d6e408696f04","datavalue":{"value":{"entity-type":"item","numeric-id":3922646,"id":"Q3922646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$6979D3EB-3F03-4E1E-916D-541607F31CBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84ad42be65af5dfa9e512f666229d02ed5041b60","datavalue":{"value":{"entity-type":"item","numeric-id":3856127,"id":"Q3856127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177937$1DCF76C1-0E2A-47BE-8A9D-F7C006BB8968","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"44c1ea6ed6b6f41cb87222030169530df3666d46","datavalue":{"value":"https://doi.org/10.1016/0304-3975(90)90108-t","type":"string"},"datatype":"url"},"type":"statement","id":"Q1177937$5C4081B3-B484-4890-BE55-2E7FEE8CA180","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b720adab3af1f241329333d408cec6b737a52990","datavalue":{"value":"W2014836228","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177937$8A01A0F6-0BE6-491F-B2A1-CD8D15A2A0FD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b038897e985a6185f1472ca068c61d8eab3426ce","datavalue":{"value":{"entity-type":"item","numeric-id":4484336,"id":"Q4484336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bcc01245a9fefd332d4668f3cbbac3496456efca","datavalue":{"value":{"amount":"+0.7965934872627258","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1177937$447F5A2E-A26D-42D0-963F-1B8DB662904D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"22aa479d92fa5eac512fc81e6ad7226cccf6f3e6","datavalue":{"value":{"entity-type":"item","numeric-id":3211296,"id":"Q3211296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e573436bcc16824ae2c59758b16f07d561ed889a","datavalue":{"value":{"amount":"+0.7900799512863159","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1177937$E4FFE6DA-6D3A-4E14-80DA-F9C3925B4309","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a21481f4370a1a9fd4c9ec8efcec8f450ae1ad60","datavalue":{"value":{"entity-type":"item","numeric-id":5277970,"id":"Q5277970"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"668ba043ea4932827bcc4665eea505aa06a21ff3","datavalue":{"value":{"amount":"+0.7875156402587891","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1177937$6124150A-FFF4-4392-9DD3-EA0AB167A097","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b04fc28ff935556a5c4174aab3a7627efd13f38b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e8926e82ebf7e444e1f10d6bfee2f04ed1f74b94","datavalue":{"value":{"amount":"+0.7821869254112244","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1177937$78DF56D1-9437-4B4C-BA74-6CBC5E5670C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f3c8d464e74f11f039e2de532d889ce898906e27","datavalue":{"value":{"entity-type":"item","numeric-id":2639838,"id":"Q2639838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b3c855cf131ace57c85687b3ad3993be400c1b1b","datavalue":{"value":{"amount":"+0.7661356329917908","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1177937$C5DF448C-7131-42E1-A3E5-4A800EFD2C4F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Type checking with universes","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Type_checking_with_universes"}}}}}