OAI/CategoryTheory/Globular/CylinderLifting.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Grothendieck.CylinderNode.oneSideMap line 12
2. theorem OAI.Grothendieck.GlobularTheory.Model.completedCylinder_upper line 20
3. theorem OAI.Grothendieck.GlobularTheory.Model.cylinderNode_upper line 32
4. theorem OAI.Grothendieck.GlobularTheory.Model.cylinderFrame_upper line 41
5. theorem OAI.Grothendieck.GlobularTheory.Model.cylinderNode_upper_fillers line 46
6. def OAI.Grothendieck.GlobularSet.LiftStage.extendOne line 62
7. theorem OAI.Grothendieck.GlobularSet.LiftStage.extendOne_old line 74
8. def OAI.Grothendieck.GlobularSet.LiftStage.extendBy line 79
9. theorem OAI.Grothendieck.GlobularSet.LiftStage.extendBy_old line 85