{"entities":{"Q2828239":{"pageid":2838977,"ns":120,"title":"Item:Q2828239","lastrevid":42230544,"modified":"2025-06-02T18:34:01Z","type":"item","id":"Q2828239","labels":{"en":{"language":"en","value":"Type theory in type theory using quotient inductive types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6642939"}},"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":"Q2828239$4AE10134-AA3E-4F4E-A37A-0E1F6083CE57","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f8099fa3b0b3195c3ab0022a47cae645b51824ab","datavalue":{"value":{"text":"Type theory in type theory using quotient inductive types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2828239$1A523100-46F3-45F6-A3E4-8C446ECC8487","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"588c3390105e2bbc903bd6ef148551ce1bbfb52b","datavalue":{"value":"1347.68045","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828239$8F88769F-4CFD-4970-81A7-4813EFEF4F92","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"313be6a49e608273ac54425ff7b9bbdd29ab9bb0","datavalue":{"value":"10.1145/2837614.2837638","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828239$44995A61-6139-4992-8B70-31F83CCDB661","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6801a503eb1bea2102d1e59832005afa5cab1cee","datavalue":{"value":{"entity-type":"item","numeric-id":1652991,"id":"Q1652991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2828239$40680BDC-1D8E-4667-81B7-350C6B794772","rank":"normal"},{"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":"Q2828239$C5BB9E87-8A46-41E9-AA92-E988427D3EC2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0a99b403aab07b56f8645942f86d22ab58064aa8","datavalue":{"value":{"entity-type":"item","numeric-id":2828237,"id":"Q2828237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2828239$77C33C2A-89C5-4917-A326-3DDA979B8CAA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1a707999eca047eb3f3f8c2c26743b59dad9c97f","datavalue":{"value":{"time":"+2016-10-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2828239$02E6C86F-070C-4F50-AED9-540CFCD40191","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"092917813a596fac82bbeed38a48d8a5d231aafc","datavalue":{"value":"http://eprints.nottingham.ac.uk/31169/","type":"string"},"datatype":"url"},"type":"statement","id":"Q2828239$5ABFD0EF-DD3B-4728-A229-9A3514C3A982","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828239$BCA95673-9A91-48E3-8E65-33438541D7B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828239$09CD88BB-3188-4D4D-A9BE-76CD6EA430D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828239$DB2D164D-C398-4FA0-85DE-0BECD4B3A724","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828239$155D7417-469A-4FEA-8DE0-4ECF332D30B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828239$4C8BFBA9-A75B-4CA7-ADF5-9EE952134BBD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bfe0375cc677457ec9d380531fe2493358a74046","datavalue":{"value":"6642939","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828239$DC14A985-263B-4B03-A21E-C4A4350B9E19","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cb0249487b7eb1ecf24cddb1d300f9fa92e8fe1d","datavalue":{"value":"Agda","type":"string"},"datatype":"string"},"type":"statement","id":"Q2828239$3E09AE1C-0DB8-4799-AE3D-A94F53903A02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6886acc9bb720e6ad7ca13e49d3bd87570dc950","datavalue":{"value":"higher inductive types","type":"string"},"datatype":"string"},"type":"statement","id":"Q2828239$5FA1D097-81B9-47E0-92F7-58D6BAA1A5FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4ecd2d433c9f863c39fe5a1fa2de24434b6de0d","datavalue":{"value":"homotopy type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2828239$4FB0C049-23E6-4812-B983-985E9237C57E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"02e2bd1176be2ca24a8b368e42bc8812510b3ef7","datavalue":{"value":"logical relations","type":"string"},"datatype":"string"},"type":"statement","id":"Q2828239$749A35BC-46C1-46B8-9E01-18CA48A1A24B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"329d09641862ba8331cecdfb9962e139d99ecf56","datavalue":{"value":"metaprogramming","type":"string"},"datatype":"string"},"type":"statement","id":"Q2828239$8876AEDE-ED0B-4C53-B240-759772439C48","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":"Q2828239$726C87B2-DC21-4ED2-B51D-7A704E7E1329","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"20885e94355546d1b9debd06cb113ad2e8a3be9b","datavalue":{"value":"W2274485505","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828239$898CE8D8-6D1D-4267-ABEA-D5D3D52BCB21","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"60a4734cee99e139b81d30164e7f66c108e2fb10","datavalue":{"value":"Q61583695","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828239$2BD0049A-C962-443C-9F9C-6AF9F09B737A","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":"0ae03ae3eb6b0b022e988ae358c4976820a3d0bc","datavalue":{"value":{"amount":"+0.9448302","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2828239$4A875AEC-396B-4580-88B0-F181EB0BC53A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80eee57571fdbb56a12fbb8fc8ab44a57cfd5c63","datavalue":{"value":{"entity-type":"item","numeric-id":5094144,"id":"Q5094144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"efd9cf345a3916c8b8c0e9c29e9170acdf683805","datavalue":{"value":{"amount":"+0.9375416","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2828239$D8397898-3243-4771-A5FF-FBBCACDA944B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"425e652d4a6ae8c4a1799b298f36c35b402139f5","datavalue":{"value":{"entity-type":"item","numeric-id":2200826,"id":"Q2200826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64827502ef4296543a5fcd5e51d84d896c743b1f","datavalue":{"value":{"amount":"+0.9232493","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2828239$A3ADB004-66DA-45A1-A903-CC9006733803","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":"60069aa999fba3c49d100eda94bb987ec8e2e633","datavalue":{"value":{"amount":"+0.9191201","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2828239$2B7E1BF4-C78B-45F3-A8A3-74D22D75CE27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38f123167db0e80ec2d75bc744cc578e44a7167f","datavalue":{"value":{"entity-type":"item","numeric-id":4635888,"id":"Q4635888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ca8cce6cf5871d0abc6e22ac9c1428eb4a45ee0a","datavalue":{"value":{"amount":"+0.91417205","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2828239$09DD2040-1B2A-46FB-A456-34385C4A211B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"76deb5535e00ebcb01402afbe64314fa9e23992c","datavalue":{"value":{"entity-type":"item","numeric-id":678762,"id":"Q678762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fce0e722c3c5f0dd235e5dcc043ae5fe04a63126","datavalue":{"value":{"amount":"+0.90766996","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2828239$DEEFAA03-D1BE-4F82-B647-7C6F736D53E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"696d83aaec159cdf8ddedd031545e8cc3910de03","datavalue":{"value":{"entity-type":"item","numeric-id":4247306,"id":"Q4247306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fadbb79c127ede7fcca0078d695f09044b67248e","datavalue":{"value":{"amount":"+0.90723497","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2828239$33193477-F89D-49A6-ACA9-D17070D08B1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04fe00dd16f83f29e78f1f29866c0bdd4cd88a8b","datavalue":{"value":{"entity-type":"item","numeric-id":4457447,"id":"Q4457447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"da584f984e74fc87af938e53117228adae36ca1b","datavalue":{"value":{"amount":"+0.9067459","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2828239$A4D4DFC8-912F-42D5-B4FA-EEF3F79F262E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"387cce94216297b66f69d2aa4feef49d02d8cfd3","datavalue":{"value":{"entity-type":"item","numeric-id":4681362,"id":"Q4681362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"da584f984e74fc87af938e53117228adae36ca1b","datavalue":{"value":{"amount":"+0.9067459","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2828239$905DE88F-8BBE-4412-AF63-14BA520284F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8fcd6a31033790feb804853ef802917b2dd1efe5","datavalue":{"value":{"entity-type":"item","numeric-id":4944857,"id":"Q4944857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"68e939844a51ba1e01ebab622d4463bbb6531164","datavalue":{"value":{"amount":"+0.9062787","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2828239$4F7D7EF7-3731-4E20-AEEA-68DF3EA0FDB7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2828239","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2828239"}}}}}