OAI/CategoryTheory/Globular/OneSidedPresentation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Grothendieck.GlobularFrame.Presentation.boundaryDesc line 17
2. theorem OAI.Grothendieck.GlobularFrame.Presentation.boundaryDesc_left line 20
3. theorem OAI.Grothendieck.GlobularFrame.Presentation.boundaryDesc_right line 24
4. theorem OAI.Grothendieck.GlobularFrame.Presentation.boundaryApp_desc line 29
5. theorem OAI.Grothendieck.GlobularFrame.Presentation.boundaryDesc_comm line 50
6. def OAI.Grothendieck.GlobularFrame.Presentation.oneSidedStage line 67
7. def OAI.Grothendieck.GlobularFrame.Presentation.oneSidedPresentation line 85