OAI/CategoryTheory/Globular/ShapeFrame.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Grothendieck.GlobularTheory.Model.representables line 12
2. abbrev OAI.Grothendieck.GlobularTheory.Model.cutoffRepresentables line 18
3. theorem OAI.Grothendieck.GlobularTheory.Model.shapeGlobularEquiv_left line 21
4. theorem OAI.Grothendieck.GlobularTheory.Model.cutoffShapeEquiv_left line 34
5. theorem OAI.Grothendieck.GlobularTheory.Model.cutoffFrameHomEquiv_left line 47
6. def OAI.Grothendieck.GlobularTheory.Model.shapeFrameIso line 59
7. theorem OAI.Grothendieck.GlobularTheory.Model.shapeFrameIso_equiv line 77
8. theorem OAI.Grothendieck.GlobularTheory.Model.shapeFrameIso_naturality line 87
9. theorem OAI.Grothendieck.GlobularTheory.Model.cutoffShapeEquiv_top line 106
10. theorem OAI.Grothendieck.GlobularTheory.Model.shapeFrameIso_globe line 114