{"entities":{"Q3094177":{"pageid":3104892,"ns":120,"title":"Item:Q3094177","lastrevid":86464478,"modified":"2026-06-03T21:56:33Z","type":"item","id":"Q3094177","labels":{"en":{"language":"en","value":"Type classes for mathematics in type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5961498"}},"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":"Q3094177$37B220FC-7841-46FF-AE6E-8EE9D336A55F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bcc62964960584c56e09121cc8629178e05e79fd","datavalue":{"value":{"text":"Type classes for mathematics in type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3094177$4B48F2DA-1454-4710-8483-6327FB928B6A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8f3e0db942316126f320f0e2ba5eb5108a9ef66f","datavalue":{"value":"1223.68105","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3094177$DD4B2AE4-B43C-4963-A92E-DFEED8603107","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0f54f799d6b128211c9558a3cde68da75fd898f9","datavalue":{"value":"10.1017/S0960129511000119","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3094177$FAB37DB9-FB66-4A17-8A33-15AFF642D961","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"603d1427f1b21e289d7f29d1759e5e0b15783239","datavalue":{"value":{"entity-type":"item","numeric-id":185814,"id":"Q185814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$D7C931A8-E669-4FFB-9137-FCA5CACB1ADB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5803880d1a3015657cb8cbe67e318be0131f8b6a","datavalue":{"value":{"entity-type":"item","numeric-id":3094176,"id":"Q3094176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$A9A32654-8F10-4B21-A5A4-20FF388A5EF5","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a53527e88e2413966f3c8ce14c92b878c452756d","datavalue":{"value":{"entity-type":"item","numeric-id":2709784,"id":"Q2709784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$4644A817-81EF-421D-BB38-B23313243DB0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5412e51208588a3303ff1411a4274ccfb0b7d7d6","datavalue":{"value":{"time":"+2011-10-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3094177$5AB8D643-4217-44C9-84A4-21070CCBE172","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3094177$395A2214-B6F8-4F80-81B7-4760BD48A924","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3094177$FF28C779-6ECD-4A66-8A56-7C409E91908F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4663a3b8587848a7294cb7ec4d70693f6083f67b","datavalue":{"value":"5961498","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3094177$DC8AB957-2FE5-43EC-994D-F27CA1E80EE5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3a96a510fd7a7846523150dd8bb125ef8f415fa","datavalue":{"value":"formalized mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q3094177$02CBC165-35D6-4266-AE6D-ABA8566A6CF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2420d9f7e2e7b5872f2cffb9d8f9912c6071b0d5","datavalue":{"value":"first-class type classes","type":"string"},"datatype":"string"},"type":"statement","id":"Q3094177$4BCF43A1-48C5-4C28-9D86-CD716AF6DC87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e8680952b101740d2661a75b00e2003d484a3f5f","datavalue":{"value":"algebraic hierarchy","type":"string"},"datatype":"string"},"type":"statement","id":"Q3094177$B99771E3-5AED-4A29-A4F7-263B77964006","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3094177$312B66DF-187B-4157-BF20-AB1D96FFDFD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q3094177$6BFD5505-B709-4D87-A2EE-DBBFEE64BFAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9d206c07deec764cd48c8bb9e8aa4b735e8f78cd","datavalue":{"value":"bundling","type":"string"},"datatype":"string"},"type":"statement","id":"Q3094177$70B83E80-7E9A-4931-90F9-CCF31CCD0DE9","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9ba88ec88a3e0f66013f52903eb001c6391d509c","datavalue":{"value":{"entity-type":"item","numeric-id":12835,"id":"Q12835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$1E2A8DEB-1B96-4DE5-BC1A-7223BD026294","rank":"normal"},{"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":"Q3094177$F643EB0B-8528-4526-BF17-CA945521B4AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"09d0e89c904b4336aa9c702b0f719264b030c9d8","datavalue":{"value":{"entity-type":"item","numeric-id":14086,"id":"Q14086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$A7C77132-6E12-43AB-9494-7E2C0B46AECF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7bb1c7eafdbb853d5fe04051d89b8463fa8b943a","datavalue":{"value":{"entity-type":"item","numeric-id":18827,"id":"Q18827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$874EB3BE-7ADC-4C03-806A-E700C68D8C7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e262f47aa23786f0d5ca3c491b5060c53e80792f","datavalue":{"value":{"entity-type":"item","numeric-id":18274,"id":"Q18274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$06DDB527-3521-46B3-884B-B23DB9AD79E1","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":"Q3094177$EFC49FCC-0C71-4F7E-8903-69676D18AD76","rank":"normal"}],"P223":[{"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":"Q3094177$5AB247A5-7465-4811-B859-E83E209E931C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$6DC83B48-5CE2-422B-B3E8-030ADED155B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79aa05cbdf7e9c30715a43e649084cfac28e9645","datavalue":{"value":{"entity-type":"item","numeric-id":4457833,"id":"Q4457833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$1CA1429D-9FC5-4F3A-98C0-F1AF534F8A40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c8847fc96bd6cc15667c599e80d53cc2bce3050","datavalue":{"value":{"entity-type":"item","numeric-id":2462635,"id":"Q2462635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$B997A70B-CF99-465D-A807-C982D20468E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5f64d57050206512889a218305d67a8f65e3f09","datavalue":{"value":{"entity-type":"item","numeric-id":3183522,"id":"Q3183522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$D63BDB5F-275B-4CB5-B771-5C53E8747CFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f788536331bb87ba4e75963340b885a6c5e47c5c","datavalue":{"value":{"entity-type":"item","numeric-id":5747643,"id":"Q5747643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$972E317C-13C4-4065-B585-95ECC3B22C99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4219b9e9a34aa8918de2de1511c7b08fa278e0a0","datavalue":{"value":{"entity-type":"item","numeric-id":866572,"id":"Q866572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$BD226CB5-E575-4FD2-975E-A4D2A7EF52B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60b8958c11cf12e9828f35bf950395907ec01462","datavalue":{"value":{"entity-type":"item","numeric-id":987984,"id":"Q987984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$7205714D-219D-4DAC-A4BD-286EB02CBF72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a15f025b82e462b08b6da310a0699c520bda9047","datavalue":{"value":{"entity-type":"item","numeric-id":3543662,"id":"Q3543662"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$F30C954B-967F-4527-8CA1-7C7B691F4DF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ff7181965704e473c064c7d95f9f7f0b397f93f","datavalue":{"value":{"entity-type":"item","numeric-id":3543665,"id":"Q3543665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$C4DC1A91-1304-4063-A14C-FC4572FD8396","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aa63f2e41ff19c6a30515e22d87f3f398a58a326","datavalue":{"value":{"entity-type":"item","numeric-id":1895401,"id":"Q1895401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$52DCCA08-AD8B-47EC-9BDB-0891BC624F04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29209482615350601b1ac00dbba8b8d6f75d6148","datavalue":{"value":{"entity-type":"item","numeric-id":3499757,"id":"Q3499757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$02BDD0A3-5891-4AED-A48A-DCA07A0D13B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a55620229a723772a6f28df349b35435b565020f","datavalue":{"value":{"entity-type":"item","numeric-id":699688,"id":"Q699688"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$46435827-29D4-46DB-86FD-4C756429CAE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"95fcaa03a7e112faaaebcb4cc431e02a031d7272","datavalue":{"value":{"entity-type":"item","numeric-id":1404425,"id":"Q1404425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$D0D060C8-6BD3-4839-B6EC-32B27799EF2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8c6dee845aa2fb3e3b96fd0f5f996675d409056","datavalue":{"value":{"entity-type":"item","numeric-id":3183538,"id":"Q3183538"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3094177$B410FE23-6D64-44A8-9167-1C068C503206","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c420807eefdb7973754738efa21cb8294924c459","datavalue":{"value":"https://doi.org/10.1017/s0960129511000119","type":"string"},"datatype":"url"},"type":"statement","id":"Q3094177$64483CE6-4B4E-4477-BDC8-B93F4AB70127","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f930869bca58e75062ddd11e20fdee2729aa2ab0","datavalue":{"value":"W2164688709","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3094177$3AFACED5-D83F-4DB8-A256-414D14051F59","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f283ce1b7bb222e202a6acf28a6a844d9018de04","datavalue":{"value":{"entity-type":"item","numeric-id":5747673,"id":"Q5747673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aad03d2810f943bfc10432ba35034ba594126f73","datavalue":{"value":{"amount":"+0.8744596838951111","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":"Q3094177$35B9AC20-4E2A-48F9-A1C9-1EFE50646C99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c00be21f476e85b1dd13b11a94c13f75ce187fdf","datavalue":{"value":{"entity-type":"item","numeric-id":3543665,"id":"Q3543665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"18a604d9038809bdd13de7d56f922fd05c288f80","datavalue":{"value":{"amount":"+0.8014445900917053","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":"Q3094177$191D18E4-DEDD-4920-90D0-87AE1CE33A80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"662db280aaa7eeb61c216bc5c52425ad27aeec81","datavalue":{"value":{"entity-type":"item","numeric-id":3612442,"id":"Q3612442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a1aa470a7763cd6bf914d9baa4048e6c00c6055f","datavalue":{"value":{"amount":"+0.7570943832397461","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":"Q3094177$7A4A6A40-B840-49F2-AFB2-19D38F997861","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"07a314e3e300ecb5f9a5ea5dd7518452d5ba23be","datavalue":{"value":{"entity-type":"item","numeric-id":3499757,"id":"Q3499757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ccb2ac200855283184e3ae725f304bf0af508862","datavalue":{"value":{"amount":"+0.7476028203964233","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":"Q3094177$2B5A7036-0E03-4A6B-997F-EB4D9FACF93C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ebdf17415979c5a0a5109871e6e533a5e657dab8","datavalue":{"value":{"entity-type":"item","numeric-id":5327346,"id":"Q5327346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"817b0ef70b7b61b5a18ecf5b6953131963cf62a4","datavalue":{"value":{"amount":"+0.7348445057868958","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":"Q3094177$8D7F3B46-3477-4C36-A036-32E3CD19DFF5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Type classes for mathematics in type theory","badges":[]}}}}}