OAI/CategoryTheory/Globular/Tree.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Grothendieck.GlobularTheory.Model.smallFreeDescCells line 11
  2. theorem OAI.Grothendieck.GlobularTheory.Model.smallFreeDescCells_gen line 22
  3. theorem OAI.Grothendieck.GlobularTheory.Model.smallFreeCell_face line 28
  4. abbrev OAI.Grothendieck.GlobularTheory.Model.linearFree line 51
  5. def OAI.Grothendieck.GlobularTheory.Model.linLow line 55
  6. def OAI.Grothendieck.GlobularTheory.Model.linEdge line 60
  7. def OAI.Grothendieck.GlobularTheory.Model.linMiddle line 65
  8. theorem OAI.Grothendieck.GlobularTheory.Model.linMiddle_source line 70
  9. theorem OAI.Grothendieck.GlobularTheory.Model.linMiddle_target line 91
  10. theorem OAI.Grothendieck.GlobularTheory.Model.linLow_face line 112
  11. theorem OAI.Grothendieck.GlobularTheory.Model.linEdge_face line 120
  12. def OAI.Grothendieck.GlobularTheory.Model.linOriginal line 128
  13. theorem OAI.Grothendieck.GlobularTheory.Model.linOriginal_low line 145
  14. theorem OAI.Grothendieck.GlobularTheory.Model.linOriginal_center line 151
  15. theorem OAI.Grothendieck.GlobularTheory.Model.linOriginal_high line 158
  16. theorem OAI.Grothendieck.GlobularTheory.Model.linOriginal_source line 167
  17. theorem OAI.Grothendieck.GlobularTheory.Model.linOriginal_target line 191
  18. def OAI.Grothendieck.GlobularTheory.Model.whiskerToLinearCell line 215
  19. theorem OAI.Grothendieck.GlobularTheory.Model.whiskerToLinearCell_source line 225
  20. theorem OAI.Grothendieck.GlobularTheory.Model.whiskerToLinearCell_target line 238
  21. abbrev OAI.Grothendieck.GlobularTheory.Model.whiskerFree line 251
  22. def OAI.Grothendieck.GlobularTheory.Model.whiskerToLinear line 255
  23. def OAI.Grothendieck.GlobularTheory.Model.wBase line 272
  24. def OAI.Grothendieck.GlobularTheory.Model.wEdge line 277
  25. theorem OAI.Grothendieck.GlobularTheory.Model.wBase_source line 282
  26. theorem OAI.Grothendieck.GlobularTheory.Model.wBase_target line 291
  27. theorem OAI.Grothendieck.GlobularTheory.Model.wEdge_source line 300
  28. def OAI.Grothendieck.GlobularTheory.Model.wMiddle line 308
  29. theorem OAI.Grothendieck.GlobularTheory.Model.wMiddle_source line 315
  30. theorem OAI.Grothendieck.GlobularTheory.Model.wMiddle_target line 322
  31. def OAI.Grothendieck.GlobularTheory.Model.wTriple line 329
  32. def OAI.Grothendieck.GlobularTheory.Model.linReverseBlock line 337
  33. theorem OAI.Grothendieck.GlobularTheory.Model.linReverseBlock_low line 353
  34. theorem OAI.Grothendieck.GlobularTheory.Model.linReverseBlock_center line 362
  35. theorem OAI.Grothendieck.GlobularTheory.Model.linReverseBlock_high line 371
  36. theorem OAI.Grothendieck.GlobularTheory.Model.transportedShapeDesc line 380
  37. theorem OAI.Grothendieck.GlobularTheory.Model.linReverseBlock_adjacent line 394
  38. def OAI.Grothendieck.GlobularTheory.Model.linearToWhisker line 432
  39. theorem OAI.Grothendieck.GlobularTheory.Model.cancelShapeTransport line 442
  40. theorem OAI.Grothendieck.GlobularTheory.Model.linearToWhisker_lowHom line 450
  41. theorem OAI.Grothendieck.GlobularTheory.Model.linearToWhisker_edgeHom line 459
  42. theorem OAI.Grothendieck.GlobularTheory.Model.linearToWhisker_tripleHom line 467
  43. theorem OAI.Grothendieck.GlobularTheory.Model.smallFreeCell_image line 475
  44. theorem OAI.Grothendieck.GlobularTheory.Model.linearToWhisker_low line 490
  45. theorem OAI.Grothendieck.GlobularTheory.Model.linearToWhisker_edge line 496
  46. theorem OAI.Grothendieck.GlobularTheory.Model.linearToWhisker_middle line 502
  47. theorem OAI.Grothendieck.GlobularTheory.Model.compCell_cancel_left line 523
  48. theorem OAI.Grothendieck.GlobularTheory.Model.whiskerToLinear_gen line 540
  49. theorem OAI.Grothendieck.GlobularTheory.Model.wEdge_target line 547
  50. theorem OAI.Grothendieck.GlobularTheory.Model.whiskerLinear_low line 556
  51. theorem OAI.Grothendieck.GlobularTheory.Model.whiskerLinear_top line 583
  52. theorem OAI.Grothendieck.GlobularPresheaf.disk_bounded line 617
  53. theorem OAI.Grothendieck.Table.bounded line 630
  54. theorem OAI.Grothendieck.GlobularTheory.Model.whiskerFree_bounded_hasFillers line 648