{"entities":{"Q5369495":{"pageid":7399069,"ns":120,"title":"Item:Q5369495","lastrevid":58554144,"modified":"2026-04-05T17:44:24Z","type":"item","id":"Q5369495","labels":{"en":{"language":"en","value":"Category theory in Coq 8.5"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6792363"}},"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":"Q5369495$9ED1E95C-0472-4BB3-9699-CEFADD06A0EF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"01ee0cad4dca45f4fc01ab702ea85408e500673e","datavalue":{"value":"1387.68208","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369495$69F1D622-C97D-4980-BE61-AE1B2A5826F0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"52254dabb8af5997f12cdfe0722d50f0619c8ae0","datavalue":{"value":{"entity-type":"item","numeric-id":2787452,"id":"Q2787452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5369495$DEE59618-4A32-4B40-99B1-71B5EE4A33DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2a24a20456dfce72b4740899a4bd7c6aec9611b4","datavalue":{"value":{"entity-type":"item","numeric-id":225076,"id":"Q225076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5369495$00AD6645-0AD1-48DB-8CDD-19F477303D1B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"eae4cdb5001296cfa1d627ad5453506a5832f064","datavalue":{"value":{"time":"+2017-10-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5369495$4A3E0644-00F5-4344-8DE9-65D0540E8437","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d321edd73c0ecd9c95ff8aaa0163dc9bf34e886c","datavalue":{"value":"https://arxiv.org/abs/1505.06430","type":"string"},"datatype":"url"},"type":"statement","id":"Q5369495$9139BB92-FBC1-4AA1-AF2C-D878B485B270","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369495$C74808D0-CC10-4BAD-8CCD-4970A0BBC7AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369495$7634E6C2-D733-4347-9353-D23573BDC8E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"957970e11422fbdef7ba9db5e2b00bc9584e024a","datavalue":{"value":"03G30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369495$E7EC1FD2-C3BF-4B03-B413-25E8F15E100A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fd14109b728357c96051ccc125db5e1d8c36ea77","datavalue":{"value":"18A99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369495$B9FA6C52-9B55-429D-A0D8-AAB4BC5D133C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c9fdba58e5344e05288d09cbbfa64fc756b9e06c","datavalue":{"value":"55U40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369495$52359E5D-131E-4513-90F8-B18AF682FC56","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5b113365ad3ef3dc9c68328a6109601eedb886be","datavalue":{"value":"6792363","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369495$A97B807A-13E8-458C-A883-823CD9D5C33E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5685485f4c27abda29cd481c0486a1adb54b3a91","datavalue":{"value":"category theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5369495$57221661-21A5-4E33-9A61-BB5A1DDB9D5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2b48acc054c9f6dbd6b4cfb055569602fccbe91f","datavalue":{"value":"Coq 8.5","type":"string"},"datatype":"string"},"type":"statement","id":"Q5369495$8D8CB6C3-D0B9-4ED8-BD10-3D4F686DF04A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c1159aa73cd8daf4c43043be733617a1e49169dd","datavalue":{"value":"universe polymorphism","type":"string"},"datatype":"string"},"type":"statement","id":"Q5369495$C3C31A8E-0938-4298-9A3E-72C19CA7CE87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4ecd2d433c9f863c39fe5a1fa2de24434b6de0d","datavalue":{"value":"homotopy type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5369495$29D47C3B-33CF-49E3-9C4A-E2F538A15B52","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":"Q5369495$524A961D-243A-463B-9C7C-026E2D183C08","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":"Q5369495$E4C34898-8D92-4B85-AA53-361C42A81B47","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":"Q5369495$547B43C7-F7A3-4FDF-A6EF-76E2A5CBF98F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d559a6d3ff27fb7ff38109fff92879994da52541","datavalue":{"value":"W2963937335","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369495$B770E624-D133-4816-A410-33839133CBC7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1f1416f31cf889fc8368d41958e98b924b571290","datavalue":{"value":{"text":"Category Theory in Coq 8.5","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5369495$22464D3F-B7C3-4C23-85E6-C679882DB021","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2cd14650b506e93298c21b5d025f0618817c4a4a","datavalue":{"value":"10.4230/LIPICS.FSCD.2016.30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369495$FC5A37A2-31A8-4008-8731-8F0D74AD42A4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f01c34cf127cab6b89eb2237d2709109219843ca","datavalue":{"value":{"entity-type":"item","numeric-id":2879258,"id":"Q2879258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7ce66a55fc124e818ca6b4705e1bc566dcc5f660","datavalue":{"value":{"amount":"+0.8294665813446045","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":"Q5369495$11DCD17F-6DD8-4AAE-91D1-8AAE7D8AEA55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e03cdfb400b819a8f34af382fa6e1e0f0778dd69","datavalue":{"value":{"entity-type":"item","numeric-id":1987219,"id":"Q1987219"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9a7d9b1a50ca545baa2b4285a419ce8dde151db5","datavalue":{"value":{"amount":"+0.7567926645278931","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":"Q5369495$5F8264D1-E068-4026-8389-D4064D0B5461","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f283ce1b7bb222e202a6acf28a6a844d9018de04","datavalue":{"value":{"entity-type":"item","numeric-id":5747673,"id":"Q5747673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ca4318278cd94a2e8bc0dec45bac5d52ccedff29","datavalue":{"value":{"amount":"+0.7299473285675049","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":"Q5369495$7AA9F129-2A98-4768-B72E-60CB0A3671DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dea9de8d016a1d49557bfa69a14fa567679694d2","datavalue":{"value":{"entity-type":"item","numeric-id":2879272,"id":"Q2879272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"11af93f5a68b22adf6a119cc13b560cb1db752d4","datavalue":{"value":{"amount":"+0.7223218679428101","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":"Q5369495$E64579D0-24D1-4C13-AD12-F92096C2248C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"119fc0bd9b24a50f4879867ef374d75d8eaf4446","datavalue":{"value":{"entity-type":"item","numeric-id":2921123,"id":"Q2921123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d8b4d81c64bfe8648b9d82f7040b8db503b27163","datavalue":{"value":{"amount":"+0.7200096249580383","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":"Q5369495$036BC664-BBA3-4BA9-B377-3E091297090F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5369495","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5369495"}}}}}