OAI/CategoryTheory/Globular/CylinderTheory.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Grothendieck.GlobularFrame.shapeRealization_sums line 11
2. def OAI.Grothendieck.GlobularTheory.Model.shapeFrameNatIso line 25
3. def OAI.Grothendieck.GlobularTheory.Model.cylinderShapeEndpoint line 29
4. theorem OAI.Grothendieck.GlobularTheory.Model.cylinderShapeEndpoint_globe line 33
5. theorem OAI.Grothendieck.GlobularTheory.Model.cutoffRepresentables_sums line 41
6. abbrev OAI.Grothendieck.GlobularTheory.Model.cylinderTheory line 52
7. abbrev OAI.Grothendieck.GlobularTheory.Model.cylinderProjection line 56