OAI/CategoryTheory/Globular/Composition.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Grothendieck.GlobularTheory.Model.sumTuple_ext line 11
  2. theorem OAI.Grothendieck.GlobularTheory.Model.map_compositionTuple line 18
  3. theorem OAI.Grothendieck.GlobularTheory.Model.map_compCell line 32
  4. def OAI.Grothendieck.GlobularTheory.Model.tupleMap line 41
  5. theorem OAI.Grothendieck.GlobularTheory.Model.tupleMap_app line 45
  6. theorem OAI.Grothendieck.GlobularTheory.Model.joined_of_parallel_expressions line 50
  7. def OAI.Grothendieck.GlobularTheory.Model.topCell line 58
  8. theorem OAI.Grothendieck.GlobularTheory.Model.tupleMap_topCell line 61
  9. theorem OAI.Grothendieck.GlobularTheory.Model.compCell_left_unit line 66
  10. theorem OAI.Grothendieck.GlobularTheory.Model.compCell_right_unit line 84
  11. theorem OAI.Grothendieck.GlobularTheory.Model.compCell_inverse_right line 102
  12. theorem OAI.Grothendieck.GlobularTheory.Model.compCell_inverse_left line 121
  13. theorem OAI.Grothendieck.GlobularSet.Hom.boundaryMap_id line 145
  14. theorem OAI.Grothendieck.GlobularSet.HasFillers.joined line 153
  15. theorem OAI.Grothendieck.GlobularSet.HasFillers.retract line 158
  16. theorem OAI.Grothendieck.GlobularSet.hasFillers_of_endpoint_factorization line 165
  17. def OAI.Grothendieck.GlobularSet.LiftsSource line 177
  18. theorem OAI.Grothendieck.GlobularSet.liftsBoundary_of_contractible line 181
  19. theorem OAI.Grothendieck.Shape.attach_seam line 204
  20. def OAI.Grothendieck.GlobularTheory.tripleShape line 212
  21. def OAI.Grothendieck.GlobularTheory.tripleFirst line 215
  22. def OAI.Grothendieck.GlobularTheory.tripleMiddle line 218
  23. def OAI.Grothendieck.GlobularTheory.tripleLast line 221
  24. theorem OAI.Grothendieck.GlobularTheory.triple_first_middle line 224
  25. theorem OAI.Grothendieck.GlobularTheory.triple_middle_last line 231
  26. def OAI.Grothendieck.GlobularTheory.Model.tripleTuple line 240
  27. theorem OAI.Grothendieck.GlobularTheory.Model.tripleTuple_first line 251
  28. theorem OAI.Grothendieck.GlobularTheory.Model.tripleTuple_middle line 264
  29. theorem OAI.Grothendieck.GlobularTheory.Model.tripleTuple_last line 277
  30. theorem OAI.Grothendieck.GlobularTheory.Model.compCell_assoc line 284