OAI/CategoryTheory/Globular/Density.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Grothendieck.GlobularPresheaf.densityDesc line 12
  2. theorem OAI.Grothendieck.GlobularPresheaf.densityDesc_cell line 27
  3. theorem OAI.Grothendieck.GlobularPresheaf.density_hom_ext line 34
  4. def OAI.Grothendieck.GlobularPresheaf.liftSmall line 43
  5. instance OAI.Grothendieck.GlobularPresheaf.liftSmall_preservesColimits line 46
  6. def OAI.Grothendieck.GlobularTheory.Model.smallFree line 54
  7. instance OAI.Grothendieck.GlobularTheory.Model.smallFree_preservesColimits line 58
  8. def OAI.Grothendieck.GlobularTheory.Model.cutoffShapeEquiv line 65
  9. theorem OAI.Grothendieck.GlobularTheory.Model.cutoffShapeEquiv_naturality line 71
  10. def OAI.Grothendieck.GlobularTheory.Model.smallFreeShapeIso line 82
  11. theorem OAI.Grothendieck.GlobularTheory.Model.smallFree_cofibrant line 106
  12. def OAI.Grothendieck.GlobularTheory.Model.smallFreeGen line 110
  13. def OAI.Grothendieck.GlobularTheory.Model.smallFreeDesc line 117
  14. theorem OAI.Grothendieck.GlobularTheory.Model.smallFreeDesc_gen line 125
  15. theorem OAI.Grothendieck.GlobularTheory.Model.smallFreeGen_source line 136
  16. theorem OAI.Grothendieck.GlobularTheory.Model.smallFreeGen_target line 144
  17. theorem OAI.Grothendieck.GlobularTheory.Model.smallFreeGen_map line 152