{"entities":{"Q5887516":{"pageid":7917066,"ns":120,"title":"Item:Q5887516","lastrevid":47837788,"modified":"2026-01-02T20:26:02Z","type":"item","id":"Q5887516","labels":{"en":{"language":"en","value":"Inductively defined types in the Calculus of Constructions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7673902"}},"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":"Q5887516$9C439CA2-500A-41E0-B45A-2430D2C4C700","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"60c41d9e6aa967274d90518eaf4d0702b0ce51ec","datavalue":{"value":{"text":"Inductively defined types in the Calculus of Constructions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5887516$6A115748-F7A6-4722-AC65-17C531E2D281","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4bba7ec8861a8ed927cac8194bcfd558f8fc7d3b","datavalue":{"value":{"entity-type":"item","numeric-id":923885,"id":"Q923885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887516$2026242A-B8BD-4D3C-AF5B-DAFBE0BFE49D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1a33736bad804e6a530176061e0a43d6da42cd52","datavalue":{"value":{"entity-type":"item","numeric-id":476188,"id":"Q476188"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887516$7855DAEB-7F81-4DB3-A903-CF8922096B7D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887516$C0ED5106-224C-4D12-A971-7F02B9D47435","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7b4034943b182da069de8768d6fd2310f3e13487","datavalue":{"value":{"time":"+2023-04-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5887516$323FDA9C-1C79-4BF0-A1C7-F66C565E618A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5887516$A6170567-7E8C-4047-9C40-5B0070176CDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5887516$E5925763-6A36-48B9-8F36-77D15A1B8089","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f2ce43bbefea3ff41802d2068622bfb7df0d2a23","datavalue":{"value":"7673902","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5887516$573D9695-7788-4D82-BD20-53A9B55F1646","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ed28ff65c7143ccab364c3b93115be1e84f3431a","datavalue":{"value":"inductive type","type":"string"},"datatype":"string"},"type":"statement","id":"Q5887516$525B5697-5016-4BE5-AC41-F5E6E0A240E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bb82a6bb049eca827530aea8e4ff9bb2ba33b1cd","datavalue":{"value":"induction principle","type":"string"},"datatype":"string"},"type":"statement","id":"Q5887516$811B8C99-4A1F-426C-BAC0-DBD201587110","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"612beca1125760dfe6c2bb491db4749c8c456bbf","datavalue":{"value":"dependent pair","type":"string"},"datatype":"string"},"type":"statement","id":"Q5887516$52C19A26-1809-429D-ADFE-E8B643978580","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b876698d821b50cd7ba02ddb5424ed80f1905d8","datavalue":{"value":"lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q5887516$C4313119-00CA-4BD0-A570-B3E49D2FA85D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ba29bc695092e1012b615eb49ec43774f5b5c42a","datavalue":{"value":"inductive definition","type":"string"},"datatype":"string"},"type":"statement","id":"Q5887516$599F1928-99A2-4678-B19B-E80EF3EFAAD5","rank":"normal"}],"P1463":[{"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":"Q5887516$00982FD6-AB59-485D-B7B2-85C54A4A5509","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":"Q5887516$44E07412-5001-469D-BF5C-9EE829989980","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b7a94fa92f5ffde499c04f91d8a733b3fbcf7ff0","datavalue":{"value":"https://doi.org/10.1007/bfb0040259","type":"string"},"datatype":"url"},"type":"statement","id":"Q5887516$06416480-74B2-4C9E-800D-F850B2A421DE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"bb33ecd96a217162cbdc672c5e402fd6577815e4","datavalue":{"value":"W1852211073","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5887516$E60905A5-B124-4976-A7D6-089D1731507A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f32e072b62ae8a8febbed4970d6ec11bdb2a4f40","datavalue":{"value":{"entity-type":"item","numeric-id":4205074,"id":"Q4205074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887516$D40C991E-55C4-4DAC-8D24-79F2C5027391","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1463bc9145dde1ffd210d6809ebbc8df1d1a40d3","datavalue":{"value":{"entity-type":"item","numeric-id":1079357,"id":"Q1079357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887516$2570D868-07F2-4F8F-B5D6-E85B1413B9FE","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":"Q5887516$225B602C-5FEC-429F-A872-18C83C6B43EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887516$46549E5E-01B0-4622-90DB-46A3D863019C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70d5dcacdf82491509f047ffa7adf630e71ade90","datavalue":{"value":{"entity-type":"item","numeric-id":5667469,"id":"Q5667469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887516$D6C42F72-7F1E-40BC-A229-1962F9C8AA02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"53bcfabc22212d3db2a4fa41c3566844e5ecdda6","datavalue":{"value":{"entity-type":"item","numeric-id":3668859,"id":"Q3668859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887516$B50F53CA-1A3C-46BD-A6BB-DFFDBD6CC1EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5cb3fb1f5163c51d21987992526ad7f1b03bc113","datavalue":{"value":{"entity-type":"item","numeric-id":5625124,"id":"Q5625124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887516$A0D2E974-FE44-4C7A-9224-A1EE725798B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"76cd3a8ba48ee34d922f75db8eaff1b1a239078a","datavalue":{"value":{"entity-type":"item","numeric-id":3680264,"id":"Q3680264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887516$C84E6B90-9405-4377-9897-E39E85E826F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5abb06f902f9ed0fef96835b4d42cff003f2fab","datavalue":{"value":{"entity-type":"item","numeric-id":3677139,"id":"Q3677139"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887516$FFC88E7B-9D38-493B-8365-6F2F3856E209","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8bfb9e615f3ffab9adcf5cbeeaf565d3840d27b3","datavalue":{"value":"10.1007/BFB0040259","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5887516$F25AE2B8-D2B0-4E50-BE53-7A2D3E66071A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a299ada1677cb50f9badc2dfb747cce9998463ae","datavalue":{"value":{"entity-type":"item","numeric-id":3026376,"id":"Q3026376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"372200183d80f4b116c0a70cdae6ad4180a4721e","datavalue":{"value":{"amount":"+0.8334450721740723","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":"Q5887516$C26C65AA-72F3-4624-9690-CB35ED8F4C65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a60c342ca70b6a001e5ab65f9968fc1d0ec10393","datavalue":{"value":{"entity-type":"item","numeric-id":3805882,"id":"Q3805882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2892145b51785394da438bffb361b1ae1cf23f82","datavalue":{"value":{"amount":"+0.8145553469657898","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":"Q5887516$CA696803-2896-4967-B355-5E150A0AFCEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9c8377e506182330634e2c485af866ac2976d484","datavalue":{"value":{"entity-type":"item","numeric-id":4938611,"id":"Q4938611"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"388649e611a1cdc48e32f89213d56dee3a44bc65","datavalue":{"value":{"amount":"+0.8098244667053223","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":"Q5887516$D0A0663C-34D3-4CDA-9F4D-83232DF31700","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04fe00dd16f83f29e78f1f29866c0bdd4cd88a8b","datavalue":{"value":{"entity-type":"item","numeric-id":4457447,"id":"Q4457447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"72a7bab7956857d00cdf2cf59dfecb12d9852faa","datavalue":{"value":{"amount":"+0.8071190714836121","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":"Q5887516$FB5C086E-B252-400F-9414-E1C29B1B3936","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ce84887953fea95566a05af0f9ca26fd3351445","datavalue":{"value":{"entity-type":"item","numeric-id":1336951,"id":"Q1336951"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"81f295659da2cf77ee19eb2a5ea057e1d4c677e1","datavalue":{"value":{"amount":"+0.806888997554779","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":"Q5887516$A4457198-A72E-40D3-B980-BFDFE216D9F5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5887516","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5887516"}}}}}