OAI/CategoryTheory/Globular/CylinderFramework.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Grothendieck.GlobularFrame line 10
  2. def OAI.Grothendieck.GlobularFrame.diagram line 22
  3. def OAI.Grothendieck.GlobularFrame.homGlob line 33
  4. def OAI.Grothendieck.GlobularFrame.post line 46
  5. structure OAI.Grothendieck.GlobularFrame.BoundaryEquiv line 52
  6. def OAI.Grothendieck.GlobularFrame.BoundaryEquiv.zero line 61
  7. def OAI.Grothendieck.GlobularFrame.BoundaryEquiv.nextValue line 72
  8. theorem OAI.Grothendieck.GlobularFrame.BoundaryEquiv.nextValue_bijective line 77
  9. def OAI.Grothendieck.GlobularFrame.BoundaryEquiv.succ line 92
  10. def OAI.Grothendieck.GlobularFrame.boundaryEquiv line 105
  11. structure OAI.Grothendieck.GlobularFrame.Hom line 109
  12. theorem OAI.Grothendieck.GlobularFrame.Hom.source_naturality line 118
  13. theorem OAI.Grothendieck.GlobularFrame.Hom.target_naturality line 123
  14. def OAI.Grothendieck.GlobularFrame.Hom.pre line 129
  15. theorem OAI.Grothendieck.GlobularFrame.Hom.boundary_naturality line 140
  16. def OAI.Grothendieck.GlobularSet.fiberProd line 156
  17. def OAI.Grothendieck.GlobularSet.fiberProd.fst line 167
  18. def OAI.Grothendieck.GlobularSet.fiberProd.snd line 171
  19. def OAI.Grothendieck.GlobularSet.fiberProd.lift line 177
  20. theorem OAI.Grothendieck.GlobularSet.fiberProd.lift_fst line 182
  21. theorem OAI.Grothendieck.GlobularSet.fiberProd.lift_snd line 184
  22. abbrev OAI.Grothendieck.GlobularFrame.oneSided line 194
  23. def OAI.Grothendieck.GlobularFrame.oneSidedMap line 195
  24. def OAI.Grothendieck.GlobularFrame.Hom.relativeGlob line 201
  25. def OAI.Grothendieck.GlobularFrame.Hom.relativeMap line 203
  26. theorem OAI.Grothendieck.GlobularFrame.Hom.relativeMap_liftsBoundary line 208