{"entities":{"Q6635505":{"pageid":14246657,"ns":120,"title":"Item:Q6635505","lastrevid":56084895,"modified":"2026-03-12T13:41:01Z","type":"item","id":"Q6635505","labels":{"en":{"language":"en","value":"Sharing proofs with predicative theories through universe-polymorphic elaboration"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7941267"}},"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":"Q6635505$8C7A8FC0-36D5-4E63-8D9C-BEC5A4BCAE1E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bcce13fb36be880b282cd8742ff247aa6bdf6bff","datavalue":{"value":{"text":"Sharing proofs with predicative theories through universe-polymorphic elaboration","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6635505$A3D814A7-5C4B-4101-934B-359D5D91989C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e7e3790ced80b833fdce050c7a25217abc7677cd","datavalue":{"value":{"entity-type":"item","numeric-id":6544120,"id":"Q6544120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$7677C88E-F44C-4B69-A1E4-A8F7A6E0F5F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8807e9b5ca6f3e9539fb2629b3f3fe474d0fb0ea","datavalue":{"value":{"entity-type":"item","numeric-id":235598,"id":"Q235598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$7EB5EC87-4A0E-4B99-B372-D24B50D81672","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$BF4FF1BF-75AA-45CA-AAB4-A7881739AEE5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"60fa3f87d97ee0a9686c2e5537009cd3455d3ea2","datavalue":{"value":{"time":"+2024-11-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":"Q6635505$EE6884B4-8280-4E97-9BDA-6F72CC25FC31","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6635505$CB20082D-E3B1-4651-B66E-8970CD91545C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"62a49b155c9af634e6c3562b1547da1f7c08791a","datavalue":{"value":"68-XX","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6635505$6E33DA51-1133-41DB-B244-1BEC01B9DB62","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ba64598ba3ea3729f746de6595938171be6204ab","datavalue":{"value":"7941267","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6635505$59C61E43-783F-4739-82B8-E2AE551E71FD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6635505$1BDA3126-244D-4CD4-8DDB-6991C41F4FFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f5795787683dc16a0e892761f65c085daecc3346","datavalue":{"value":"impredicativity","type":"string"},"datatype":"string"},"type":"statement","id":"Q6635505$1F1F57B1-5C37-43D7-A87C-1980E9C098EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1c34c2e8c5d0fb69f0d1e8e3e7dfa80780452cc0","datavalue":{"value":"predicativity","type":"string"},"datatype":"string"},"type":"statement","id":"Q6635505$9423C5BD-B1CC-4879-A128-10A0B3642CDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bf4383627d45fb5f4ba25831006036a0a071053b","datavalue":{"value":"proof translation","type":"string"},"datatype":"string"},"type":"statement","id":"Q6635505$2228846D-C17A-4767-920B-33126B998A33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c1159aa73cd8daf4c43043be733617a1e49169dd","datavalue":{"value":"universe polymorphism","type":"string"},"datatype":"string"},"type":"statement","id":"Q6635505$A327CF67-03F9-45C0-8830-9C3D3D186F7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f133d5c0825f61ea4d1285bd4c4e1695cb1ac9e7","datavalue":{"value":"universe-polymorphic elaboration","type":"string"},"datatype":"string"},"type":"statement","id":"Q6635505$D377E2DD-568B-40BD-A9A9-6ED89F413109","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"613ae915311035d09258a2411c846f9a80581351","datavalue":{"value":"unification for universe levels","type":"string"},"datatype":"string"},"type":"statement","id":"Q6635505$175AD105-4B9C-43BD-93F8-BB267B4A1359","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cb0249487b7eb1ecf24cddb1d300f9fa92e8fe1d","datavalue":{"value":"Agda","type":"string"},"datatype":"string"},"type":"statement","id":"Q6635505$35C0B053-7DBA-4A86-AC08-6135D384774D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d5c1e23f8e4f19689b4beca21c28903730de6f22","datavalue":{"value":"Dedukti","type":"string"},"datatype":"string"},"type":"statement","id":"Q6635505$EA87C846-7226-49A0-88AF-850698B4FC54","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":"Q6635505$0E560DF4-2945-4F5A-9386-339CFC3E0A32","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ea3b9dcc765a0506e851fe3e6b94c778ecda1a4","datavalue":{"value":{"entity-type":"item","numeric-id":2176677,"id":"Q2176677"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$03443A87-01EA-43D0-BAA4-6F6FA6DAC80E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"baa06e98dd2bbc2e50d854d66656326eb2c6a08d","datavalue":{"value":{"entity-type":"item","numeric-id":5195248,"id":"Q5195248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$B47AA9C6-E46E-4551-A23A-FFB3C2845525","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f1e9f15aec2253c6d8e4742c7e3c60b7a3917a6","datavalue":{"value":{"entity-type":"item","numeric-id":1111775,"id":"Q1111775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$BAAEF988-FBA5-4307-99BF-3F7504408C0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"96e079aa7338cd7372f634e3c1da203aade6413c","datavalue":{"value":{"entity-type":"item","numeric-id":6643043,"id":"Q6643043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$0DA0A451-8437-4E29-9A06-B7908DA36D25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"23dfe1f5a7256dcdfce4b4f09ca6e1a62bbeb6b7","datavalue":{"value":{"entity-type":"item","numeric-id":5883738,"id":"Q5883738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$CD130652-9485-41D2-B672-AE155CEC93CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4cc846e4285dd73747ab89d2dd8d67254289009","datavalue":{"value":{"entity-type":"item","numeric-id":4799892,"id":"Q4799892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$796BBEDB-E76E-47AA-9E1E-6AA55BE8ED3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b169c0923be721d2a0aaf8231f0f0f40317694ae","datavalue":{"value":{"entity-type":"item","numeric-id":4447247,"id":"Q4447247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$D94A9011-D441-4C94-B5AE-4B5C3BE3B3A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e6aa3e3851825ce947035770e997710fa99c398","datavalue":{"value":{"entity-type":"item","numeric-id":4657751,"id":"Q4657751"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$D391640E-4504-4E4A-900D-69CE5A788CA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9978b7c4cc188e85861053a3341ddd6c9e61540","datavalue":{"value":{"entity-type":"item","numeric-id":6544119,"id":"Q6544119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$87F64676-13C3-431C-8630-E180C99CD23E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"686d8c1af79a48830313f258a972641c870a4f2f","datavalue":{"value":{"entity-type":"item","numeric-id":2631965,"id":"Q2631965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$033210CB-8989-4EAD-BBED-BFB46144E19A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34b87924f23be2e9cf6d7b6faa675b811f5a3d7c","datavalue":{"value":{"entity-type":"item","numeric-id":3612625,"id":"Q3612625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$EF96DA5F-ED86-49FF-B500-26BFB06699F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5bb564ebccf41e8ed52c97939f8eed6f8781aa4f","datavalue":{"value":{"entity-type":"item","numeric-id":4281470,"id":"Q4281470"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$7B440CCE-18AD-4F24-8ABD-F05C6D72FF77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b853766179e337a7e1beeb8fa93252a8e59c518f","datavalue":{"value":{"entity-type":"item","numeric-id":6610621,"id":"Q6610621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$41D2B2D0-7998-461F-82FF-4D67A0FD6786","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3994f2ce4ebe41fe0dc4606342e21a9dcadf705b","datavalue":{"value":{"entity-type":"item","numeric-id":6544121,"id":"Q6544121"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$EF06507C-BAED-419D-A0B7-F8BB4418932C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca9b21e92d1e385b1aa703cba49bf61d8d21f05a","datavalue":{"value":{"entity-type":"item","numeric-id":1177937,"id":"Q1177937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$D8F4E890-77AE-481E-9C06-5588C4FC8A45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"599c5dbf52817fbbe5f2f15e33a96dc6ac97514e","datavalue":{"value":{"entity-type":"item","numeric-id":3908463,"id":"Q3908463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$55F06B46-13D6-45A5-ACC1-B953CEA85F77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba1eb42d9c5348c57088bd4b838a7a5b42853faa","datavalue":{"value":{"entity-type":"item","numeric-id":1314356,"id":"Q1314356"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$40BABEB2-5DE1-4BD6-8986-72A163AFE3D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3671c04a28b3c6321772a8c859c51ac112c8b4d","datavalue":{"value":{"entity-type":"item","numeric-id":1127334,"id":"Q1127334"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$70A11726-AEEA-4A87-9562-A06985EBA380","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"caf63ddf3ade55d0065bf270ea1718adb7e9fbdb","datavalue":{"value":{"entity-type":"item","numeric-id":4246950,"id":"Q4246950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$CAC31A7A-CB82-4D72-915C-6DF6D547153B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca5666f921e01dd97435dae76a72d1660a28c596","datavalue":{"value":{"entity-type":"item","numeric-id":2879272,"id":"Q2879272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$FF042398-811C-46B3-81B5-CB17831BE8A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0b3f657f0eb24207aa576cf8fba987dfefd9f923","datavalue":{"value":{"entity-type":"item","numeric-id":5372007,"id":"Q5372007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$63339189-6ADA-4E27-86B6-90A87AEE8010","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2b1206124823be24b7ecdfbab28a76561450dd06","datavalue":{"value":"10.46298/LMCS-20(3:23)2024","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6635505$33E5FB2A-39E9-4462-90ED-38136201F66F","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6635505$4A6E2465-566E-47AC-942A-2455A7A89F8F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6635505","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6635505"}}}}}