OAI/CategoryTheory/Globular/Fillers.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Grothendieck.GlobularTheory.Model.freeShapeMap line 13
  2. theorem OAI.Grothendieck.GlobularTheory.Model.freeShapeMap_low_bijective line 17
  3. def OAI.Grothendieck.GlobularSet.HasFillers line 44
  4. theorem OAI.Grothendieck.GlobularSet.Hom.reflects_parallel_of_low line 46
  5. theorem OAI.Grothendieck.GlobularSet.Hom.boundaryMap_bijective_of_low line 56
  6. theorem OAI.Grothendieck.GlobularSet.HasFillers.of_low_bijective line 76
  7. theorem OAI.Grothendieck.GlobularTheory.Model.freeShape_joined line 92
  8. theorem OAI.Grothendieck.GlobularTheory.Model.freeShape_hasFillers line 114
  9. theorem OAI.Grothendieck.GlobularTheory.Model.cutoff_freeShape_hasFillers line 131
  10. def OAI.Grothendieck.GlobularTheory.Model.presheafFunctor line 147
  11. def OAI.Grothendieck.GlobularTheory.Model.forgetGlobular line 151
  12. def OAI.Grothendieck.GlobularTheory.Model.presheafReflection line 154
  13. def OAI.Grothendieck.GlobularTheory.Model.freePresheaf line 159
  14. def OAI.Grothendieck.GlobularTheory.Model.presheafAdjunction line 164
  15. def OAI.Grothendieck.GlobularTheory.Model.freeGlobular line 170
  16. def OAI.Grothendieck.GlobularTheory.Model.globularAdjunction line 173
  17. instance OAI.Grothendieck.GlobularTheory.Model.freeGlobular_preservesColimits line 177
  18. def OAI.Grothendieck.GlobularTheory.composition line 188
  19. theorem OAI.Grothendieck.GlobularTheory.composition_source line 192
  20. theorem OAI.Grothendieck.GlobularTheory.composition_target line 197
  21. def OAI.Grothendieck.GlobularTheory.inverse line 202
  22. theorem OAI.Grothendieck.GlobularTheory.inverse_source line 206
  23. theorem OAI.Grothendieck.GlobularTheory.inverse_target line 210
  24. theorem OAI.Grothendieck.GlobularTheory.Model.map_eval line 216
  25. def OAI.Grothendieck.GlobularTheory.Model.sumTuple line 223
  26. theorem OAI.Grothendieck.GlobularTheory.Model.sumTuple_left line 230
  27. theorem OAI.Grothendieck.GlobularTheory.Model.sumTuple_right line 237
  28. def OAI.Grothendieck.GlobularTheory.Model.compositionTuple line 244
  29. theorem OAI.Grothendieck.GlobularTheory.Model.compositionTuple_left line 250
  30. theorem OAI.Grothendieck.GlobularTheory.Model.compositionTuple_right line 255
  31. def OAI.Grothendieck.GlobularTheory.Model.compCell line 260
  32. theorem OAI.Grothendieck.GlobularTheory.Model.compCell_source line 264
  33. theorem OAI.Grothendieck.GlobularTheory.Model.compCell_target line 271
  34. def OAI.Grothendieck.GlobularTheory.Model.inverseCell line 278
  35. theorem OAI.Grothendieck.GlobularTheory.Model.inverseCell_source line 281
  36. theorem OAI.Grothendieck.GlobularTheory.Model.inverseCell_target line 289
  37. theorem OAI.Grothendieck.GlobularTheory.Model.map_inverseCell line 297