OAI/CategoryTheory/Globular/Groupoid.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Grothendieck.GlobularTheory.Model.cutoffFreeGlobular line 10
  2. def OAI.Grothendieck.GlobularTheory.Model.cutoffForgetGlobular line 14
  3. def OAI.Grothendieck.GlobularTheory.Model.cutoffGlobularAdjunction line 18
  4. instance OAI.Grothendieck.GlobularTheory.Model.cutoffFreeGlobular_preservesColimits line 22
  5. theorem OAI.Grothendieck.GlobularTheory.Model.cutoffFreeGlobular_cofibrant line 26
  6. def OAI.Grothendieck.GlobularTheory.Model.shapeGlobularEquiv line 42
  7. theorem OAI.Grothendieck.GlobularTheory.Model.shapeGlobularEquiv_natural line 48
  8. theorem OAI.Grothendieck.GlobularTheory.Model.cutoffFreeShape_cofibrant line 59
  9. structure OAI.Grothendieck.GlobularTheory.Model.CellGroupoid line 83
  10. abbrev OAI.Grothendieck.GlobularTheory.Model.CellGroupoid.Edge line 90
  11. def OAI.Grothendieck.GlobularTheory.Model.CellGroupoid.edgeSetoid line 94
  12. def OAI.Grothendieck.GlobularTheory.Model.CellGroupoid.edgeComp line 99
  13. instance OAI.Grothendieck.GlobularTheory.Model.CellGroupoid.(instance at line 105) line 105
  14. def OAI.Grothendieck.GlobularTheory.Model.CellGroupoid.ofEdge line 131
  15. theorem OAI.Grothendieck.GlobularTheory.Model.CellGroupoid.ofEdge_eq_iff line 134
  16. instance OAI.Grothendieck.GlobularTheory.Model.CellGroupoid.(instance at line 138) line 138
  17. def OAI.Grothendieck.GlobularTheory.Model.CellGroupoid.map line 151
  18. def OAI.Grothendieck.GlobularSet.LiftStage.extendTop line 178
  19. def OAI.Grothendieck.GlobularSet.LiftStage.ofBounded line 213
  20. theorem OAI.Grothendieck.GlobularSet.LiftStage.ofBounded_fac line 229
  21. theorem OAI.Grothendieck.GlobularSet.lift_of_top_joined line 239
  22. theorem OAI.Grothendieck.GlobularTheory.Model.free_hasFillers_of_top_homotopy line 268