OAI/CategoryTheory/Globular/SmallObject.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Grothendieck.GlobularTheory.Model.presheafFunctor_finitelyAccessible line 11
  2. instance OAI.Grothendieck.GlobularTheory.Model.freeShape_finitelyPresentable line 22
  3. instance OAI.Grothendieck.GlobularTheory.Model.disk_finitelyPresentable line 29
  4. instance OAI.Grothendieck.GlobularTheory.Model.boundaryDisk_finitelyPresentable line 33
  5. def OAI.Grothendieck.GlobularTheory.Model.highBoundaries line 56
  6. theorem OAI.Grothendieck.GlobularTheory.Model.isCoskeletal_iff_local line 60
  7. theorem OAI.Grothendieck.GlobularTheory.Model.highBoundaries_local line 95
  8. instance OAI.Grothendieck.GlobularTheory.Model.cutoffInclusion_finitelyAccessible line 100
  9. theorem OAI.Grothendieck.GlobularTheory.Model.cutoff_finitelyPresentable line 108
  10. instance OAI.Grothendieck.GlobularTheory.Model.hasLimits line 116
  11. theorem OAI.Grothendieck.GlobularTheory.Model.hasFillers_iff line 122
  12. theorem OAI.Grothendieck.GlobularTheory.Model.hasFillers_of_filteredColimit line 139
  13. theorem OAI.Grothendieck.GlobularTheory.Model.hasFillers_of_cutoffFilteredColimit line 149
  14. theorem OAI.Grothendieck.smallObjectArgument_of_finiteDomains line 165
  15. abbrev OAI.Grothendieck.GlobularTheory.Model.cutoffDisk line 177
  16. abbrev OAI.Grothendieck.GlobularTheory.Model.cutoffBoundary line 180
  17. abbrev OAI.Grothendieck.GlobularTheory.Model.cutoffI line 183
  18. abbrev OAI.Grothendieck.GlobularTheory.Model.cutoffJ line 187
  19. def OAI.Grothendieck.GlobularTheory.Model.boundaryClass line 191
  20. def OAI.Grothendieck.GlobularTheory.Model.sourceClass line 195
  21. theorem OAI.Grothendieck.GlobularTheory.Model.boundaryClass_rlp_iff line 199
  22. theorem OAI.Grothendieck.GlobularTheory.Model.sourceClass_rlp_iff line 211
  23. theorem OAI.Grothendieck.GlobularTheory.Model.boundaryClass_smallObject line 223
  24. theorem OAI.Grothendieck.GlobularTheory.Model.sourceClass_smallObject line 231
  25. def OAI.Grothendieck.GlobularTheory.Model.Cofibrant line 239
  26. theorem OAI.Grothendieck.GlobularTheory.Model.Cofibrant.of_cofibration line 244
  27. theorem OAI.Grothendieck.GlobularTheory.Model.Cofibrant.retract line 253
  28. theorem OAI.Grothendieck.GlobularTheory.Model.hasLiftingProperty_J_of_I line 260
  29. theorem OAI.Grothendieck.GlobularTheory.Model.sourceClass_cofibration_le line 283
  30. theorem OAI.Grothendieck.GlobularTheory.Model.boundaryClass_cofibration_le line 292