{"entities":{"Q4993350":{"pageid":7022927,"ns":120,"title":"Item:Q4993350","lastrevid":54021848,"modified":"2026-01-26T02:51:25Z","type":"item","id":"Q4993350","labels":{"en":{"language":"en","value":"A syntax for higher inductive-inductive types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7359416"}},"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":"Q4993350$54F930F8-DC0B-4A23-8FD9-25D786941BA3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"716a5b7e2d5a5cf78b903769fb4d55e6afe74b63","datavalue":{"value":"1462.68022","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993350$E12CA1C9-0F83-49AC-9B13-1004E31DA03C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a7cbc48b481a6b830ab14eacad20738b43bab2e0","datavalue":{"value":{"entity-type":"item","numeric-id":2176676,"id":"Q2176676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$16CB49C4-1BAC-45A9-B7E6-2CAE76670555","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"08ce0e0cdedd491f2be40b586710d257b049396c","datavalue":{"value":{"entity-type":"item","numeric-id":421064,"id":"Q421064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$77D06718-53CA-4C21-93EB-71C63BBC1ADA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"19226134edc7102663c447aa756e808a7a8d2948","datavalue":{"value":{"time":"+2021-06-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4993350$EFB67DC5-41BB-4B99-A48C-9987BA87083C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993350$693854C2-0741-4F51-A583-E927EFD9EB73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993350$2D5E6ED9-918E-452E-8658-6D49CAFB6F3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"72047dd175f2df177aa1ddf4f7ca150e0c1e70c2","datavalue":{"value":"55U35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993350$4551B649-ECFD-403B-8017-457ED6236E61","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f4c098a83426391b829d295931764a215e6399e4","datavalue":{"value":"7359416","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993350$8678662A-2FD4-40F1-9C09-C7025B84AF01","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4ecd2d433c9f863c39fe5a1fa2de24434b6de0d","datavalue":{"value":"homotopy type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q4993350$3596EDF3-1B20-4403-AB60-42BB8F196EA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6f9664d8f5f982ad8c7114c1fd4c8edf6f81ead4","datavalue":{"value":"inductive-inductive types","type":"string"},"datatype":"string"},"type":"statement","id":"Q4993350$36D7D912-F22E-40EB-AFF6-F63AE179BFC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6886acc9bb720e6ad7ca13e49d3bd87570dc950","datavalue":{"value":"higher inductive types","type":"string"},"datatype":"string"},"type":"statement","id":"Q4993350$E0E6388F-1F28-47B0-A516-7369F29A9E8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"044652d5f26029074bb40747b62382dcce60f703","datavalue":{"value":"quotient inductive types","type":"string"},"datatype":"string"},"type":"statement","id":"Q4993350$272E5640-FA79-4320-8354-EFF388D31383","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"02e2bd1176be2ca24a8b368e42bc8812510b3ef7","datavalue":{"value":"logical relations","type":"string"},"datatype":"string"},"type":"statement","id":"Q4993350$52A36C2D-97FF-4DEE-8272-B5E198129920","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"067e00213990a6f2431e78667be3f10443c92f4f","datavalue":{"value":{"entity-type":"item","numeric-id":16052,"id":"Q16052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$CC5DB5B2-A456-43D8-936C-853BA88BF57C","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":"Q4993350$3D2DC812-F208-4DF8-BDFD-B484AB934887","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d8ce1ab7cbc344458f6c5f69920718926ea1d05","datavalue":{"value":{"entity-type":"item","numeric-id":2566024,"id":"Q2566024"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$AE47F622-626A-4280-BC2E-7555D4FE74BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d10e46b1e0cfb4bb12a7ff92b5fe74e9b2afacba","datavalue":{"value":{"entity-type":"item","numeric-id":1652995,"id":"Q1652995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$63D1A604-7986-4778-AF9A-670B691A19B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34a544eff9bd65de4592fa7b247517554bcdddd5","datavalue":{"value":{"entity-type":"item","numeric-id":2828239,"id":"Q2828239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$E562E0B7-0421-4189-BB24-C354CF8DD160","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e739d4e358cfe0bff089251671b51e298177305f","datavalue":{"value":{"entity-type":"item","numeric-id":5408445,"id":"Q5408445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$ED128A0D-3B0F-4C3C-99B6-A5C9DCD3F832","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb8b75f0e49d9cef046d4a84d906b1de8953a19f","datavalue":{"value":{"entity-type":"item","numeric-id":4635888,"id":"Q4635888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$F22CA233-803A-4363-ABC5-91BAF375D082","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e154aa9118f1cfec335fe4b3f0ee878903e59e9e","datavalue":{"value":{"entity-type":"item","numeric-id":5176953,"id":"Q5176953"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$6EE88A21-96A9-4692-8292-E2134B4C4D44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"95fab8824d82d4ca6fefb7d000ea15dc3e260bd1","datavalue":{"value":{"entity-type":"item","numeric-id":2844694,"id":"Q2844694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$4888CCA0-91A4-4384-AA5F-AF920E61C674","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":"Q4993350$FBD829E7-59BF-47D4-942C-A4EF47B5FC16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"364525b70d80e5ad032dd4bcb752b39f36195669","datavalue":{"value":{"entity-type":"item","numeric-id":4508246,"id":"Q4508246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$8B98EE64-1390-49C5-8074-C4D9EB5A1A27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"670b0cf2adae33c7590dfeacbd93de769c0fc86c","datavalue":{"value":{"entity-type":"item","numeric-id":2130587,"id":"Q2130587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$C5953B5E-8CD7-4AC8-B797-049378BA4E60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5765b1c70da77537c6e225225ff527afc50bcc4e","datavalue":{"value":{"entity-type":"item","numeric-id":4263867,"id":"Q4263867"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$2A40834A-8B82-46C3-BA6C-7CC659491226","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"129baccb9ec914278b9a5678f35aa75814ad23bb","datavalue":{"value":{"entity-type":"item","numeric-id":4635920,"id":"Q4635920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$D32C5243-D097-408C-AC73-37A4874AE282","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"062480f97a81d260cf760081be6431a87b424b78","datavalue":{"value":{"entity-type":"item","numeric-id":283766,"id":"Q283766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$DE921F13-AF83-4DA3-9C65-0CEA0A2EB202","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9579a4ebc8fc362938d3ee4c1626b4dbb8862f2","datavalue":{"value":{"entity-type":"item","numeric-id":4281483,"id":"Q4281483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$03230531-D801-4AB9-9FC8-DB7046DA0001","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":"Q4993350$31A67F3F-8059-47E2-9548-728DB6B1E74B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"784f038b41cf6a95136e868957e992da42f29715","datavalue":{"value":{"entity-type":"item","numeric-id":2819787,"id":"Q2819787"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993350$C3ABC32E-F94B-4C52-929E-DD73E15E644A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d81087d7ca791bb5fbaaa3f6676ce405b101fd19","datavalue":{"value":"https://drops.dagstuhl.de/opus/volltexte/2018/9190/pdf/LIPIcs-FSCD-2018-20.pdf/","type":"string"},"datatype":"url"},"type":"statement","id":"Q4993350$F3F3F106-D302-4BF5-BA2B-C47C1DA27BEB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"867b1b8a14bc44fa22163eebcb6fb5a12a332d50","datavalue":{"value":"W2885792094","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993350$0F4CED5C-6819-4F1E-B6B8-AEA538939DCA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fb07cd1e405a074983e452fa35c050a4e476547c","datavalue":{"value":{"text":"A Syntax for Higher Inductive-Inductive Types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4993350$79C82178-C1D0-430B-B82C-D293C8C67939","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1261138ceceb9925fd4b04090ef78e14c8d58564","datavalue":{"value":"10.4230/LIPICS.FSCD.2018.20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993350$588822B9-D696-4DAA-9993-A7D22F29B7EB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aac67a273a6ae0afefb612f1d3784f5bcff8aa55","datavalue":{"value":{"entity-type":"item","numeric-id":1652995,"id":"Q1652995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"04174ecbe73449ae791beacc01f920f45abd8285","datavalue":{"value":{"amount":"+0.8342142105102539","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":"Q4993350$815BF2F7-2529-4FA2-8C8B-14591A5432AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e001309006a43b2c682ba66be212a39e7be2b26a","datavalue":{"value":{"entity-type":"item","numeric-id":4958656,"id":"Q4958656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1065cd2f98642c3837ae8f114cbeebf218b20897","datavalue":{"value":{"amount":"+0.7611356377601624","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":"Q4993350$7AC47CFB-11EB-4690-A2F0-8EEC2ADA7C33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7fef228a353cc07d2c1654ce9e3f29b1224dff3b","datavalue":{"value":{"entity-type":"item","numeric-id":3586059,"id":"Q3586059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cf914a8d0a355799daacaa047dcba20975862215","datavalue":{"value":{"amount":"+0.7493305206298828","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":"Q4993350$F7111427-8A23-4A27-815C-0C4061D8999A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"94ed348b0a35c2a6bf56c4bce9f1bd324eddbb65","datavalue":{"value":{"entity-type":"item","numeric-id":3090862,"id":"Q3090862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"30611a7e7b785473ef8533d98b85e8879a01a3ea","datavalue":{"value":{"amount":"+0.7476765513420105","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":"Q4993350$B5AE0B47-2C59-4FBC-9717-88326ECB2263","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"46d5eb500b91b900b7e0ec167e7c875fd9ecd2d8","datavalue":{"value":{"entity-type":"item","numeric-id":2828239,"id":"Q2828239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"298063c81dc267c4335bed3878e4d38253e0f83f","datavalue":{"value":{"amount":"+0.738724946975708","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":"Q4993350$37F514C5-314C-4A7E-8886-AB4EA61F4BE3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4993350","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4993350"}}}}}