{"entities":{"Q3638923":{"pageid":5668829,"ns":120,"title":"Item:Q3638923","lastrevid":88698416,"modified":"2026-06-04T15:13:04Z","type":"item","id":"Q3638923","labels":{"en":{"language":"en","value":"An induction principle for nested datatypes in intensional type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5622307"}},"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":"Q3638923$78A6E00C-F09A-44A4-B85E-A737396435AD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1ee31924bbf17e4734c19887ba486ed8babf695f","datavalue":{"value":{"text":"An induction principle for nested datatypes in intensional type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3638923$C436B760-365C-4548-94B7-4CB1E5EDE0B0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8116f21c323f8dfecc94bc4ab42d217ccbfb774a","datavalue":{"value":"1191.68164","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3638923$BB6A5EE3-D14E-476E-B01C-7D0EF0305A17","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2a0f492089f8323fae06f296bbbe942fe5da333a","datavalue":{"value":"10.1017/S095679680900731X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3638923$F3FF91EA-C583-4CB9-9B16-B5DA29F2A986","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0f31cf0ba649c82a71b5cbd30114eb63bfddbeed","datavalue":{"value":{"entity-type":"item","numeric-id":627203,"id":"Q627203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3638923$B8B3D5CE-7A06-475A-9041-DC5EA244C2E6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"c0cefd96801130048cf3f8ae21032b5cf52d744d","datavalue":{"value":{"entity-type":"item","numeric-id":2713363,"id":"Q2713363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3638923$9E59E5D3-7003-414A-AF3F-6950D0E1A046","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"979675af8434f65c971325fe4cac7cabed000b0e","datavalue":{"value":{"time":"+2009-10-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3638923$A9C13F50-6651-497E-8EFE-3DDE5F430B5E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3638923$C1EDD65B-D29B-45FA-A4C3-01070912370B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3638923$140F3B41-5490-4E03-BFC8-711588F8BAF8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"578881795d9c9fc19677966b5b7c568b8f2dd6c5","datavalue":{"value":"5622307","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3638923$2E7ACB01-757E-4F0B-9650-DBAE95423DFF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"84a3d57a442430d76e1a66aa304bc2390efa571b","datavalue":{"value":"true nesting","type":"string"},"datatype":"string"},"type":"statement","id":"Q3638923$277DA4C2-883B-4FC6-9858-46F20728786B","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":"Q3638923$F5894287-7DDF-4914-9BF6-A411775E9C1C","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":"Q3638923$47F8AD2C-E017-4C29-8D4A-E278F6A7102B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e6e84dc7d2442795960d241851cf13bc84741e4","datavalue":{"value":{"entity-type":"item","numeric-id":1412830,"id":"Q1412830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3638923$46572898-0FBD-42F0-B363-5EE44633F366","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb40888863b7482529afe1d3e94fafa33922ef75","datavalue":{"value":{"entity-type":"item","numeric-id":1389772,"id":"Q1389772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3638923$F935122D-2A21-425F-A5C1-2AED42F66707","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":"Q3638923$1180A5C3-2543-42C5-B913-B2CED63B292D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a1c4e3e9abb8d3f1418514c061c1d7ea6d5d61f","datavalue":{"value":{"entity-type":"item","numeric-id":1346686,"id":"Q1346686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3638923$B72DF25D-3A5C-4737-9C0F-917C12A05F03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a17422820de131ed03dd36bb6484e8aa078aa9e","datavalue":{"value":{"entity-type":"item","numeric-id":1965249,"id":"Q1965249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3638923$CE1BA606-DF05-4C83-91F1-1052AF00C92C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a797407b4949355fcd06204fe2bcb7b1218a925","datavalue":{"value":{"entity-type":"item","numeric-id":4256148,"id":"Q4256148"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3638923$2787CA05-BE58-434A-B65D-211C410CE67C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"150719399e882b786834d79969b3d0373e1dfbae","datavalue":{"value":{"entity-type":"item","numeric-id":1770412,"id":"Q1770412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3638923$24E059AA-167B-4DDD-BB2A-6260509CE9C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a19e38fbc8f9f8c11b9ab7ad79f464c27504bd57","datavalue":{"value":{"entity-type":"item","numeric-id":1882785,"id":"Q1882785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3638923$B61997FA-A7BD-4A71-9B21-5BD03026272B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"801fc82b2263da90eb46f3f131ff2056c6826c16","datavalue":{"value":{"entity-type":"item","numeric-id":5958300,"id":"Q5958300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3638923$455C3888-DD21-49B8-8BC8-8386629893CF","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":"Q3638923$CAD663B8-F7E1-43EB-ADBA-400BA7B7CB49","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0f7f90919181d7fd39fe7ee9f5f53d1191d927ec","datavalue":{"value":{"entity-type":"item","numeric-id":3507459,"id":"Q3507459"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1c4a85cc4a96d045c9e51df40ee69f0a0d5db733","datavalue":{"value":{"amount":"+0.8676188588142395","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":"Q3638923$5B5AA98B-A99D-4C7F-B0EE-B7052CEAD125","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51b78ba281286c1cc0ddf52fabe91d14b7284261","datavalue":{"value":{"entity-type":"item","numeric-id":3521990,"id":"Q3521990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3843fb11ee4dda7811057aa5af31cbecfb72a2a4","datavalue":{"value":{"amount":"+0.8004751205444336","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":"Q3638923$A56D811C-4A9E-4425-B574-FD24A629B838","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"03e96a75c638ea07d906709b6f3d72e0361a09eb","datavalue":{"value":{"entity-type":"item","numeric-id":627204,"id":"Q627204"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f8782500088742cb781ab3335a9ccc1e1c33bb54","datavalue":{"value":{"amount":"+0.7972568869590759","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":"Q3638923$670C882A-5ED7-4AD1-9246-82C3B0298018","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8481af880417872a6aa16122fd2b04cd7ce47b4d","datavalue":{"value":{"entity-type":"item","numeric-id":1770412,"id":"Q1770412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"75b0bd742e256fb890936fd2348966fe37288e21","datavalue":{"value":{"amount":"+0.7727831602096558","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":"Q3638923$B27B0714-0171-42AF-A08A-82ECD90F5343","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6a316e6ef0b87e92870cc171f9edd26b23fea6b8","datavalue":{"value":{"entity-type":"item","numeric-id":4435457,"id":"Q4435457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"943b6e25e7efc4a58d45e603e33d32d083b15949","datavalue":{"value":{"amount":"+0.7645750045776367","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":"Q3638923$017DA1C8-2D13-4F85-9959-77042821F4D5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An induction principle for nested datatypes in intensional type theory","badges":[]}}}}}