OAI/CategoryTheory/Globular/CylinderPathLifting.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Grothendieck.GlobularSet.liftsBoundary_of_bijective line 11
2. theorem OAI.Grothendieck.GlobularSet.LiftsBoundary.comp line 19
3. theorem OAI.Grothendieck.GlobularFrame.Hom.pre_liftsBoundary line 31
4. theorem OAI.Grothendieck.GlobularFrame.jointSource_lift line 56
5. theorem OAI.Grothendieck.GlobularTheory.Model.fullCylinderEvaluation_bijective line 80
6. theorem OAI.Grothendieck.GlobularTheory.Model.fullCylinderEndpoint_liftsBoundary line 92
7. theorem OAI.Grothendieck.GlobularTheory.Model.fullCylinder_joint line 101