OAI/CategoryTheory/Globular/Model.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Grothendieck.GlobularSet line 9

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:9 (same declaration text).

  2. structure OAI.Grothendieck.GlobularSet.Hom line 19

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:19 (same declaration text).

  3. def OAI.Grothendieck.GlobularSet.Parallel line 24

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:24 (same declaration text).

  4. def OAI.Grothendieck.GlobularSet.Joined line 28

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:28 (same declaration text).

  5. theorem OAI.Grothendieck.GlobularSet.Joined.parallel line 31
  6. theorem OAI.Grothendieck.GlobularSet.Hom.map_joined line 38
  7. def OAI.Grothendieck.GlobularSet.Boundary line 43

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:31 (same declaration text).

  8. def OAI.Grothendieck.GlobularSet.boundary line 47

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:35 (same declaration text).

  9. theorem OAI.Grothendieck.GlobularSet.Hom.map_parallel line 54
  10. def OAI.Grothendieck.GlobularSet.Hom.boundaryMap line 64

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:42 (same declaration text).

  11. structure OAI.Grothendieck.Globe line 78

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:56 (same declaration text).

  12. inductive OAI.Grothendieck.Globe.Face line 83

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:61 (same declaration text).

  13. def OAI.Grothendieck.Globe.Face.comp line 89

    Distinct definitions of this name: ComparatorChallenges/GrothendieckElementaryExpansion.lean:67 (different declaration text). Qualify references as OAI.Grothendieck.Globe.Face.comp@path.

  14. theorem OAI.Grothendieck.Globe.Face.id_comp line 95
  15. theorem OAI.Grothendieck.Globe.Face.comp_id line 98
  16. theorem OAI.Grothendieck.Globe.Face.assoc line 100
  17. instance OAI.Grothendieck.Globe.(instance at line 106) line 106
  18. def OAI.Grothendieck.Globe.face line 116

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:84 (same declaration text).

  19. def OAI.Grothendieck.Globe.source line 119

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:87 (same declaration text).

  20. def OAI.Grothendieck.Globe.target line 121

    Distinct definitions of this name: ComparatorChallenges/GrothendieckElementaryExpansion.lean:89 (same statement text; different proof or body). Qualify references as OAI.Grothendieck.Globe.target@path.

  21. theorem OAI.Grothendieck.Globe.source_source line 124
  22. theorem OAI.Grothendieck.Globe.target_source line 127
  23. abbrev OAI.Grothendieck.GlobularPresheaf line 131

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:93 (same declaration text).

  24. def OAI.Grothendieck.GlobularPresheaf.underlying line 135

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:97 (same declaration text).

  25. def OAI.Grothendieck.GlobularPresheaf.underlyingMap line 146

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:108 (same declaration text).

  26. def OAI.Grothendieck.GlobularPresheaf.disk line 153

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:115 (same declaration text).

  27. def OAI.Grothendieck.GlobularPresheaf.face line 155

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:117 (same declaration text).

  28. inductive OAI.Grothendieck.Table line 160

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:122 (same declaration text).

  29. def OAI.Grothendieck.Table.height line 166

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:128 (same declaration text).

  30. def OAI.Grothendieck.Table.realizeWithLast line 170

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:132 (same declaration text).

  31. def OAI.Grothendieck.Table.realize line 179

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:141 (same declaration text).

  32. def OAI.Grothendieck.Table.lastInclusion line 181

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:143 (same declaration text).

  33. abbrev OAI.Grothendieck.Shape line 186

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:148 (same declaration text).

  34. def OAI.Grothendieck.Shape.realize line 190

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:152 (same declaration text).

  35. def OAI.Grothendieck.Shape.height line 192

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:154 (same declaration text).

  36. def OAI.Grothendieck.Shape.globe line 194

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:156 (same declaration text).

  37. instance OAI.Grothendieck.Shape.(instance at line 196) line 196
  38. def OAI.Grothendieck.Shape.face line 205

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:166 (same declaration text).

  39. def OAI.Grothendieck.Shape.source line 208

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:169 (same declaration text).

  40. def OAI.Grothendieck.Shape.target line 210

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:171 (same declaration text).

  41. def OAI.Grothendieck.Shape.attach line 212

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:173 (same declaration text).

  42. def OAI.Grothendieck.Shape.seam line 215

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:176 (same declaration text).

  43. def OAI.Grothendieck.Shape.inl line 219

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:180 (same declaration text).

  44. def OAI.Grothendieck.Shape.inr line 224

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:185 (same declaration text).

  45. structure OAI.Grothendieck.TheoryData line 231

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:192 (same declaration text).

  46. structure OAI.Grothendieck.TheoryData.Obj line 245

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:206 (same declaration text).

  47. instance OAI.Grothendieck.TheoryData.(instance at line 248) line 248
  48. def OAI.Grothendieck.TheoryData.arity line 256

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:217 (same declaration text).

  49. def OAI.Grothendieck.TheoryData.PreservesGlobularSums line 262

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:223 (same declaration text).

  50. structure OAI.Grothendieck.GlobularTheory line 269

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:230 (same declaration text).

  51. abbrev OAI.Grothendieck.GlobularTheory.Obj line 274

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:235 (same declaration text).

  52. structure OAI.Grothendieck.GlobularTheory.Morphism line 277

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:238 (same declaration text).

  53. def OAI.Grothendieck.GlobularTheory.Morphism.id line 286

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:247 (same declaration text).

  54. def OAI.Grothendieck.GlobularTheory.Morphism.comp line 292

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:253 (same declaration text).

  55. def OAI.Grothendieck.GlobularTheory.Parallel line 300

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:261 (same declaration text).

  56. structure OAI.Grothendieck.GlobularTheory.AdmissiblePair line 307

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:268 (same declaration text).

  57. def OAI.Grothendieck.GlobularTheory.Fills line 315

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:276 (same declaration text).

  58. def OAI.Grothendieck.GlobularTheory.IsFreeExtension line 320

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:281 (same declaration text).

  59. structure OAI.Grothendieck.GlobularTheory.CellularPresentation line 329

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:290 (same declaration text).

  60. def OAI.Grothendieck.GlobularTheory.IsCoherator line 343

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:304 (same declaration text).

  61. def OAI.Grothendieck.GlobularTheory.shapeGlobes line 348

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:308 (same declaration text).

  62. def OAI.Grothendieck.GlobularTheory.globes line 354

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:314 (same declaration text).

  63. structure OAI.Grothendieck.GlobularTheory.Model line 357

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:317 (same declaration text).

  64. instance OAI.Grothendieck.GlobularTheory.Model.(instance at line 368) line 368
  65. def OAI.Grothendieck.GlobularTheory.Model.underlying line 376

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:336 (same declaration text).

  66. def OAI.Grothendieck.GlobularTheory.Model.underlyingMap line 379

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:339 (same declaration text).

  67. def OAI.Grothendieck.GlobularTheory.Model.freeShape line 383

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:343 (same declaration text).

  68. def OAI.Grothendieck.GlobularTheory.Model.disk line 387

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:347 (same declaration text).

  69. def OAI.Grothendieck.GlobularTheory.Model.J line 390

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:350 (same declaration text).

  70. structure OAI.Grothendieck.GlobularTheory.Model.BoundaryAttachment line 394

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:354 (same declaration text).

  71. structure OAI.Grothendieck.GlobularTheory.Model.CellularPresentation line 406

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:366 (same declaration text).

  72. def OAI.Grothendieck.GlobularTheory.Model.IsCellular line 420

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:380 (same declaration text).

  73. def OAI.Grothendieck.GlobularTheory.unitPair line 424

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:384 (same declaration text).

  74. def OAI.Grothendieck.GlobularTheory.unit line 432

    Also declared: ComparatorChallenges/GrothendieckElementaryExpansion.lean:392 (same declaration text).

  75. def OAI.Grothendieck.GlobularTheory.Model.eval line 439

    Distinct definitions of this name: ComparatorChallenges/GrothendieckElementaryExpansion.lean:395 (different declaration text). Qualify references as OAI.Grothendieck.GlobularTheory.Model.eval@path.

  76. def OAI.Grothendieck.GlobularTheory.Model.unitCell line 443

    Distinct definitions of this name: ComparatorChallenges/GrothendieckElementaryExpansion.lean:399 (different declaration text). Qualify references as OAI.Grothendieck.GlobularTheory.Model.unitCell@path.

  77. def OAI.Grothendieck.GlobularTheory.Model.baseCell line 447

    Distinct definitions of this name: ComparatorChallenges/GrothendieckElementaryExpansion.lean:403 (different declaration text). Qualify references as OAI.Grothendieck.GlobularTheory.Model.baseCell@path.

  78. theorem OAI.Grothendieck.GlobularTheory.Model.map_unitCell line 452
  79. theorem OAI.Grothendieck.GlobularTheory.Model.map_baseCell line 460
  80. def OAI.Grothendieck.GlobularTheory.Model.Loops line 468

    Distinct definitions of this name: ComparatorChallenges/GrothendieckElementaryExpansion.lean:408 (different declaration text). Qualify references as OAI.Grothendieck.GlobularTheory.Model.Loops@path.

  81. def OAI.Grothendieck.GlobularTheory.Model.Components line 473

    Distinct definitions of this name: ComparatorChallenges/GrothendieckElementaryExpansion.lean:413 (different declaration text). Qualify references as OAI.Grothendieck.GlobularTheory.Model.Components@path.

  82. def OAI.Grothendieck.GlobularTheory.Model.HomotopyGroup line 476

    Distinct definitions of this name: ComparatorChallenges/GrothendieckElementaryExpansion.lean:416 (different declaration text). Qualify references as OAI.Grothendieck.GlobularTheory.Model.HomotopyGroup@path.

  83. def OAI.Grothendieck.GlobularTheory.Model.loopsMap line 480

    Distinct definitions of this name: ComparatorChallenges/GrothendieckElementaryExpansion.lean:420 (different declaration text). Qualify references as OAI.Grothendieck.GlobularTheory.Model.loopsMap@path.

  84. def OAI.Grothendieck.GlobularTheory.Model.componentsMap line 499

    Distinct definitions of this name: ComparatorChallenges/GrothendieckElementaryExpansion.lean:439 (different declaration text). Qualify references as OAI.Grothendieck.GlobularTheory.Model.componentsMap@path.

  85. def OAI.Grothendieck.GlobularTheory.Model.homotopyMap line 507

    Distinct definitions of this name: ComparatorChallenges/GrothendieckElementaryExpansion.lean:447 (different declaration text). Qualify references as OAI.Grothendieck.GlobularTheory.Model.homotopyMap@path.

  86. def OAI.Grothendieck.GlobularTheory.Model.WeakEquivalence line 516

    Distinct definitions of this name: ComparatorChallenges/GrothendieckElementaryExpansion.lean:456 (different declaration text). Qualify references as OAI.Grothendieck.GlobularTheory.Model.WeakEquivalence@path.