OAI/CategoryTheory/Globular/Coglobular.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Grothendieck.CoGlobularObject line 10
  2. def OAI.Grothendieck.CoGlobularObject.adjacent line 20
  3. theorem OAI.Grothendieck.CoGlobularObject.adjacent_pair line 23
  4. def OAI.Grothendieck.CoGlobularObject.face line 29
  5. theorem OAI.Grothendieck.CoGlobularObject.face_succ line 35
  6. theorem OAI.Grothendieck.CoGlobularObject.face_adjacent line 40
  7. theorem OAI.Grothendieck.CoGlobularObject.face_comp line 57
  8. def OAI.Grothendieck.CoGlobularObject.eval line 70
  9. def OAI.Grothendieck.CoGlobularObject.functor line 75
  10. def OAI.Grothendieck.CoGlobularObject.realization line 92
  11. def OAI.Grothendieck.CoGlobularObject.globeIso line 97
  12. instance OAI.Grothendieck.CoGlobularObject.preservesColimits_realization line 102
  13. theorem OAI.Grothendieck.CoGlobularObject.globeIso_naturality line 108
  14. def OAI.Grothendieck.CoGlobularObject.homEquiv line 115
  15. def OAI.Grothendieck.CoGlobularObject.cell line 121
  16. theorem OAI.Grothendieck.CoGlobularObject.homEquiv_app line 126
  17. theorem OAI.Grothendieck.CoGlobularObject.hom_ext line 137
  18. structure OAI.Grothendieck.FiniteCoGlobularObject line 151
  19. def OAI.Grothendieck.FiniteCoGlobularObject.completedObj line 163
  20. theorem OAI.Grothendieck.FiniteCoGlobularObject.completedObj_eq line 166
  21. theorem OAI.Grothendieck.FiniteCoGlobularObject.completedObj_terminal line 169
  22. def OAI.Grothendieck.FiniteCoGlobularObject.completedArrow line 172
  23. theorem OAI.Grothendieck.FiniteCoGlobularObject.completed_identity line 180
  24. abbrev OAI.Grothendieck.FiniteCoGlobularObject.complete line 193
  25. def OAI.Grothendieck.FiniteCoGlobularObject.map line 200
  26. def OAI.Grothendieck.FiniteCoGlobularObject.lowIso line 208
  27. def OAI.Grothendieck.FiniteCoGlobularObject.face line 211
  28. theorem OAI.Grothendieck.FiniteCoGlobularObject.face_succ line 215
  29. theorem OAI.Grothendieck.FiniteCoGlobularObject.face_comp line 227
  30. theorem OAI.Grothendieck.FiniteCoGlobularObject.face_adjacent line 233
  31. def OAI.Grothendieck.FiniteCoGlobularObject.realization line 240
  32. def OAI.Grothendieck.FiniteCoGlobularObject.globeIso line 243
  33. theorem OAI.Grothendieck.FiniteCoGlobularObject.globeIso_face line 248
  34. def OAI.Grothendieck.Shape.linearBlock line 267
  35. theorem OAI.Grothendieck.Shape.linearBlock_low line 270
  36. theorem OAI.Grothendieck.Shape.linearBlock_center line 273
  37. theorem OAI.Grothendieck.Shape.linearBlock_high line 277
  38. def OAI.Grothendieck.Shape.linearAdjacent line 280
  39. theorem OAI.Grothendieck.Shape.face_comp line 294
  40. theorem OAI.Grothendieck.Shape.face_triple_first_last line 300
  41. theorem OAI.Grothendieck.Shape.linearAdjacent_identity line 313
  42. def OAI.Grothendieck.Shape.linearDiagram line 329
  43. def OAI.Grothendieck.Shape.linearGlobularDiagram line 336
  44. def OAI.Grothendieck.Shape.linearization line 339
  45. def OAI.Grothendieck.Shape.linearGlobeIso line 342