1#SIXFORMAT GapDocGAP 2HELPBOOKINFOSIXTMP := rec( 3encoding := "UTF-8", 4bookname := "MonoidalCategories", 5entries := 6[ [ "Title page", ".", [ 0, 0, 0 ], 1, 1, "title page", "X7D2C85EC87DD46E5" ], 7 [ "Table of Contents", ".-1", [ 0, 0, 1 ], 53, 2, "table of contents", 8 "X8537FEB07AF2BEC8" ], 9 [ 10 "\033[1X\033[33X\033[0;-2YTensor Product and Internal Hom\033[133X\033[101X\ 11", "1", [ 1, 0, 0 ], 1, 3, "tensor product and internal hom", 12 "X7AF6C1DF84986EEA" ], 13 [ "\033[1X\033[33X\033[0;-2YMonoidal Categories\033[133X\033[101X", "1.1", 14 [ 1, 1, 0 ], 4, 3, "monoidal categories", "X808DC49C7ED99B52" ], 15 [ "\033[1X\033[33X\033[0;-2YBraided Monoidal Categories\033[133X\033[101X", 16 "1.2", [ 1, 2, 0 ], 387, 9, "braided monoidal categories", 17 "X7D94AD967E6D60F1" ], 18 [ "\033[1X\033[33X\033[0;-2YSymmetric Monoidal Categories\033[133X\033[101X" 19 , "1.3", [ 1, 3, 0 ], 459, 10, "symmetric monoidal categories", 20 "X85ED71067F7CEA82" ], 21 [ 22 "\033[1X\033[33X\033[0;-2YSymmetric Closed Monoidal Categories\033[133X\\ 23033[101X", "1.4", [ 1, 4, 0 ], 466, 11, "symmetric closed monoidal categories" 24 , "X849F4CB58466EAEB" ], 25 [ 26 "\033[1X\033[33X\033[0;-2YRigid Symmetric Closed Monoidal Categories\033[13\ 273X\033[101X", "1.5", [ 1, 5, 0 ], 1190, 23, 28 "rigid symmetric closed monoidal categories", "X805AEF9784062A31" ], 29 [ "\033[1X\033[33X\033[0;-2YExamples and Tests\033[133X\033[101X", "2", 30 [ 2, 0, 0 ], 1, 25, "examples and tests", "X7967FE8E7BBDF485" ], 31 [ "\033[1X\033[33X\033[0;-2YBasics\033[133X\033[101X", "2.1", [ 2, 1, 0 ], 32 4, 25, "basics", "X868F7BAB7AC2EEBC" ], 33 [ "Index", "ind", [ "Ind", 0, 0 ], 1, 26, "index", "X83A0356F839C696F" ], 34 [ 35 "\033[2XTensorProductOnObjects\033[102X for iscapcategoryobject, iscapcateg\ 36oryobject", "1.1-1", [ 1, 1, 1 ], 36, 3, 37 "tensorproductonobjects for iscapcategoryobject iscapcategoryobject", 38 "X797034F17AA47EE0" ], 39 [ "\033[2XAddTensorProductOnObjects\033[102X for iscapcategory, isfunction", 40 "1.1-2", [ 1, 1, 2 ], 44, 3, 41 "addtensorproductonobjects for iscapcategory isfunction", 42 "X7CED389B792142F5" ], 43 [ 44 "\033[2XTensorProductOnMorphisms\033[102X for iscapcategorymorphism, iscapc\ 45ategorymorphism", "1.1-3", [ 1, 1, 3 ], 53, 4, 46 "tensorproductonmorphisms for iscapcategorymorphism iscapcategorymorphis\ 47m", "X84997A1E8188D6BE" ], 48 [ 49 "\033[2XTensorProductOnMorphismsWithGivenTensorProducts\033[102X for iscapc\ 50ategoryobject, iscapcategorymorphism, iscapcategorymorphism, iscapcategoryobje\ 51ct", "1.1-4", [ 1, 1, 4 ], 61, 4, 52 "tensorproductonmorphismswithgiventensorproducts for iscapcategoryobject\ 53 iscapcategorymorphism iscapcategorymorphism iscapcategoryobject", 54 "X85008BF07C2C0386" ], 55 [ 56 "\033[2XAddTensorProductOnMorphismsWithGivenTensorProducts\033[102X for isc\ 57apcategory, isfunction", "1.1-5", [ 1, 1, 5 ], 70, 4, 58 "addtensorproductonmorphismswithgiventensorproducts for iscapcategory is\ 59function", "X879659397D11AD9F" ], 60 [ 61 "\033[2XAssociatorRightToLeft\033[102X for iscapcategoryobject, iscapcatego\ 62ryobject, iscapcategoryobject", "1.1-6", [ 1, 1, 6 ], 81, 4, 63 "associatorrighttoleft for iscapcategoryobject iscapcategoryobject iscap\ 64categoryobject", "X84C2FAEA7B9678AA" ], 65 [ 66 "\033[2XAssociatorRightToLeftWithGivenTensorProducts\033[102X for iscapcate\ 67goryobject, iscapcategoryobject, iscapcategoryobject, iscapcategoryobject, isc\ 68apcategoryobject", "1.1-7", [ 1, 1, 7 ], 91, 4, 69 "associatorrighttoleftwithgiventensorproducts for iscapcategoryobject is\ 70capcategoryobject iscapcategoryobject iscapcategoryobject iscapcategoryobject" 71 , "X85645C4D86060ED2" ], 72 [ 73 "\033[2XAddAssociatorRightToLeftWithGivenTensorProducts\033[102X for iscapc\ 74ategory, isfunction", "1.1-8", [ 1, 1, 8 ], 102, 4, 75 "addassociatorrighttoleftwithgiventensorproducts for iscapcategory isfun\ 76ction", "X7CF105217904D280" ], 77 [ 78 "\033[2XAssociatorLeftToRight\033[102X for iscapcategoryobject, iscapcatego\ 79ryobject, iscapcategoryobject", "1.1-9", [ 1, 1, 9 ], 112, 5, 80 "associatorlefttoright for iscapcategoryobject iscapcategoryobject iscap\ 81categoryobject", "X7C5A064C7E1995F1" ], 82 [ 83 "\033[2XAssociatorLeftToRightWithGivenTensorProducts\033[102X for iscapcate\ 84goryobject, iscapcategoryobject, iscapcategoryobject, iscapcategoryobject, isc\ 85apcategoryobject", "1.1-10", [ 1, 1, 10 ], 122, 5, 86 "associatorlefttorightwithgiventensorproducts for iscapcategoryobject is\ 87capcategoryobject iscapcategoryobject iscapcategoryobject iscapcategoryobject" 88 , "X7C59D73F8389E389" ], 89 [ 90 "\033[2XAddAssociatorLeftToRightWithGivenTensorProducts\033[102X for iscapc\ 91ategory, isfunction", "1.1-11", [ 1, 1, 11 ], 133, 5, 92 "addassociatorlefttorightwithgiventensorproducts for iscapcategory isfun\ 93ction", "X850B5B357F592FAE" ], 94 [ "\033[2XTensorUnit\033[102X for iscapcategory", "1.1-12", [ 1, 1, 12 ], 95 143, 5, "tensorunit for iscapcategory", "X7BF7FFDF8789474A" ], 96 [ "\033[2XAddTensorUnit\033[102X for iscapcategory, isfunction", "1.1-13", 97 [ 1, 1, 13 ], 151, 5, "addtensorunit for iscapcategory isfunction", 98 "X7BC4B940858F903B" ], 99 [ "\033[2XLeftUnitor\033[102X for iscapcategoryobject", "1.1-14", 100 [ 1, 1, 14 ], 160, 5, "leftunitor for iscapcategoryobject", 101 "X7EBCAFDD81BDB655" ], 102 [ 103 "\033[2XLeftUnitorWithGivenTensorProduct\033[102X for iscapcategoryobject, \ 104iscapcategoryobject", "1.1-15", [ 1, 1, 15 ], 168, 6, 105 "leftunitorwithgiventensorproduct for iscapcategoryobject iscapcategoryo\ 106bject", "X7ED284DF7BA21774" ], 107 [ 108 "\033[2XAddLeftUnitorWithGivenTensorProduct\033[102X for iscapcategory, isf\ 109unction", "1.1-16", [ 1, 1, 16 ], 176, 6, 110 "addleftunitorwithgiventensorproduct for iscapcategory isfunction", 111 "X8614FD9C78812C98" ], 112 [ "\033[2XLeftUnitorInverse\033[102X for iscapcategoryobject", "1.1-17", 113 [ 1, 1, 17 ], 185, 6, "leftunitorinverse for iscapcategoryobject", 114 "X79A274078147A9F7" ], 115 [ 116 "\033[2XLeftUnitorInverseWithGivenTensorProduct\033[102X for iscapcategoryo\ 117bject, iscapcategoryobject", "1.1-18", [ 1, 1, 18 ], 193, 6, 118 "leftunitorinversewithgiventensorproduct for iscapcategoryobject iscapca\ 119tegoryobject", "X849609447CAE996B" ], 120 [ 121 "\033[2XAddLeftUnitorInverseWithGivenTensorProduct\033[102X for iscapcatego\ 122ry, isfunction", "1.1-19", [ 1, 1, 19 ], 201, 6, 123 "addleftunitorinversewithgiventensorproduct for iscapcategory isfunction\ 124", "X87CB487587ED3EC5" ], 125 [ "\033[2XRightUnitor\033[102X for iscapcategoryobject", "1.1-20", 126 [ 1, 1, 20 ], 211, 6, "rightunitor for iscapcategoryobject", 127 "X82F758CB7A23468A" ], 128 [ 129 "\033[2XRightUnitorWithGivenTensorProduct\033[102X for iscapcategoryobject,\ 130 iscapcategoryobject", "1.1-21", [ 1, 1, 21 ], 219, 6, 131 "rightunitorwithgiventensorproduct for iscapcategoryobject iscapcategory\ 132object", "X84C8F97F7BF2282D" ], 133 [ 134 "\033[2XAddRightUnitorWithGivenTensorProduct\033[102X for iscapcategory, is\ 135function", "1.1-22", [ 1, 1, 22 ], 227, 7, 136 "addrightunitorwithgiventensorproduct for iscapcategory isfunction", 137 "X7DB39DC9794F3FCA" ], 138 [ "\033[2XRightUnitorInverse\033[102X for iscapcategoryobject", "1.1-23", 139 [ 1, 1, 23 ], 236, 7, "rightunitorinverse for iscapcategoryobject", 140 "X82DC825480E87301" ], 141 [ 142 "\033[2XRightUnitorInverseWithGivenTensorProduct\033[102X for iscapcategory\ 143object, iscapcategoryobject", "1.1-24", [ 1, 1, 24 ], 244, 7, 144 "rightunitorinversewithgiventensorproduct for iscapcategoryobject iscapc\ 145ategoryobject", "X85A8A87C87B33008" ], 146 [ 147 "\033[2XAddRightUnitorInverseWithGivenTensorProduct\033[102X for iscapcateg\ 148ory, isfunction", "1.1-25", [ 1, 1, 25 ], 252, 7, 149 "addrightunitorinversewithgiventensorproduct for iscapcategory isfunctio\ 150n", "X8682171F86C6793E" ], 151 [ 152 "\033[2XLeftDistributivityExpanding\033[102X for iscapcategoryobject, islis\ 153t", "1.1-26", [ 1, 1, 26 ], 262, 7, 154 "leftdistributivityexpanding for iscapcategoryobject islist", 155 "X7ACF268E7D82B0C9" ], 156 [ 157 "\033[2XLeftDistributivityExpandingWithGivenObjects\033[102X for iscapcateg\ 158oryobject, iscapcategoryobject, islist, iscapcategoryobject", "1.1-27", 159 [ 1, 1, 27 ], 272, 7, 160 "leftdistributivityexpandingwithgivenobjects for iscapcategoryobject isc\ 161apcategoryobject islist iscapcategoryobject", "X7CA18968862D2285" ], 162 [ 163 "\033[2XAddLeftDistributivityExpandingWithGivenObjects\033[102X for iscapca\ 164tegory, isfunction", "1.1-28", [ 1, 1, 28 ], 282, 8, 165 "addleftdistributivityexpandingwithgivenobjects for iscapcategory isfunc\ 166tion", "X814BA200802D26E4" ], 167 [ 168 "\033[2XLeftDistributivityFactoring\033[102X for iscapcategoryobject, islis\ 169t", "1.1-29", [ 1, 1, 29 ], 293, 8, 170 "leftdistributivityfactoring for iscapcategoryobject islist", 171 "X780322FE7E5A626D" ], 172 [ 173 "\033[2XLeftDistributivityFactoringWithGivenObjects\033[102X for iscapcateg\ 174oryobject, iscapcategoryobject, islist, iscapcategoryobject", "1.1-30", 175 [ 1, 1, 30 ], 303, 8, 176 "leftdistributivityfactoringwithgivenobjects for iscapcategoryobject isc\ 177apcategoryobject islist iscapcategoryobject", "X784D8CD685F5F021" ], 178 [ 179 "\033[2XAddLeftDistributivityFactoringWithGivenObjects\033[102X for iscapca\ 180tegory, isfunction", "1.1-31", [ 1, 1, 31 ], 313, 8, 181 "addleftdistributivityfactoringwithgivenobjects for iscapcategory isfunc\ 182tion", "X7F0A439478576973" ], 183 [ 184 "\033[2XRightDistributivityExpanding\033[102X for islist, iscapcategoryobje\ 185ct", "1.1-32", [ 1, 1, 32 ], 324, 8, 186 "rightdistributivityexpanding for islist iscapcategoryobject", 187 "X8409C74778A4313A" ], 188 [ 189 "\033[2XRightDistributivityExpandingWithGivenObjects\033[102X for iscapcate\ 190goryobject, islist, iscapcategoryobject, iscapcategoryobject", "1.1-33", 191 [ 1, 1, 33 ], 335, 8, 192 "rightdistributivityexpandingwithgivenobjects for iscapcategoryobject is\ 193list iscapcategoryobject iscapcategoryobject", "X7DBE629F811DEADC" ], 194 [ 195 "\033[2XAddRightDistributivityExpandingWithGivenObjects\033[102X for iscapc\ 196ategory, isfunction", "1.1-34", [ 1, 1, 34 ], 345, 9, 197 "addrightdistributivityexpandingwithgivenobjects for iscapcategory isfun\ 198ction", "X7A6178C17EFC817A" ], 199 [ 200 "\033[2XRightDistributivityFactoring\033[102X for islist, iscapcategoryobje\ 201ct", "1.1-35", [ 1, 1, 35 ], 356, 9, 202 "rightdistributivityfactoring for islist iscapcategoryobject", 203 "X86C5C33786C1DC28" ], 204 [ 205 "\033[2XRightDistributivityFactoringWithGivenObjects\033[102X for iscapcate\ 206goryobject, islist, iscapcategoryobject, iscapcategoryobject", "1.1-36", 207 [ 1, 1, 36 ], 366, 9, 208 "rightdistributivityfactoringwithgivenobjects for iscapcategoryobject is\ 209list iscapcategoryobject iscapcategoryobject", "X795267217F7807CE" ], 210 [ 211 "\033[2XAddRightDistributivityFactoringWithGivenObjects\033[102X for iscapc\ 212ategory, isfunction", "1.1-37", [ 1, 1, 37 ], 376, 9, 213 "addrightdistributivityfactoringwithgivenobjects for iscapcategory isfun\ 214ction", "X842099557CF2036E" ], 215 [ "\033[2XBraiding\033[102X for iscapcategoryobject, iscapcategoryobject", 216 "1.2-1", [ 1, 2, 1 ], 405, 10, 217 "braiding for iscapcategoryobject iscapcategoryobject", 218 "X7C6ADBFE7A8DD1E3" ], 219 [ 220 "\033[2XBraidingWithGivenTensorProducts\033[102X for iscapcategoryobject, i\ 221scapcategoryobject, iscapcategoryobject, iscapcategoryobject", "1.2-2", 222 [ 1, 2, 2 ], 413, 10, 223 "braidingwithgiventensorproducts for iscapcategoryobject iscapcategoryob\ 224ject iscapcategoryobject iscapcategoryobject", "X7F4B09A87B2500C0" ], 225 [ 226 "\033[2XAddBraidingWithGivenTensorProducts\033[102X for iscapcategory, isfu\ 227nction", "1.2-3", [ 1, 2, 3 ], 422, 10, 228 "addbraidingwithgiventensorproducts for iscapcategory isfunction", 229 "X7A52CBE8801D6B28" ], 230 [ 231 "\033[2XBraidingInverse\033[102X for iscapcategoryobject, iscapcategoryobje\ 232ct", "1.2-4", [ 1, 2, 4 ], 432, 10, 233 "braidinginverse for iscapcategoryobject iscapcategoryobject", 234 "X8195EC5279D3E8D0" ], 235 [ 236 "\033[2XBraidingInverseWithGivenTensorProducts\033[102X for iscapcategoryob\ 237ject, iscapcategoryobject, iscapcategoryobject, iscapcategoryobject", 238 "1.2-5", [ 1, 2, 5 ], 440, 10, 239 "braidinginversewithgiventensorproducts for iscapcategoryobject iscapcat\ 240egoryobject iscapcategoryobject iscapcategoryobject", "X854AFBC67C836769" ], 241 [ "\033[2XAddBraidingInverseWithGivenTensorProducts\033[102X for iscapcatego\ 242ry, isfunction", "1.2-6", [ 1, 2, 6 ], 449, 10, 243 "addbraidinginversewithgiventensorproducts for iscapcategory isfunction" 244 , "X85C7E40583A5955F" ], 245 [ 246 "\033[2XInternalHomOnObjects\033[102X for iscapcategoryobject, iscapcategor\ 247yobject", "1.4-1", [ 1, 4, 1 ], 475, 11, 248 "internalhomonobjects for iscapcategoryobject iscapcategoryobject", 249 "X78AA83E77B380D68" ], 250 [ "\033[2XAddInternalHomOnObjects\033[102X for iscapcategory, isfunction", 251 "1.4-2", [ 1, 4, 2 ], 483, 11, 252 "addinternalhomonobjects for iscapcategory isfunction", 253 "X7B74F8FD8348D590" ], 254 [ 255 "\033[2XInternalHomOnMorphisms\033[102X for iscapcategorymorphism, iscapcat\ 256egorymorphism", "1.4-3", [ 1, 4, 3 ], 492, 11, 257 "internalhomonmorphisms for iscapcategorymorphism iscapcategorymorphism" 258 , "X7C0191A483A72F98" ], 259 [ 260 "\033[2XInternalHomOnMorphismsWithGivenInternalHoms\033[102X for iscapcateg\ 261oryobject, iscapcategorymorphism, iscapcategorymorphism, iscapcategoryobject", 262 "1.4-4", [ 1, 4, 4 ], 503, 11, 263 "internalhomonmorphismswithgiveninternalhoms for iscapcategoryobject isc\ 264apcategorymorphism iscapcategorymorphism iscapcategoryobject", 265 "X861226B47B5CB713" ], 266 [ 267 "\033[2XAddInternalHomOnMorphismsWithGivenInternalHoms\033[102X for iscapca\ 268tegory, isfunction", "1.4-5", [ 1, 4, 5 ], 515, 11, 269 "addinternalhomonmorphismswithgiveninternalhoms for iscapcategory isfunc\ 270tion", "X8070203E80388349" ], 271 [ 272 "\033[2XEvaluationMorphism\033[102X for iscapcategoryobject, iscapcategoryo\ 273bject", "1.4-6", [ 1, 4, 6 ], 527, 12, 274 "evaluationmorphism for iscapcategoryobject iscapcategoryobject", 275 "X809226D2878DD662" ], 276 [ 277 "\033[2XEvaluationMorphismWithGivenSource\033[102X for iscapcategoryobject,\ 278 iscapcategoryobject, iscapcategoryobject", "1.4-7", [ 1, 4, 7 ], 537, 12, 279 "evaluationmorphismwithgivensource for iscapcategoryobject iscapcategory\ 280object iscapcategoryobject", "X7E42359B7A888F61" ], 281 [ 282 "\033[2XAddEvaluationMorphismWithGivenSource\033[102X for iscapcategory, is\ 283function", "1.4-8", [ 1, 4, 8 ], 548, 12, 284 "addevaluationmorphismwithgivensource for iscapcategory isfunction", 285 "X7D5C06137CEB86B0" ], 286 [ 287 "\033[2XCoevaluationMorphism\033[102X for iscapcategoryobject, iscapcategor\ 288yobject", "1.4-9", [ 1, 4, 9 ], 558, 12, 289 "coevaluationmorphism for iscapcategoryobject iscapcategoryobject", 290 "X79E277047AB3E909" ], 291 [ 292 "\033[2XCoevaluationMorphismWithGivenRange\033[102X for iscapcategoryobject\ 293, iscapcategoryobject, iscapcategoryobject", "1.4-10", [ 1, 4, 10 ], 568, 12, 294 "coevaluationmorphismwithgivenrange for iscapcategoryobject iscapcategor\ 295yobject iscapcategoryobject", "X7E8123AD8567A5C0" ], 296 [ 297 "\033[2XAddCoevaluationMorphismWithGivenRange\033[102X for iscapcategory, i\ 298sfunction", "1.4-11", [ 1, 4, 11 ], 579, 12, 299 "addcoevaluationmorphismwithgivenrange for iscapcategory isfunction", 300 "X817E96AA7ACACE89" ], 301 [ 302 "\033[2XTensorProductToInternalHomAdjunctionMap\033[102X for iscapcategoryo\ 303bject, iscapcategoryobject, iscapcategorymorphism", "1.4-12", [ 1, 4, 12 ], 304 589, 13, 305 "tensorproducttointernalhomadjunctionmap for iscapcategoryobject iscapca\ 306tegoryobject iscapcategorymorphism", "X809E6A3182D62DCB" ], 307 [ 308 "\033[2XAddTensorProductToInternalHomAdjunctionMap\033[102X for iscapcatego\ 309ry, isfunction", "1.4-13", [ 1, 4, 13 ], 598, 13, 310 "addtensorproducttointernalhomadjunctionmap for iscapcategory isfunction\ 311", "X7BB46BD486E96939" ], 312 [ 313 "\033[2XInternalHomToTensorProductAdjunctionMap\033[102X for iscapcategoryo\ 314bject, iscapcategoryobject, iscapcategorymorphism", "1.4-14", [ 1, 4, 14 ], 315 608, 13, 316 "internalhomtotensorproductadjunctionmap for iscapcategoryobject iscapca\ 317tegoryobject iscapcategorymorphism", "X7A48DA157CCFB0B9" ], 318 [ 319 "\033[2XAddInternalHomToTensorProductAdjunctionMap\033[102X for iscapcatego\ 320ry, isfunction", "1.4-15", [ 1, 4, 15 ], 617, 13, 321 "addinternalhomtotensorproductadjunctionmap for iscapcategory isfunction\ 322", "X7C8C2DC381EA0962" ], 323 [ 324 "\033[2XMonoidalPreComposeMorphism\033[102X for iscapcategoryobject, iscapc\ 325ategoryobject, iscapcategoryobject", "1.4-16", [ 1, 4, 16 ], 627, 13, 326 "monoidalprecomposemorphism for iscapcategoryobject iscapcategoryobject \ 327iscapcategoryobject", "X86E4E97C82BFB45C" ], 328 [ 329 "\033[2XMonoidalPreComposeMorphismWithGivenObjects\033[102X for iscapcatego\ 330ryobject, iscapcategoryobject, iscapcategoryobject, iscapcategoryobject, iscap\ 331categoryobject", "1.4-17", [ 1, 4, 17 ], 638, 13, 332 "monoidalprecomposemorphismwithgivenobjects for iscapcategoryobject isca\ 333pcategoryobject iscapcategoryobject iscapcategoryobject iscapcategoryobject", 334 "X7FE4A52284060F20" ], 335 [ 336 "\033[2XAddMonoidalPreComposeMorphismWithGivenObjects\033[102X for iscapcat\ 337egory, isfunction", "1.4-18", [ 1, 4, 18 ], 651, 14, 338 "addmonoidalprecomposemorphismwithgivenobjects for iscapcategory isfunct\ 339ion", "X7A22CD657A2A338C" ], 340 [ 341 "\033[2XMonoidalPostComposeMorphism\033[102X for iscapcategoryobject, iscap\ 342categoryobject, iscapcategoryobject", "1.4-19", [ 1, 4, 19 ], 663, 14, 343 "monoidalpostcomposemorphism for iscapcategoryobject iscapcategoryobject\ 344 iscapcategoryobject", "X79F4FCE781385829" ], 345 [ 346 "\033[2XMonoidalPostComposeMorphismWithGivenObjects\033[102X for iscapcateg\ 347oryobject, iscapcategoryobject, iscapcategoryobject, iscapcategoryobject, isca\ 348pcategoryobject", "1.4-20", [ 1, 4, 20 ], 674, 14, 349 "monoidalpostcomposemorphismwithgivenobjects for iscapcategoryobject isc\ 350apcategoryobject iscapcategoryobject iscapcategoryobject iscapcategoryobject", 351 "X7E6933B8816EE4E3" ], 352 [ 353 "\033[2XAddMonoidalPostComposeMorphismWithGivenObjects\033[102X for iscapca\ 354tegory, isfunction", "1.4-21", [ 1, 4, 21 ], 687, 14, 355 "addmonoidalpostcomposemorphismwithgivenobjects for iscapcategory isfunc\ 356tion", "X7FC3725A7CF804F9" ], 357 [ "\033[2XDualOnObjects\033[102X for iscapcategoryobject", "1.4-22", 358 [ 1, 4, 22 ], 699, 14, "dualonobjects for iscapcategoryobject", 359 "X80FFC71D7E57DD53" ], 360 [ "\033[2XAddDualOnObjects\033[102X for iscapcategory, isfunction", 361 "1.4-23", [ 1, 4, 23 ], 706, 15, 362 "adddualonobjects for iscapcategory isfunction", "X7BB4DD5381EBF082" ], 363 [ "\033[2XDualOnMorphisms\033[102X for iscapcategorymorphism", "1.4-24", 364 [ 1, 4, 24 ], 715, 15, "dualonmorphisms for iscapcategorymorphism", 365 "X815C0BC47D000819" ], 366 [ 367 "\033[2XDualOnMorphismsWithGivenDuals\033[102X for iscapcategoryobject, isc\ 368apcategorymorphism, iscapcategoryobject", "1.4-25", [ 1, 4, 25 ], 723, 15, 369 "dualonmorphismswithgivenduals for iscapcategoryobject iscapcategorymorp\ 370hism iscapcategoryobject", "X7DCC0F468386AA46" ], 371 [ 372 "\033[2XAddDualOnMorphismsWithGivenDuals\033[102X for iscapcategory, isfunc\ 373tion", "1.4-26", [ 1, 4, 26 ], 732, 15, 374 "adddualonmorphismswithgivenduals for iscapcategory isfunction", 375 "X85DA12C581E673DE" ], 376 [ "\033[2XEvaluationForDual\033[102X for iscapcategoryobject", "1.4-27", 377 [ 1, 4, 27 ], 742, 15, "evaluationfordual for iscapcategoryobject", 378 "X86D42C7587F03A68" ], 379 [ 380 "\033[2XEvaluationForDualWithGivenTensorProduct\033[102X for iscapcategoryo\ 381bject, iscapcategoryobject, iscapcategoryobject", "1.4-28", [ 1, 4, 28 ], 382 750, 15, 383 "evaluationfordualwithgiventensorproduct for iscapcategoryobject iscapca\ 384tegoryobject iscapcategoryobject", "X7B588B1B8472834E" ], 385 [ 386 "\033[2XAddEvaluationForDualWithGivenTensorProduct\033[102X for iscapcatego\ 387ry, isfunction", "1.4-29", [ 1, 4, 29 ], 759, 15, 388 "addevaluationfordualwithgiventensorproduct for iscapcategory isfunction\ 389", "X7CB63A4E7E905CD4" ], 390 [ "\033[2XCoevaluationForDual\033[102X for iscapcategoryobject", "1.4-30", 391 [ 1, 4, 30 ], 769, 16, "coevaluationfordual for iscapcategoryobject", 392 "X83849B327C8074E9" ], 393 [ 394 "\033[2XCoevaluationForDualWithGivenTensorProduct\033[102X for iscapcategor\ 395yobject, iscapcategoryobject, iscapcategoryobject", "1.4-31", [ 1, 4, 31 ], 396 777, 16, 397 "coevaluationfordualwithgiventensorproduct for iscapcategoryobject iscap\ 398categoryobject iscapcategoryobject", "X7C65E6A97AAE0DE3" ], 399 [ 400 "\033[2XAddCoevaluationForDualWithGivenTensorProduct\033[102X for iscapcate\ 401gory, isfunction", "1.4-32", [ 1, 4, 32 ], 786, 16, 402 "addcoevaluationfordualwithgiventensorproduct for iscapcategory isfuncti\ 403on", "X831DC3947941E8BA" ], 404 [ "\033[2XMorphismToBidual\033[102X for iscapcategoryobject", "1.4-33", 405 [ 1, 4, 33 ], 796, 16, "morphismtobidual for iscapcategoryobject", 406 "X7F68B55781C1DFB1" ], 407 [ 408 "\033[2XMorphismToBidualWithGivenBidual\033[102X for iscapcategoryobject, i\ 409scapcategoryobject", "1.4-34", [ 1, 4, 34 ], 804, 16, 410 "morphismtobidualwithgivenbidual for iscapcategoryobject iscapcategoryob\ 411ject", "X79260E5680F1E741" ], 412 [ 413 "\033[2XAddMorphismToBidualWithGivenBidual\033[102X for iscapcategory, isfu\ 414nction", "1.4-35", [ 1, 4, 35 ], 812, 16, 415 "addmorphismtobidualwithgivenbidual for iscapcategory isfunction", 416 "X84C05B087EFCE599" ], 417 [ 418 "\033[2XTensorProductInternalHomCompatibilityMorphism\033[102X for iscapcat\ 419egoryobject, iscapcategoryobject, iscapcategoryobject, iscapcategoryobject", 420 "1.4-36", [ 1, 4, 36 ], 822, 17, 421 "tensorproductinternalhomcompatibilitymorphism for iscapcategoryobject i\ 422scapcategoryobject iscapcategoryobject iscapcategoryobject", 423 "X85FD880E7B76936C" ], 424 [ 425 "\033[2XTensorProductInternalHomCompatibilityMorphismWithGivenObjects\033[1\ 42602X for iscapcategoryobject, iscapcategoryobject, iscapcategoryobject, iscapca\ 427tegoryobject, islist", "1.4-37", [ 1, 4, 37 ], 835, 17, 428 "tensorproductinternalhomcompatibilitymorphismwithgivenobjects for iscap\ 429categoryobject iscapcategoryobject iscapcategoryobject iscapcategoryobject isl\ 430ist", "X7DDA8E317EF3078D" ], 431 [ 432 "\033[2XAddTensorProductInternalHomCompatibilityMorphismWithGivenObjects\\ 433033[102X for iscapcategory, isfunction", "1.4-38", [ 1, 4, 38 ], 850, 17, 434 "addtensorproductinternalhomcompatibilitymorphismwithgivenobjects for is\ 435capcategory isfunction", "X871C6B55843A0AF3" ], 436 [ 437 "\033[2XTensorProductDualityCompatibilityMorphism\033[102X for iscapcategor\ 438yobject, iscapcategoryobject", "1.4-39", [ 1, 4, 39 ], 864, 17, 439 "tensorproductdualitycompatibilitymorphism for iscapcategoryobject iscap\ 440categoryobject", "X7D173DB08132E40A" ], 441 [ 442 "\033[2XTensorProductDualityCompatibilityMorphismWithGivenObjects\033[102X \ 443for iscapcategoryobject, iscapcategoryobject, iscapcategoryobject, iscapcatego\ 444ryobject", "1.4-40", [ 1, 4, 40 ], 874, 17, 445 "tensorproductdualitycompatibilitymorphismwithgivenobjects for iscapcate\ 446goryobject iscapcategoryobject iscapcategoryobject iscapcategoryobject", 447 "X794ED97782B8DF76" ], 448 [ 449 "\033[2XAddTensorProductDualityCompatibilityMorphismWithGivenObjects\033[10\ 4502X for iscapcategory, isfunction", "1.4-41", [ 1, 4, 41 ], 885, 18, 451 "addtensorproductdualitycompatibilitymorphismwithgivenobjects for iscapc\ 452ategory isfunction", "X78D1B6AF8654A950" ], 453 [ 454 "\033[2XMorphismFromTensorProductToInternalHom\033[102X for iscapcategoryob\ 455ject, iscapcategoryobject", "1.4-42", [ 1, 4, 42 ], 896, 18, 456 "morphismfromtensorproducttointernalhom for iscapcategoryobject iscapcat\ 457egoryobject", "X8439BFF57BFE390F" ], 458 [ 459 "\033[2XMorphismFromTensorProductToInternalHomWithGivenObjects\033[102X for\ 460 iscapcategoryobject, iscapcategoryobject, iscapcategoryobject, iscapcategoryo\ 461bject", "1.4-43", [ 1, 4, 43 ], 906, 18, 462 "morphismfromtensorproducttointernalhomwithgivenobjects for iscapcategor\ 463yobject iscapcategoryobject iscapcategoryobject iscapcategoryobject", 464 "X8473D28B7F3A5E20" ], 465 [ 466 "\033[2XAddMorphismFromTensorProductToInternalHomWithGivenObjects\033[102X \ 467for iscapcategory, isfunction", "1.4-44", [ 1, 4, 44 ], 917, 18, 468 "addmorphismfromtensorproducttointernalhomwithgivenobjects for iscapcate\ 469gory isfunction", "X86D3AF4A80FA738D" ], 470 [ 471 "\033[2XIsomorphismFromTensorProductToInternalHom\033[102X for iscapcategor\ 472yobject, iscapcategoryobject", "1.4-45", [ 1, 4, 45 ], 928, 18, 473 "isomorphismfromtensorproducttointernalhom for iscapcategoryobject iscap\ 474categoryobject", "X7E88C05A78C378B3" ], 475 [ 476 "\033[2XAddIsomorphismFromTensorProductToInternalHom\033[102X for iscapcate\ 477gory, isfunction", "1.4-46", [ 1, 4, 46 ], 938, 19, 478 "addisomorphismfromtensorproducttointernalhom for iscapcategory isfuncti\ 479on", "X80A7C9A57D85D981" ], 480 [ 481 "\033[2XMorphismFromInternalHomToTensorProduct\033[102X for iscapcategoryob\ 482ject, iscapcategoryobject", "1.4-47", [ 1, 4, 47 ], 948, 19, 483 "morphismfrominternalhomtotensorproduct for iscapcategoryobject iscapcat\ 484egoryobject", "X7D189B8280CECBA2" ], 485 [ 486 "\033[2XMorphismFromInternalHomToTensorProductWithGivenObjects\033[102X for\ 487 iscapcategoryobject, iscapcategoryobject, iscapcategoryobject, iscapcategoryo\ 488bject", "1.4-48", [ 1, 4, 48 ], 959, 19, 489 "morphismfrominternalhomtotensorproductwithgivenobjects for iscapcategor\ 490yobject iscapcategoryobject iscapcategoryobject iscapcategoryobject", 491 "X7D10805D840AAC8D" ], 492 [ 493 "\033[2XAddMorphismFromInternalHomToTensorProductWithGivenObjects\033[102X \ 494for iscapcategory, isfunction", "1.4-49", [ 1, 4, 49 ], 971, 19, 495 "addmorphismfrominternalhomtotensorproductwithgivenobjects for iscapcate\ 496gory isfunction", "X7A4A4C668706D593" ], 497 [ 498 "\033[2XIsomorphismFromInternalHomToTensorProduct\033[102X for iscapcategor\ 499yobject, iscapcategoryobject", "1.4-50", [ 1, 4, 50 ], 982, 19, 500 "isomorphismfrominternalhomtotensorproduct for iscapcategoryobject iscap\ 501categoryobject", "X87A9E42D7F3FDEAD" ], 502 [ 503 "\033[2XAddIsomorphismFromInternalHomToTensorProduct\033[102X for iscapcate\ 504gory, isfunction", "1.4-51", [ 1, 4, 51 ], 993, 20, 505 "addisomorphismfrominternalhomtotensorproduct for iscapcategory isfuncti\ 506on", "X7EAC425A87FF2C0E" ], 507 [ "\033[2XTraceMap\033[102X for iscapcategorymorphism", "1.4-52", 508 [ 1, 4, 52 ], 1003, 20, "tracemap for iscapcategorymorphism", 509 "X85D0C9487A22AFFE" ], 510 [ "\033[2XAddTraceMap\033[102X for iscapcategory, isfunction", "1.4-53", 511 [ 1, 4, 53 ], 1011, 20, "addtracemap for iscapcategory isfunction", 512 "X8446431880FFF111" ], 513 [ "\033[2XRankMorphism\033[102X for iscapcategoryobject", "1.4-54", 514 [ 1, 4, 54 ], 1020, 20, "rankmorphism for iscapcategoryobject", 515 "X82F0DBD485D93793" ], 516 [ "\033[2XAddRankMorphism\033[102X for iscapcategory, isfunction", 517 "1.4-55", [ 1, 4, 55 ], 1028, 20, 518 "addrankmorphism for iscapcategory isfunction", "X849B17E08679450A" ], 519 [ "\033[2XIsomorphismFromDualToInternalHom\033[102X for iscapcategoryobject" 520 , "1.4-56", [ 1, 4, 56 ], 1037, 20, 521 "isomorphismfromdualtointernalhom for iscapcategoryobject", 522 "X7C8F7512785C7028" ], 523 [ 524 "\033[2XAddIsomorphismFromDualToInternalHom\033[102X for iscapcategory, isf\ 525unction", "1.4-57", [ 1, 4, 57 ], 1047, 21, 526 "addisomorphismfromdualtointernalhom for iscapcategory isfunction", 527 "X7882497883F6666A" ], 528 [ "\033[2XIsomorphismFromInternalHomToDual\033[102X for iscapcategoryobject" 529 , "1.4-58", [ 1, 4, 58 ], 1057, 21, 530 "isomorphismfrominternalhomtodual for iscapcategoryobject", 531 "X7E1B1DE47E838F75" ], 532 [ 533 "\033[2XAddIsomorphismFromInternalHomToDual\033[102X for iscapcategory, isf\ 534unction", "1.4-59", [ 1, 4, 59 ], 1067, 21, 535 "addisomorphismfrominternalhomtodual for iscapcategory isfunction", 536 "X7A91D0187FF3C50E" ], 537 [ 538 "\033[2XUniversalPropertyOfDual\033[102X for iscapcategoryobject, iscapcate\ 539goryobject, iscapcategorymorphism", "1.4-60", [ 1, 4, 60 ], 1077, 21, 540 "universalpropertyofdual for iscapcategoryobject iscapcategoryobject isc\ 541apcategorymorphism", "X7AF8F68887146C20" ], 542 [ "\033[2XAddUniversalPropertyOfDual\033[102X for iscapcategory, isfunction" 543 , "1.4-61", [ 1, 4, 61 ], 1086, 21, 544 "adduniversalpropertyofdual for iscapcategory isfunction", 545 "X7FCEDB3B7DF69A1E" ], 546 [ "\033[2XLambdaIntroduction\033[102X for iscapcategorymorphism", "1.4-62", 547 [ 1, 4, 62 ], 1096, 21, "lambdaintroduction for iscapcategorymorphism", 548 "X80F3F2287B9E55E3" ], 549 [ "\033[2XAddLambdaIntroduction\033[102X for iscapcategory, isfunction", 550 "1.4-63", [ 1, 4, 63 ], 1105, 22, 551 "addlambdaintroduction for iscapcategory isfunction", 552 "X84944B6283F2802A" ], 553 [ 554 "\033[2XLambdaElimination\033[102X for iscapcategoryobject, iscapcategoryob\ 555ject, iscapcategorymorphism", "1.4-64", [ 1, 4, 64 ], 1115, 22, 556 "lambdaelimination for iscapcategoryobject iscapcategoryobject iscapcate\ 557gorymorphism", "X79EC44077F661E80" ], 558 [ "\033[2XAddLambdaElimination\033[102X for iscapcategory, isfunction", 559 "1.4-65", [ 1, 4, 65 ], 1124, 22, 560 "addlambdaelimination for iscapcategory isfunction", 561 "X8406FBCD7EE968FF" ], 562 [ 563 "\033[2XIsomorphismFromObjectToInternalHom\033[102X for iscapcategoryobject\ 564", "1.4-66", [ 1, 4, 66 ], 1134, 22, 565 "isomorphismfromobjecttointernalhom for iscapcategoryobject", 566 "X8726BA888787D53D" ], 567 [ 568 "\033[2XIsomorphismFromObjectToInternalHomWithGivenInternalHom\033[102X for\ 569 iscapcategoryobject, iscapcategoryobject", "1.4-67", [ 1, 4, 67 ], 1142, 22, 570 "isomorphismfromobjecttointernalhomwithgiveninternalhom for iscapcategor\ 571yobject iscapcategoryobject", "X87F91EF37C76A7F7" ], 572 [ 573 "\033[2XAddIsomorphismFromObjectToInternalHomWithGivenInternalHom\033[102X \ 574for iscapcategory, isfunction", "1.4-68", [ 1, 4, 68 ], 1151, 22, 575 "addisomorphismfromobjecttointernalhomwithgiveninternalhom for iscapcate\ 576gory isfunction", "X78ED7FCC83D091AB" ], 577 [ 578 "\033[2XIsomorphismFromInternalHomToObject\033[102X for iscapcategoryobject\ 579", "1.4-69", [ 1, 4, 69 ], 1162, 23, 580 "isomorphismfrominternalhomtoobject for iscapcategoryobject", 581 "X831CF4E1824FA178" ], 582 [ 583 "\033[2XIsomorphismFromInternalHomToObjectWithGivenInternalHom\033[102X for\ 584 iscapcategoryobject, iscapcategoryobject", "1.4-70", [ 1, 4, 70 ], 1170, 23, 585 "isomorphismfrominternalhomtoobjectwithgiveninternalhom for iscapcategor\ 586yobject iscapcategoryobject", "X7988DC7C79BED3B2" ], 587 [ 588 "\033[2XAddIsomorphismFromInternalHomToObjectWithGivenInternalHom\033[102X \ 589for iscapcategory, isfunction", "1.4-71", [ 1, 4, 71 ], 1179, 23, 590 "addisomorphismfrominternalhomtoobjectwithgiveninternalhom for iscapcate\ 591gory isfunction", "X7D6421147BF6651B" ], 592 [ 593 "\033[2XTensorProductInternalHomCompatibilityMorphismInverse\033[102X for i\ 594scapcategoryobject, iscapcategoryobject, iscapcategoryobject, iscapcategoryobj\ 595ect", "1.5-1", [ 1, 5, 1 ], 1206, 23, 596 "tensorproductinternalhomcompatibilitymorphisminverse for iscapcategoryo\ 597bject iscapcategoryobject iscapcategoryobject iscapcategoryobject", 598 "X79374295858E884C" ], 599 [ 600 "\033[2XTensorProductInternalHomCompatibilityMorphismInverseWithGivenObject\ 601s\033[102X for iscapcategoryobject, iscapcategoryobject, iscapcategoryobject, \ 602iscapcategoryobject, islist", "1.5-2", [ 1, 5, 2 ], 1219, 23, 603 "tensorproductinternalhomcompatibilitymorphisminversewithgivenobjects fo\ 604r iscapcategoryobject iscapcategoryobject iscapcategoryobject iscapcategoryobj\ 605ect islist", "X7D5443AA7C591DDF" ], 606 [ 607 "\033[2XAddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObj\ 608ects\033[102X for iscapcategory, isfunction", "1.5-3", [ 1, 5, 3 ], 1234, 24, 609 "addtensorproductinternalhomcompatibilitymorphisminversewithgivenobjects\ 610 for iscapcategory isfunction", "X7D9EA11980170B0C" ], 611 [ "\033[2XMorphismFromBidual\033[102X for iscapcategoryobject", "1.5-4", 612 [ 1, 5, 4 ], 1248, 24, "morphismfrombidual for iscapcategoryobject", 613 "X7E02E8197EA201EA" ], 614 [ 615 "\033[2XMorphismFromBidualWithGivenBidual\033[102X for iscapcategoryobject,\ 616 iscapcategoryobject", "1.5-5", [ 1, 5, 5 ], 1256, 24, 617 "morphismfrombidualwithgivenbidual for iscapcategoryobject iscapcategory\ 618object", "X785CF0BB7BC0AC0D" ], 619 [ 620 "\033[2XAddMorphismFromBidualWithGivenBidual\033[102X for iscapcategory, is\ 621function", "1.5-6", [ 1, 5, 6 ], 1265, 24, 622 "addmorphismfrombidualwithgivenbidual for iscapcategory isfunction", 623 "X877C409E865C2BB3" ] ] 624); 625