OAI/CategoryTheory/Globular/ReverseWhisker.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerFree line 11
  2. def OAI.Grothendieck.GlobularTheory.Model.rwBase line 15
  3. def OAI.Grothendieck.GlobularTheory.Model.rwEdge line 20
  4. theorem OAI.Grothendieck.GlobularTheory.Model.rwBase_source line 25
  5. theorem OAI.Grothendieck.GlobularTheory.Model.rwBase_target line 34
  6. theorem OAI.Grothendieck.GlobularTheory.Model.rwEdge_target line 43
  7. def OAI.Grothendieck.GlobularTheory.Model.smallReverseWhiskerCell line 51
  8. theorem OAI.Grothendieck.GlobularTheory.Model.smallReverseWhiskerCell_source line 61
  9. theorem OAI.Grothendieck.GlobularTheory.Model.smallReverseWhiskerCell_target line 80
  10. def OAI.Grothendieck.GlobularTheory.Model.smallReverseWhiskerDesc line 99
  11. theorem OAI.Grothendieck.GlobularTheory.Model.smallReverseWhiskerDesc_base line 118
  12. theorem OAI.Grothendieck.GlobularTheory.Model.smallReverseWhiskerDesc_edge line 125
  13. def OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerIn line 131
  14. theorem OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerIn_gen line 135
  15. theorem OAI.Grothendieck.GlobularTheory.Model.inverseCell_inverse line 140
  16. theorem OAI.Grothendieck.GlobularTheory.Model.rwEdge_source line 154
  17. def OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerToWhisker line 163
  18. def OAI.Grothendieck.GlobularTheory.Model.whiskerToReverseWhisker line 170
  19. theorem OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerRound_base line 177
  20. theorem OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerRound_edge line 189
  21. theorem OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerRound_low line 202
  22. theorem OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerRound_top line 216
  23. theorem OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerFree_bounded_hasFillers line 238
  24. theorem OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerFree_hom_ext line 254
  25. def OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerFreeMap line 270
  26. theorem OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerFreeMap_base line 275
  27. theorem OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerFreeMap_edge line 281
  28. theorem OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerIn_naturality line 287
  29. theorem OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerFree_hasFillers_of_spine line 295
  30. theorem OAI.Grothendieck.GlobularTheory.Model.reverseWhiskerFree_hasFillers line 364