OAI/CategoryTheory/Globular/Whisker.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Grothendieck.GlobularTheory.RepresentedHom line 10
  2. theorem OAI.Grothendieck.GlobularTheory.RepresentedHom.ext line 18
  3. def OAI.Grothendieck.GlobularTheory.representedData line 28
  4. def OAI.Grothendieck.GlobularTheory.representedTheory line 53
  5. def OAI.Grothendieck.GlobularTheory.representedProjection line 114
  6. inductive OAI.Grothendieck.GlobularSet.WhiskerCell line 127
  7. def OAI.Grothendieck.GlobularSet.WhiskerCell.source line 134
  8. def OAI.Grothendieck.GlobularSet.WhiskerCell.target line 141
  9. theorem OAI.Grothendieck.GlobularSet.WhiskerCell.source_base line 148
  10. theorem OAI.Grothendieck.GlobularSet.WhiskerCell.target_base line 152
  11. theorem OAI.Grothendieck.GlobularSet.WhiskerCell.source_tip line 156
  12. theorem OAI.Grothendieck.GlobularSet.WhiskerCell.target_tip line 160
  13. theorem OAI.Grothendieck.GlobularSet.WhiskerCell.source_edge line 164
  14. theorem OAI.Grothendieck.GlobularSet.WhiskerCell.target_edge line 167
  15. def OAI.Grothendieck.GlobularSet.whisker line 172
  16. def OAI.Grothendieck.GlobularSet.whiskerInclusion line 191
  17. def OAI.Grothendieck.GlobularSet.whiskerMap line 196
  18. theorem OAI.Grothendieck.GlobularSet.whisker_bounded line 213
  19. theorem OAI.Grothendieck.GlobularSet.whiskerMap_injective line 223
  20. def OAI.Grothendieck.GlobularSet.toPresheafUnderlying line 232
  21. def OAI.Grothendieck.GlobularSet.whiskerDesc line 237
  22. theorem OAI.Grothendieck.GlobularSet.whisker_hom_ext line 259
  23. def OAI.Grothendieck.GlobularPresheaf.whiskering line 283
  24. def OAI.Grothendieck.GlobularPresheaf.whiskeringInclusion line 293
  25. def OAI.Grothendieck.GlobularPresheaf.whiskeringDesc line 297
  26. theorem OAI.Grothendieck.GlobularPresheaf.whiskering_hom_ext line 303
  27. theorem OAI.Grothendieck.GlobularPresheaf.whiskering_pushout line 316