{"entities":{"Q5056372":{"pageid":7085949,"ns":120,"title":"Item:Q5056372","lastrevid":91242023,"modified":"2026-06-04T22:38:24Z","type":"item","id":"Q5056372","labels":{"en":{"language":"en","value":"A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7628980"}},"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":"Q5056372$D85D8416-0EB6-4224-B553-8C2D80E602B3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a5c8d46860d8f30fd0bc85c3278d69e7a7ed674f","datavalue":{"value":{"text":"A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5056372$C11B28EC-4DE1-47BC-9B0F-37B7B0728CCF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b5d3f4822965856b350424603679ac76594cba4e","datavalue":{"value":"1505.03031","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056372$8EE12B69-7B6F-4F57-8B87-76EEC6E32C01","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"23bd1baa7c746f249e31b91b49f77e2df757498f","datavalue":{"value":"10.1145/3545115","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056372$622ED546-9BA2-4AB7-9FB2-92004CC68F0B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7101304f0a7b3ff1515b05fcde309f466c2b0aff","datavalue":{"value":{"entity-type":"item","numeric-id":5056371,"id":"Q5056371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$8DBA5BEE-1C7A-4555-8B82-0036B915BD4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8825a5f48e59e5b1e1510e59d52fce48da47c37b","datavalue":{"value":{"entity-type":"item","numeric-id":229739,"id":"Q229739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$86F12ABE-34A7-4CF8-A652-15F419B88814","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8820c971aa9efd594753d17fc620264198cc7b7f","datavalue":{"value":{"entity-type":"item","numeric-id":276264,"id":"Q276264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$9516B57F-9DDC-44AC-AB47-91C3B66A9489","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ae5381e7211b64f5f54296c18dfaf60be613ba86","datavalue":{"value":{"entity-type":"item","numeric-id":2946565,"id":"Q2946565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$27F7098A-42C0-453C-ACC4-B4D5B57DB061","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3ffbf7a5071d227412d80225c3d73ff104ccb41d","datavalue":{"value":{"time":"+2022-12-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5056372$ED82BB46-4A3B-40C0-87BB-5C9FC990E397","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5699268a307f98b3a0d3d22e1ed90e0c07a803ce","datavalue":{"value":"https://arxiv.org/abs/2206.02831","type":"string"},"datatype":"url"},"type":"statement","id":"Q5056372$938BDEE2-4628-42E1-88C4-D2A8C7434B15","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056372$FBEE1E21-9714-409A-ACC8-8F8C6AE973AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056372$A40F6A94-591E-429C-9C60-284DC1F5F21A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056372$223F9134-2513-4982-929F-6D08482D5870","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b71e15d3a17f1ae7a1c0239050ee3b6d6009a74c","datavalue":{"value":"18F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056372$071C534F-DF8E-4D96-9B49-B14910B91293","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dc9a4660f4497e5f1d0102b9481bc1c28d08d790","datavalue":{"value":"18N45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056372$1793F11D-139B-42E8-B9B5-EE152F078468","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"491fd28abfe1010b99bd908d377140611c92b283","datavalue":{"value":"7628980","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056372$D95FD845-ACB1-4DAA-89C4-371192CB6217","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5685485f4c27abda29cd481c0486a1adb54b3a91","datavalue":{"value":"category theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5056372$EF6CB0BC-C7E3-4089-9534-C78A1E3FFA3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5056372$18E66EBD-68AF-4DCD-A255-E3C3782F67C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2cb5e5f47853b7e8c42d45fe0bc97f54e0a0273d","datavalue":{"value":"contextual types","type":"string"},"datatype":"string"},"type":"statement","id":"Q5056372$70C58E0E-618C-4F95-BCE4-4352DF56301B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e22447b229c7a32c8d247e1ea4002861fd0fbd68","datavalue":{"value":"dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q5056372$B9934C1D-C05D-4C9D-8E0F-742039F1AB59","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6111489034643139b6436054b44d6250e7c1756c","datavalue":{"value":{"entity-type":"item","numeric-id":41339,"id":"Q41339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$BFD163F6-E714-4F64-A5A7-17F31739A6F1","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":"Q5056372$31195714-767A-4BBD-83EC-20CD7946FA9D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"43f2855a422537bb8ec286e6c0a317a791aa4b1a","datavalue":{"value":"W4298334981","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5056372$630A61C9-ED57-4B84-A696-755703E16193","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d26571693b6a8567e0a13f75c14953cf8fd0307e","datavalue":{"value":{"entity-type":"item","numeric-id":4281466,"id":"Q4281466"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$8CD267B4-ADEA-46CC-87F7-AB7EE040EC5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8a08c25c238f048b2e589efdf52c68fe9575e27c","datavalue":{"value":{"entity-type":"item","numeric-id":5220184,"id":"Q5220184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$A41C3540-D82F-43A0-9A56-E852CCEC2250","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dcbad67c372b78d4e89fdcc7d1bf3491d1269881","datavalue":{"value":{"entity-type":"item","numeric-id":5278407,"id":"Q5278407"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$BFCAE179-CDC2-4D79-AAF4-B868D7000CB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a765e855228292779b4203bd15443a2ad99c5c33","datavalue":{"value":{"entity-type":"item","numeric-id":5740406,"id":"Q5740406"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$8B625348-3662-46E1-B2F5-E09719B06B63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05618bc94dd537d3034b233a45ab1cb0906c9164","datavalue":{"value":{"entity-type":"item","numeric-id":3196622,"id":"Q3196622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$C5F488F6-2732-479E-B406-F8D45BC23646","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e544e438e6837b40684be8afb567ee872639a802","datavalue":{"value":{"entity-type":"item","numeric-id":4647575,"id":"Q4647575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$96920E03-CE03-421C-9E58-B0FF517D2104","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6095534c15ecadaae247856571b46e36c024f785","datavalue":{"value":{"entity-type":"item","numeric-id":1948284,"id":"Q1948284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$A4BDE218-5E28-4985-AEBD-D71B2115DB06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$5EEC6083-1B6D-4935-AE3D-9A766CEEBE8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"48a73b0bc94774198cd192d06e32293454cda383","datavalue":{"value":{"entity-type":"item","numeric-id":4225149,"id":"Q4225149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$0C733FFD-26ED-4F42-B779-5B5BF78F6EAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7212cbd21b262d16bcb7ffda7fc76bc50e112b40","datavalue":{"value":{"entity-type":"item","numeric-id":1208414,"id":"Q1208414"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$F5294C57-E78E-463A-92A1-D056EF4FEC34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77296dadb12c0ad0178e86e8a48ab1b9569a7901","datavalue":{"value":{"entity-type":"item","numeric-id":5039161,"id":"Q5039161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$F3A68CE0-065B-45A4-AB4C-351C3F24BAEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5441f18107b2a62e3594a6223410af9d2680a52b","datavalue":{"value":{"entity-type":"item","numeric-id":4993352,"id":"Q4993352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$5508C44D-0668-4534-81F2-F92328BF0AA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"45d621c08d6b6b648b2f02de3b6f7c65499ed1c5","datavalue":{"value":{"entity-type":"item","numeric-id":5277812,"id":"Q5277812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$146DB3DA-D187-4A54-BB80-A577EDD2BFE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88dd97334618a8abcb30d6b953aa7791488fcf62","datavalue":{"value":{"entity-type":"item","numeric-id":3189856,"id":"Q3189856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$5BD1B963-7C1C-494E-B11C-81A5300246B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db64b11464b9db48e2a389bd15fbba45af72595f","datavalue":{"value":{"entity-type":"item","numeric-id":5277845,"id":"Q5277845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$E97DE0EE-0973-4B01-B433-565745060C48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a90a510f27550100d45a2ef21dd83bca5c9e1966","datavalue":{"value":{"entity-type":"item","numeric-id":5747747,"id":"Q5747747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$A8254D65-C5F8-4492-8A6D-9358736E83F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37ac7bdfe4b7979285a1fd3ed4f6f2bcfdef1a58","datavalue":{"value":{"entity-type":"item","numeric-id":2200843,"id":"Q2200843"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$31925E01-32FA-4930-800B-9B34FF4C8472","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ff195701c0a951481f573bb7459fc69fbbed7fe9","datavalue":{"value":{"entity-type":"item","numeric-id":3786612,"id":"Q3786612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$7585E2D9-883A-47C8-83FF-ADFE9016F90C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d65f0b9793d4d69696724fba6626456d2e0d7a8a","datavalue":{"value":{"entity-type":"item","numeric-id":4640312,"id":"Q4640312"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5056372$AEAD7BDA-007C-416D-B34C-CFA8E80258F9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6ea27bdfec2ba133868d47d02bd5dc4fb070c1fe","datavalue":{"value":{"entity-type":"item","numeric-id":5752573,"id":"Q5752573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f713b037e5100e7cef2289f4c3c0ce9abdee54ad","datavalue":{"value":{"amount":"+0.74708092212677","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":"Q5056372$8DCF1EAD-3A84-4385-9598-302072059416","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e923df3bf9608d52d0b963a0f393bb430f783da4","datavalue":{"value":{"entity-type":"item","numeric-id":4225149,"id":"Q4225149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa07b9c7df92a19889b9959dc7814b4057a8fb1c","datavalue":{"value":{"amount":"+0.7467814087867737","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":"Q5056372$87DCED3E-F85C-4A10-905F-7AFB9E591D04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9e0526d2de6ea50db5116bfab90728355ff84bb1","datavalue":{"value":{"entity-type":"item","numeric-id":4961720,"id":"Q4961720"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa07b9c7df92a19889b9959dc7814b4057a8fb1c","datavalue":{"value":{"amount":"+0.7467814087867737","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":"Q5056372$F8237E44-29EB-4F38-B69B-469FCD8756EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"78bcc8aeb44460893848e59e91008ebee928816a","datavalue":{"value":{"entity-type":"item","numeric-id":4647575,"id":"Q4647575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1fcf4e347e9f5c38c644eeef9fc572d43d4a7272","datavalue":{"value":{"amount":"+0.7345806360244751","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":"Q5056372$62C4194E-7235-46B2-A295-9282FE759F1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"718ddf24aca222678c69eebcd41c61f56bc43624","datavalue":{"value":{"entity-type":"item","numeric-id":2253180,"id":"Q2253180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"650aa7ca23a29c1d2fa4f8bf6894f3cf1e57d581","datavalue":{"value":{"amount":"+0.7332517504692078","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":"Q5056372$FBC4D6D2-9888-42F5-9CAC-DA2F35249557","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Category_Theoretic_View_of_Contextual_Types:_From_Simple_Types_to_Dependent_Types"}}}}}