OAI/CategoryTheory/Globular/LinearCells.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Grothendieck.FiniteCoGlobularObject.cell line 12
  2. theorem OAI.Grothendieck.FiniteCoGlobularObject.cell_face line 17
  3. instance OAI.Grothendieck.FiniteCoGlobularObject.preservesColimits_realization line 32
  4. def OAI.Grothendieck.Shape.linearLow line 40
  5. def OAI.Grothendieck.Shape.linearEdge line 45
  6. def OAI.Grothendieck.Shape.linearTriple line 50
  7. theorem OAI.Grothendieck.Shape.linearLow_face line 55
  8. theorem OAI.Grothendieck.Shape.linearEdge_face line 68
  9. theorem OAI.Grothendieck.Shape.linearTriple_face line 81
  10. def OAI.Grothendieck.GlobularTheory.Model.smallFreeCell line 98
  11. theorem OAI.Grothendieck.GlobularTheory.Model.smallFreeCell_source line 103
  12. theorem OAI.Grothendieck.GlobularTheory.Model.smallFreeCell_target line 112
  13. theorem OAI.Grothendieck.GlobularTheory.Model.smallFreeCell_map line 121
  14. theorem OAI.Grothendieck.GlobularTheory.Model.smallShapeDesc_cell line 128
  15. def OAI.Grothendieck.GlobularPresheaf.finiteRealizationDesc line 143
  16. theorem OAI.Grothendieck.GlobularPresheaf.finiteRealizationDesc_cell line 177
  17. theorem OAI.Grothendieck.FiniteCoGlobularObject.face_natural line 194