OAI/CategoryTheory/Globular/Colimits.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Grothendieck.GlobularSet.source_bijective_of_coskeletal line 13
  2. theorem OAI.Grothendieck.GlobularTheory.Model.cellEquiv_comp line 31
  3. theorem OAI.Grothendieck.GlobularTheory.Model.cellEquiv_J line 35
  4. theorem OAI.Grothendieck.GlobularTheory.Model.J_coskeletalLocalMap line 42
  5. theorem OAI.Grothendieck.GlobularTheory.Model.CoskeletalLocalMap.pushout line 56
  6. theorem OAI.Grothendieck.GlobularTheory.Model.elementary_pushout_low_bijective line 71
  7. theorem OAI.Grothendieck.GlobularTheory.Model.low_bijections_eq_local line 79
  8. theorem OAI.Grothendieck.GlobularTheory.Model.low_bijective_transfinite line 88
  9. theorem OAI.Grothendieck.GlobularSet.exactBoundaryTest_split_into_coskeletal line 109
  10. theorem OAI.Grothendieck.GlobularTheory.Model.elementary_pushout_to_coskeletal line 137
  11. structure OAI.Grothendieck.GlobularTheory.SumIndex line 154
  12. def OAI.Grothendieck.GlobularTheory.sumDiagram line 161
  13. def OAI.Grothendieck.GlobularTheory.sumCone line 166
  14. def OAI.Grothendieck.GlobularTheory.sumConeIsLimit line 171
  15. def OAI.Grothendieck.GlobularTheory.sumComparison line 175
  16. def OAI.Grothendieck.GlobularTheory.sumComparisons line 179
  17. instance OAI.Grothendieck.GlobularTheory.shrinkYoneda_cardinalPresentable line 185
  18. instance OAI.Grothendieck.GlobularTheory.sumComparison_source_presentable line 193
  19. theorem OAI.Grothendieck.GlobularTheory.sumComparisons_rightAdjoint line 202
  20. theorem OAI.Grothendieck.GlobularTheory.sumComparison_local_iff line 213
  21. theorem OAI.Grothendieck.GlobularTheory.Model.sums_local line 232
  22. def OAI.Grothendieck.GlobularTheory.Model.toLocal line 238
  23. theorem OAI.Grothendieck.GlobularTheory.Model.local_sums line 243
  24. def OAI.Grothendieck.GlobularTheory.Model.fromLocal line 254
  25. def OAI.Grothendieck.GlobularTheory.Model.localEquivalence line 261
  26. instance OAI.Grothendieck.GlobularTheory.Model.hasColimits line 268
  27. abbrev OAI.Grothendieck.GlobularTheory.Model.CutoffModels line 281
  28. def OAI.Grothendieck.GlobularTheory.Model.chosenCutoff line 284
  29. def OAI.Grothendieck.GlobularTheory.Model.cutoffUnit line 288
  30. theorem OAI.Grothendieck.GlobularTheory.Model.cutoffUnit_low_bijective line 292
  31. theorem OAI.Grothendieck.GlobularTheory.Model.chosenCutoff_coskeletal line 297
  32. theorem OAI.Grothendieck.GlobularTheory.Model.cutoffUnit_universal line 301
  33. def OAI.Grothendieck.GlobularTheory.Model.cutoffObject line 306
  34. def OAI.Grothendieck.GlobularTheory.Model.cutoffEquiv line 310
  35. theorem OAI.Grothendieck.GlobularTheory.Model.cutoffEquiv_natural line 323
  36. def OAI.Grothendieck.GlobularTheory.Model.cutoffFunctor line 330
  37. def OAI.Grothendieck.GlobularTheory.Model.cutoffAdjunction line 335
  38. def OAI.Grothendieck.GlobularTheory.Model.cutoffReflective line 339
  39. theorem OAI.Grothendieck.GlobularTheory.Model.cutoff_hasColimits line 343