OAI/CategoryTheory/Globular/CylinderContractibility.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Grothendieck.GlobularPresheaf.liftSmallDiskIso line 10
2. theorem OAI.Grothendieck.GlobularTheory.Model.hasFillers_of_iso line 20
3. def OAI.Grothendieck.GlobularTheory.Model.cylinderCriticalData line 25
4. theorem OAI.Grothendieck.GlobularTheory.Model.cutoff_boundary_surjective_iff line 44
5. theorem OAI.Grothendieck.GlobularTheory.Model.cutoffFrame_diskWhisker_hasFillers line 71
6. theorem OAI.Grothendieck.GlobularTheory.Model.cylinderNode_high_hasFillers line 80
7. theorem OAI.Grothendieck.GlobularTheory.Model.cylinder_oneSided_contractible line 95