OAI/CategoryTheory/Globular/BoundaryCells.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Grothendieck.GlobularSet.LiftStage.evalFace_app line 11
  2. def OAI.Grothendieck.GlobularFrame.diskDiagram line 31
  3. theorem OAI.Grothendieck.GlobularFrame.diskDiagram_cell line 51
  4. def OAI.Grothendieck.GlobularFrame.boundaryCell line 61
  5. theorem OAI.Grothendieck.GlobularFrame.boundaryCell_top line 65
  6. theorem OAI.Grothendieck.GlobularFrame.boundaryCell_low line 68
  7. theorem OAI.Grothendieck.GlobularFrame.boundaryCell_inc line 73
  8. theorem OAI.Grothendieck.GlobularFrame.boundaryCell_adjacent line 83
  9. def OAI.Grothendieck.GlobularFrame.boundaryApp line 103
  10. theorem OAI.Grothendieck.GlobularFrame.boundaryApp_face line 111
  11. theorem OAI.Grothendieck.GlobularFrame.boundaryApp_source line 114
  12. theorem OAI.Grothendieck.GlobularFrame.boundaryApp_target line 123
  13. theorem OAI.Grothendieck.GlobularFrame.boundaryApp_inc line 133
  14. theorem OAI.Grothendieck.GlobularFrame.Hom.face_naturality line 146
  15. theorem OAI.Grothendieck.GlobularFrame.Hom.boundaryCell_naturality line 159
  16. theorem OAI.Grothendieck.GlobularFrame.Hom.boundaryApp_naturality line 172