OAI/CategoryTheory/Thomason/CylinderAssociativity.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Cylinder Associativity.

  1. lemma OAI.Thomason.GrayRecursive.hom_join_val line 15
  2. structure OAI.Thomason.GrayRecursive.CylinderComposition line 22
  3. lemma OAI.Thomason.GrayRecursive.CylinderComposition.endpoint line 31
  4. lemma OAI.Thomason.GrayRecursive.zeroFaceMatching_seam line 48
  5. def OAI.Thomason.GrayRecursive.cylinderCompositionZero line 54
  6. def OAI.Thomason.GrayRecursive.CylinderComposition.secondDiagonal line 65
  7. lemma OAI.Thomason.GrayRecursive.CylinderComposition.diagonal_matching line 69
  8. def OAI.Thomason.GrayRecursive.CylinderComposition.positiveEnds line 77
  9. lemma OAI.Thomason.GrayRecursive.CylinderComposition.positiveEnds_vertex line 81
  10. def OAI.Thomason.GrayRecursive.CylinderComposition.positiveDiagram line 85
  11. def OAI.Thomason.GrayRecursive.CylinderComposition.succ line 144
  12. def OAI.Thomason.GrayRecursive.cylinderComposition line 154
  13. abbrev OAI.Thomason.GrayRecursive.pasteCylinder line 171
  14. lemma OAI.Thomason.GrayRecursive.pasteCylinder_endpoint_top line 175
  15. lemma OAI.Thomason.GrayRecursive.pasteCylinder_endpoint line 181
  16. lemma OAI.Thomason.GrayRecursive.pasteCylinder_zero line 190
  17. lemma OAI.Thomason.GrayRecursive.pasteCylinder_succ_edge line 195
  18. lemma OAI.Thomason.GrayRecursive.pasteCylinder_succ_up line 200
  19. lemma OAI.Thomason.GrayRecursive.pasteCylinder_natural line 207
  20. lemma OAI.Thomason.GrayRecursive.globeSuspended_ext line 254
  21. lemma OAI.Thomason.GrayRecursive.constantInterval_faceMatching line 269
  22. lemma OAI.Thomason.GrayRecursive.pasteCylinder_constant line 288
  23. lemma OAI.Thomason.GrayRecursive.pushout_faceMatching line 367
  24. def OAI.Thomason.GrayRecursive.cooperation line 372
  25. lemma OAI.Thomason.GrayRecursive.cooperation_endpoint line 375
  26. lemma OAI.Thomason.GrayRecursive.pushout_globe_composition line 398
  27. lemma OAI.Thomason.GrayRecursive.cooperation_projection line 404
  28. theorem OAI.Thomason.GrayRecursive.cooperationExists_all line 423
  29. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.ext line 437
  30. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.ofFunctor_lift line 449
  31. lemma OAI.Thomason.GrayRecursive.IntervalMatching.concat_left line 464
  32. lemma OAI.Thomason.GrayRecursive.IntervalMatching.concat_right line 469
  33. lemma OAI.Thomason.GrayRecursive.IntervalMatching.natural line 474
  34. abbrev OAI.Thomason.GrayRecursive.pairFunctor line 480
  35. lemma OAI.Thomason.GrayRecursive.concatInterval_pair line 483
  36. lemma OAI.Thomason.GrayRecursive.IntervalMatching.pair line 499
  37. lemma OAI.Thomason.GrayRecursive.concatInterval_homCompose line 510
  38. lemma OAI.Thomason.GrayRecursive.IntervalMatching.constantAt line 536
  39. lemma OAI.Thomason.GrayRecursive.concatInterval_constantAt line 541
  40. lemma OAI.Thomason.GrayRecursive.concatInterval_val_congr line 547
  41. lemma OAI.Thomason.GrayRecursive.concatInterval_homCompose_left line 563
  42. lemma OAI.Thomason.GrayRecursive.concatInterval_homCompose_right line 576
  43. def OAI.Thomason.GrayRecursive.IntervalAssociative line 600
  44. def OAI.Thomason.GrayRecursive.RectangleDiagram.assocLeft line 612
  45. def OAI.Thomason.GrayRecursive.RectangleDiagram.assocRight line 617
  46. def OAI.Thomason.GrayRecursive.RectangleDiagram.assocA line 622
  47. def OAI.Thomason.GrayRecursive.RectangleDiagram.assocB line 623
  48. def OAI.Thomason.GrayRecursive.RectangleDiagram.assocC line 624
  49. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.assocB_map line 626
  50. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.assocAB line 635
  51. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.assocBC line 642
  52. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.concat_one_assoc line 650
  53. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.concat_two_assoc line 660
  54. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.concat_one_assoc' line 675
  55. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.concat_two_assoc' line 683
  56. lemma OAI.Thomason.GrayRecursive.RectangleDiagram.concat_assoc line 694
  57. lemma OAI.Thomason.GrayRecursive.concatInterval_associative line 714