OAI/CategoryTheory/Globular/SkeletalPresentation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Grothendieck.GlobularSet.LiftStage.restrict line 11
2. structure OAI.Grothendieck.GlobularFrame.Presentation line 21
3. def OAI.Grothendieck.GlobularFrame.Presentation.stageOn line 35
4. def OAI.Grothendieck.GlobularFrame.Presentation.postStage line 52
5. def OAI.Grothendieck.GlobularFrame.Presentation.comparison line 57
6. theorem OAI.Grothendieck.GlobularFrame.Presentation.comparison_base line 60
7. theorem OAI.Grothendieck.GlobularFrame.Presentation.comparison_stage line 62
8. theorem OAI.Grothendieck.GlobularFrame.Presentation.comparison_lifting line 66