OAI/CategoryTheory/Globular/Cutoff.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Grothendieck.GlobularTheory.Model.components_eq_iff line 13
  2. theorem OAI.Grothendieck.GlobularTheory.Model.loops_joined_equivalence line 19
  3. theorem OAI.Grothendieck.GlobularTheory.Model.weakEquivalence_of_exactBoundaryTest line 25
  4. def OAI.Grothendieck.GlobularSet.cutoffCell line 70
  5. def OAI.Grothendieck.GlobularSet.cutoffFace line 73
  6. theorem OAI.Grothendieck.GlobularSet.cutoffCell_low line 87
  7. theorem OAI.Grothendieck.GlobularSet.cutoffCell_high line 90
  8. theorem OAI.Grothendieck.GlobularSet.cutoffFace_low line 93
  9. theorem OAI.Grothendieck.GlobularSet.cutoffFace_seam line 98
  10. theorem OAI.Grothendieck.GlobularSet.comp_eq_of_heq line 104
  11. def OAI.Grothendieck.GlobularSet.cutoff line 113
  12. theorem OAI.Grothendieck.GlobularTheory.Model.underlyingMap_id line 159
  13. theorem OAI.Grothendieck.GlobularTheory.Model.underlyingMap_comp line 163
  14. theorem OAI.Grothendieck.GlobularTheory.Model.BoundaryAttachment.hasLiftingProperty line 167
  15. theorem OAI.Grothendieck.GlobularTheory.Model.section_of_isCellular line 197
  16. def OAI.Grothendieck.GlobularTheory.Model.unitMap line 222
  17. theorem OAI.Grothendieck.GlobularTheory.Model.J_comp_unitMap line 228
  18. theorem OAI.Grothendieck.GlobularTheory.Model.elementary_pushout_retraction line 238
  19. theorem OAI.Grothendieck.GlobularTheory.Model.weakEquivalence_of_partialPath_data line 246
  20. def OAI.Grothendieck.GlobularSet.faceMap line 313
  21. theorem OAI.Grothendieck.GlobularSet.faceMap_succ line 319
  22. theorem OAI.Grothendieck.GlobularSet.faceMap_source line 323
  23. theorem OAI.Grothendieck.GlobularSet.faceMap_target line 329
  24. theorem OAI.Grothendieck.GlobularSet.faceMap_comp line 341
  25. def OAI.Grothendieck.GlobularSet.evalFace line 355
  26. theorem OAI.Grothendieck.GlobularSet.evalFace_comp line 359
  27. def OAI.Grothendieck.GlobularSet.presheaf line 369