{"entities":{"Q3075242":{"pageid":3085958,"ns":120,"title":"Item:Q3075242","lastrevid":51185618,"modified":"2026-01-17T03:23:22Z","type":"item","id":"Q3075242","labels":{"en":{"language":"en","value":"Sets in Coq, Coq in Sets"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5850138"}},"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":"Q3075242$3B848420-AF12-4C5F-AE60-EC6EE05F5743","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1e069fd6b059c11e4e94003e68df23ffa43ae1f0","datavalue":{"value":"1211.03023","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3075242$A627C6AC-7BCB-4A08-B71E-774C0DDB813C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b26e1c71794d37584d6b37be5173796d517f4644","datavalue":{"value":{"entity-type":"item","numeric-id":2754028,"id":"Q2754028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3075242$4EFF789A-258A-471D-847C-31AB19AD4695","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"76c08091180089def748f7e20273d2f981bdee68","datavalue":{"value":{"time":"+2011-02-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3075242$953C108E-D487-4C5D-82E6-BB4388ABF6D1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6734307e24b42c37a34ab9bcd1116029fa6db5a3","datavalue":{"value":"http://jfr.cib.unibo.it/article/view/1695","type":"string"},"datatype":"url"},"type":"statement","id":"Q3075242$EF3926C0-47E3-4CAB-B123-C888E3483B63","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3075242$F05D9FF4-5806-4BD9-8C35-1900782244FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7d6d1b45c606677a96fadd625efc72a171c20037","datavalue":{"value":"03E99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3075242$FB7D1C12-2DB9-470D-A76D-24F405F9F0D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3075242$6DF7CC41-584B-466B-87D4-FB68CBEF138E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"67fac79d81876ae2cbce6d86bf60ef6b9f2f6b81","datavalue":{"value":"5850138","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3075242$27223CD6-0D6C-494B-8365-3FAF8DD81B8D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3f11152d1931ca8ff860dd602781c6dc319db01d","datavalue":{"value":"set-theoretical models","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075242$43938492-F806-4F9E-8965-9C43CC13938C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4939422e7c810bdbc977f0068d541c8f8f5f2b33","datavalue":{"value":"Calculus of Inductive Constructions","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075242$B82F9443-F173-4A10-A8AD-9E193DF07545","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075242$27983029-B3D2-4CCE-9A5A-0D779600078A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"27053093570a92fff4e919f3d76d6d1ef93b0691","datavalue":{"value":"ZF","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075242$80335CE4-4DDD-46E9-93D7-3D74C2980672","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c0e1d3fd90144d6a82eeafe3352992a8ee833e42","datavalue":{"value":"inaccessible cardinals","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075242$B5A2880D-F4CC-4EEF-AA04-43459E333F9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c93acdee2b6d50e857d963ee94472bf230f7086a","datavalue":{"value":"HF","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075242$8F69B821-DB38-47A2-A4DA-AF6FD64DFAE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1e74996e55d08d5503c25807ec7e547c5c73d629","datavalue":{"value":"hereditarily finite sets","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075242$ED748D7D-59C8-478C-9A73-ABBBDC3FC26C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3a3e490a5573fdb0fc094d6fec9b93b8e47303ef","datavalue":{"value":"replacement axiom","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075242$63E26B30-E8E4-4FA9-A8C5-8F9360EB9171","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3075242$A8292698-22D8-4954-91DD-BAB34607922E","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":"Q3075242$32524F35-6C68-4678-9588-6CCB68C5ACFC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cdfd99d9c223eb0f3fc5e26de01873d6f72966b3","datavalue":{"value":{"entity-type":"item","numeric-id":4364399,"id":"Q4364399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"741e6b3ce885645d435bb07145e990e8618fa100","datavalue":{"value":{"amount":"+0.81035977602005","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":"Q3075242$21930816-78BE-4468-9A0C-EE88FB09C6CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"557fe52cb2d789e27e0fa76724761dbafd3d5f21","datavalue":{"value":{"entity-type":"item","numeric-id":4647584,"id":"Q4647584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c399a2ea0df464a163526bf1e6a96aabb86f5635","datavalue":{"value":{"amount":"+0.7818677425384521","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":"Q3075242$DF45DBA9-B1FF-4D6D-A8EF-993A69BC27BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f7da573bb2fe73b2a35b388b2a57bb39b406f9d0","datavalue":{"value":{"entity-type":"item","numeric-id":2829273,"id":"Q2829273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b3ccdfab4bc61faac1dce594e573529819207283","datavalue":{"value":{"amount":"+0.7791609764099121","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":"Q3075242$AB9A478B-5CD9-4916-B294-D8B18D95039F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b1e3fef7a91f717d982de5af60bbc76f7514a80","datavalue":{"value":{"entity-type":"item","numeric-id":4944846,"id":"Q4944846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"38fd2ff3da593c2debb0d6a6f11912b5e22457c3","datavalue":{"value":{"amount":"+0.774224042892456","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":"Q3075242$B151DACA-C99D-457E-9A34-5FA92C45BA3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d3aaa93dc04ba647ae61fca95e7a61b06376efcc","datavalue":{"value":{"entity-type":"item","numeric-id":2752532,"id":"Q2752532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"38fd2ff3da593c2debb0d6a6f11912b5e22457c3","datavalue":{"value":{"amount":"+0.774224042892456","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":"Q3075242$2A93F652-7B70-4E34-8BC5-1F2D9EE344D9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3075242","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3075242"}}}}}