OAI/CategoryTheory/Globular/Boundary.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Grothendieck.Shape.face_two_source line 12
  2. theorem OAI.Grothendieck.Shape.globe_seam_general line 17
  3. theorem OAI.Grothendieck.GlobularTheory.Model.compCell_congr_left line 24
  4. theorem OAI.Grothendieck.GlobularTheory.Model.compCell_congr_right line 75
  5. def OAI.Grothendieck.GlobularTheory.Model.targetDisk line 134
  6. theorem OAI.Grothendieck.GlobularTheory.Model.cellEquiv_targetDisk line 140
  7. structure OAI.Grothendieck.GlobularTheory.Model.BoundaryRepresentation line 147
  8. def OAI.Grothendieck.GlobularTheory.Model.BoundaryRepresentation.zero line 158
  9. abbrev OAI.Grothendieck.GlobularTheory.Model.BoundaryRepresentation.nextObj line 171
  10. def OAI.Grothendieck.GlobularTheory.Model.BoundaryRepresentation.nextValue line 173
  11. theorem OAI.Grothendieck.GlobularTheory.Model.BoundaryRepresentation.nextValue_bijective line 180
  12. theorem OAI.Grothendieck.GlobularTheory.Model.BoundaryRepresentation.face_condition line 201
  13. def OAI.Grothendieck.GlobularTheory.Model.BoundaryRepresentation.succ line 215
  14. def OAI.Grothendieck.GlobularTheory.Model.boundaryRepresentation line 234
  15. abbrev OAI.Grothendieck.GlobularTheory.Model.boundaryDisk line 239
  16. abbrev OAI.Grothendieck.GlobularTheory.Model.I line 242
  17. theorem OAI.Grothendieck.GlobularTheory.Model.hasLiftingProperty_I_iff line 247
  18. theorem OAI.Grothendieck.GlobularTheory.Model.liftsBoundaries_iff line 286
  19. theorem OAI.Grothendieck.GlobularTheory.Model.hasLiftingProperty_J_iff line 290