{"entities":{"Q7361765":{"pageid":31520834,"ns":120,"title":"Item:Q7361765","lastrevid":105368930,"modified":"2026-10-07T13:37:39Z","type":"item","id":"Q7361765","labels":{"en":{"language":"en","value":"Bicategories"}},"descriptions":{"en":{"language":"en","value":"AFP entry Bicategory"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"649c021dfcd3dfe84420a0c8b0928672ccfd0d97","datavalue":{"value":"https://isa-afp.org/entries/Bicategory.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361765$0C8D7E56-BBBB-4DED-A7C5-9537EF1557D8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5d45836b2c2459ddaa79b882709b6e678573b236","datavalue":{"value":{"time":"+2020-01-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361765$ADE5FA60-D773-4673-B940-EE79076B958B","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"aa006e0db7ed3b9da6b729bd3c50b09ed2535412","datavalue":{"value":"Eugene W. Stark","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361765$321CDC27-A3B2-4B2B-893B-39BDBC55AB16","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"84788e4a42963da87e4829de7fa8708ebaf33111","datavalue":{"value":{"text":"Bicategories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361765$7495E952-0318-4E3E-8D87-B2E169DF6F37","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"5fc1357e5cd0b856e9df067bb1d65b41c35fbfc2","datavalue":{"value":"Taking as a starting point the author's previous work on developing aspects of category theory in Isabelle/HOL, this article gives a compatible formalization of the notion of \"bicategory\" and develops a framework within which formal proofs of facts about bicategories can be given. The framework includes a number of basic results, including the Coherence Theorem, the Strictness Theorem, pseudofunctors and biequivalence, and facts about internal equivalences and adjunctions in a bicategory. As a driving application and demonstration of the utility of the framework, it is used to give a formal proof of a theorem, due to Carboni, Kasangian, and Street, that characterizes up to biequivalence the bicategories of spans in a category with pullbacks. The formalization effort necessitated the filling-in of many details that were not evident from the brief presentation in the original paper, as well as identifying a few minor corrections along the way. Revisions made subsequent to the first version of this article added additional material on pseudofunctors, pseudonatural transformations, modifications, and equivalence of bicategories; the main thrust being to give a proof that a pseudofunctor is a biequivalence if and only if it can be extended to an equivalence of bicategories.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361765$D9E72EDD-2FD9-4693-9B44-6F4DB1A8102F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"02440399404883cec035c4ba4333b0b2f70b96a3","datavalue":{"value":{"entity-type":"item","numeric-id":4596052,"id":"Q4596052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361765$826E5018-22A1-4B2D-919E-013D5CD1EE53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bfedd305f8349e1773d49ada817a2bc3f98c047c","datavalue":{"value":{"entity-type":"item","numeric-id":1065921,"id":"Q1065921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361765$D2B4333C-AD32-44F2-AF9D-5538941D00C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"358596db31a85268f2da249f2d363886b423d4b0","datavalue":{"value":{"entity-type":"item","numeric-id":3767474,"id":"Q3767474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361765$CB08927E-366A-4A2A-A465-BEDAD5D5E376","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fd51c3c41da2eaa6b1f56306d51915860a1708c3","datavalue":{"value":{"entity-type":"item","numeric-id":1098929,"id":"Q1098929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361765$0333AC66-694D-48D1-B6E4-A8500A7C44F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"356b8e5086f470dfbaff79e4652f6bdde3f61f89","datavalue":{"value":{"entity-type":"item","numeric-id":3498625,"id":"Q3498625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361765$CCFE33DF-6F65-4E7B-8D66-A9D84F5916F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"95e9eaaaa80a0ca8f9fb93e183a48c2ed7d8cdf2","datavalue":{"value":{"entity-type":"item","numeric-id":3386389,"id":"Q3386389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361765$D56838C5-FA59-4127-9F55-92B44BBF8D62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d95fe6b711716f8b9810844eff2ba2b9a1ed7141","datavalue":{"value":{"entity-type":"item","numeric-id":4092156,"id":"Q4092156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361765$5DA4195A-19A8-4AAF-ACE1-7952BC4E91C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"41e0444e22e4266453ab8adbf280b94bbe6588c9","datavalue":{"value":{"entity-type":"item","numeric-id":3876103,"id":"Q3876103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361765$F4E36474-9BDB-4F13-9E77-72CED7E594C8","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361765$35F0F5C9-146F-4521-875E-E2259513A989","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"13aca46e307c0fa39f919117d8f86b52b1974922","datavalue":{"value":{"entity-type":"item","numeric-id":7361946,"id":"Q7361946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361765$CDC531A6-9737-48A0-98FC-340420D0F003","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"572089e83311a7b04b56c3ffe6d7a11baed7d211","datavalue":{"value":{"entity-type":"item","numeric-id":7360823,"id":"Q7360823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361765$D23C282D-242E-4D29-B3CE-F1CA35ADECB5","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361765$A7AD03D3-CED7-4C68-AE96-56C4B9A61EA4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Bicategories","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Bicategories"}}}}}