{"entities":{"Q1687770":{"pageid":1698511,"ns":120,"title":"Item:Q1687770","lastrevid":72000060,"modified":"2026-04-14T01:59:39Z","type":"item","id":"Q1687770","labels":{"en":{"language":"en","value":"Homotopy type theory in Lean"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6821869"}},"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":"Q1687770$F5A1BB09-50BD-4172-B5F4-DE836EEA671B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"614bee91fba3fcd5395aa5cde55a4a74337d2385","datavalue":{"value":{"text":"Homotopy type theory in Lean","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1687770$7B8E0042-5F8A-4EFD-9475-B24ED819C1EC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e4b66359714a8517fae43c4c72a766be553d49e1","datavalue":{"value":"1484.68319","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687770$E617BA6A-DCAE-4871-A76D-A9FF4A964141","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e2678f09b853692286aed3e37e57d593b9653b22","datavalue":{"value":"10.1007/978-3-319-66107-0_30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687770$BCD7E33E-5E8B-46B9-B206-6E2E1317DD73","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8dc9f7061148c184d156fce1cd302b98949f36de","datavalue":{"value":{"entity-type":"item","numeric-id":1687767,"id":"Q1687767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$62F42B96-691E-49EB-9C44-56D41E1C4879","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8ed91f18c49a16f542aacf01077ba8073712fd1e","datavalue":{"value":{"entity-type":"item","numeric-id":1687768,"id":"Q1687768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$A9DB7108-6838-47AC-8205-42EFEE96E2E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3e65812be4cd0be55e195a415cc5c72e9a1b4f46","datavalue":{"value":{"entity-type":"item","numeric-id":1687769,"id":"Q1687769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$1BB35CF3-8C12-494B-A188-0BED45770483","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7600255b4ee907c1b1dfbc5f62c7b1165ab1b6d0","datavalue":{"value":{"time":"+2018-01-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1687770$CE11F0C5-DDA6-44A1-A85A-348276B84466","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6ffc5c7d92ab51c20a8701e28b8f0644c49bfc1b","datavalue":{"value":"https://arxiv.org/abs/1704.06781","type":"string"},"datatype":"url"},"type":"statement","id":"Q1687770$F9B43C03-4D0C-4A4C-9C61-E16FD8190033","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687770$A6BFF53E-48A4-4BD2-9496-5C28ECB94B4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687770$9741A70D-7F03-4228-8EC9-E84620000E52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687770$AA512AB5-E330-4598-8A73-7398DF8AC908","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"957970e11422fbdef7ba9db5e2b00bc9584e024a","datavalue":{"value":"03G30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687770$776AC6CD-12D6-467C-89AC-111EDFB1896C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c9fdba58e5344e05288d09cbbfa64fc756b9e06c","datavalue":{"value":"55U40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687770$5E66D9F9-DA9C-4F77-8F86-A5E7451BA9B2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5909c9135b56adb8f04e2ff116e5a055f0fe8b36","datavalue":{"value":"6821869","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687770$1E7CC7E5-3DAE-49AE-9A37-C8AE9D5E3FD2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4ecd2d433c9f863c39fe5a1fa2de24434b6de0d","datavalue":{"value":"homotopy type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1687770$CAA0C16F-054E-4F4C-886D-6D5176FAD2D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3a96a510fd7a7846523150dd8bb125ef8f415fa","datavalue":{"value":"formalized mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1687770$90F0ACA2-07F3-424A-BAE5-46B299AECD7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4e8fd89fa28c0f6c3672ef10c3a2104586281edb","datavalue":{"value":"Lean","type":"string"},"datatype":"string"},"type":"statement","id":"Q1687770$C6ECAC95-CC25-4B97-BCF5-ECE750136335","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q1687770$03F26673-F9CE-4304-B590-ECEB72F14D67","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$20494701-0485-4A2A-A04A-C044A0C1E335","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b29eb58b948f9f996cbb5eae736ddbdaf0434b06","datavalue":{"value":{"entity-type":"item","numeric-id":34514,"id":"Q34514"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$8E312685-A300-4A42-81E9-52615C507796","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"39d1d25ae8c00cfad058b188db36fd61dac09925","datavalue":{"value":{"entity-type":"item","numeric-id":27041,"id":"Q27041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$BC34A6E8-A541-476B-8553-E1396BD27ABF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"723501325a83c597975238fada166e87a140940f","datavalue":{"value":{"entity-type":"item","numeric-id":27040,"id":"Q27040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$52AE1FA8-C8C9-4849-B019-D921889105CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b69ae52d53a05f3f4bf4d99cc0f83e03b73ae561","datavalue":{"value":{"entity-type":"item","numeric-id":27033,"id":"Q27033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$B5FB5762-77F9-46A2-854B-CDBA1E9B318E","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":"Q1687770$8569EB83-C5B3-4BF9-9AD9-BF558837D584","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7a3aa840bca23450e2329b2f2acf2ae44c0f39ca","datavalue":{"value":"W2608494448","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687770$B6EBE1E9-74F6-4BF8-81EC-EF25D44A38E8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7bcf33a5f992d181e7e78bbd8db6166cca7b5d2d","datavalue":{"value":{"entity-type":"item","numeric-id":5740648,"id":"Q5740648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$45090E3B-FB09-4597-9181-BA8B7BE8ED14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"264956f36982175453c070f2d8f8f60b18172d34","datavalue":{"value":{"entity-type":"item","numeric-id":5370902,"id":"Q5370902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$DAA63BD2-5993-4910-B919-9956DB5E50ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ecdac14a6d1f0425c3e321b73a201f6c904fd9b","datavalue":{"value":{"entity-type":"item","numeric-id":3598111,"id":"Q3598111"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$6C5E5EC2-5DDC-4386-BEDE-1D48C8276438","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aa12f01cd8d3619e98f3b449656daf677722f3f","datavalue":{"value":{"entity-type":"item","numeric-id":3121020,"id":"Q3121020"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$6D736DE5-C677-4088-B3C3-C15F48D15051","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4fd098ea4c8653eaec826e6d53d5157343c914f","datavalue":{"value":{"entity-type":"item","numeric-id":4580226,"id":"Q4580226"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$750A16FB-171A-441F-B9FC-8488827C7463","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0191c8d55bfb13f05e230de930538ee944fa6808","datavalue":{"value":{"entity-type":"item","numeric-id":1336951,"id":"Q1336951"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$00473F8F-8012-4BC1-93DA-9DB8130E9005","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"97aac3e9983bb038948e2fba3a98c71cc7d8d801","datavalue":{"value":{"entity-type":"item","numeric-id":5757920,"id":"Q5757920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$C5B9E012-980C-4F5F-8649-C6E837B2CA31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9c5d4cff434102bed227e3e021e251aecd1efd2","datavalue":{"value":{"entity-type":"item","numeric-id":4236885,"id":"Q4236885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$118E059A-72DB-49D8-9274-56312F33364C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0734eca8b44b27cc39aa495faea7cd858d51f4e1","datavalue":{"value":{"entity-type":"item","numeric-id":4247303,"id":"Q4247303"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$6366B3D6-6445-4A95-9657-6AF862D2CC02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a929ba3a3ad2ac94896c6474d644a301f4db300","datavalue":{"value":{"entity-type":"item","numeric-id":2031691,"id":"Q2031691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$D1DE26EB-1CEF-4DAA-B680-5094A26461BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f985e5e7c8a7887023cac4b87587be4a01f9a98","datavalue":{"value":{"entity-type":"item","numeric-id":4635794,"id":"Q4635794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$CB5AF433-5010-4785-A640-16D6211F766B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8242928870aab67343ad0152eb7ca8357168f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$E43E9DDD-94FC-4832-8BD6-2EA2BEB33129","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dcb51c6d7d97a019286f77f818933cb7ec1ae2a5","datavalue":{"value":{"entity-type":"item","numeric-id":5747673,"id":"Q5747673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$79F3EA2A-91BA-4CC5-8D8D-C30344E43123","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"890522dc4e3ecb3007fccfde8c53acf4163b6c1a","datavalue":{"value":{"entity-type":"item","numeric-id":5420262,"id":"Q5420262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687770$C25D05DA-98D5-4428-BD5C-1A4D14D06CE8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fa00a3b4a22b28151da0a7d0a412db455ab32f97","datavalue":{"value":{"entity-type":"item","numeric-id":4635794,"id":"Q4635794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ab78a129d49d6d76fbc5a3918da06bc6c0200665","datavalue":{"value":{"amount":"+0.7834986448287964","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":"Q1687770$68C2E331-A9DE-4724-95E7-E346CDF5200A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cfc9b9330d1f5c66f120be434f09d27704326a4c","datavalue":{"value":{"entity-type":"item","numeric-id":5740649,"id":"Q5740649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"941e746c8ef22edb4149b1f9ce0b9011ffad82b2","datavalue":{"value":{"amount":"+0.7729111313819885","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":"Q1687770$A60BE119-8BC7-4A0E-ABCA-741A2287C651","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a6e2fa711171a0ac47274caeed4c6108ca6294c1","datavalue":{"value":{"entity-type":"item","numeric-id":2933829,"id":"Q2933829"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78bc4663f63004b0ac600cd2dd06c64036c10117","datavalue":{"value":{"amount":"+0.7678936123847961","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":"Q1687770$B65B2D1C-BC37-44ED-B427-887710EEA0AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eceaac39afb5b5bf6071ca0d9d41e6a0697cba8e","datavalue":{"value":{"entity-type":"item","numeric-id":2986785,"id":"Q2986785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f4748ab469b373ef7e6ca9678a3226eec126ab6a","datavalue":{"value":{"amount":"+0.7653990983963013","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":"Q1687770$CECA7D02-4AD2-415B-8EA1-84F30782E1EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7be9f0bb3e23e9ef4020847e600b42c1a56f4949","datavalue":{"value":{"entity-type":"item","numeric-id":2938036,"id":"Q2938036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a51dee5819607412ecd42c125fa74f34e4307833","datavalue":{"value":{"amount":"+0.7652576565742493","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":"Q1687770$8E2AEF5E-4F9E-479E-95A2-3D6BBC45D78C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Homotopy type theory in Lean","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Homotopy_type_theory_in_Lean"}}}}}