OAI/CategoryTheory/Globular/CylinderGluing.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Grothendieck.GlobularFrame.CriticalData line 12
  2. def OAI.Grothendieck.GlobularFrame.CriticalData.stageOfFac line 21
  3. def OAI.Grothendieck.GlobularFrame.CriticalData.initialCell line 40
  4. theorem OAI.Grothendieck.GlobularFrame.CriticalData.initialCell_low line 50
  5. theorem OAI.Grothendieck.GlobularFrame.CriticalData.initialCell_top line 57
  6. theorem OAI.Grothendieck.GlobularFrame.CriticalData.initialCell_fac line 61
  7. def OAI.Grothendieck.GlobularFrame.CriticalData.initialStage line 73
  8. structure OAI.Grothendieck.GlobularFrame.RelativeStage line 79
  9. def OAI.Grothendieck.GlobularFrame.RelativeStage.succ line 90
  10. theorem OAI.Grothendieck.GlobularFrame.RelativeStage.succ_old line 122
  11. def OAI.Grothendieck.GlobularFrame.RelativeStage.extendBy line 127
  12. theorem OAI.Grothendieck.GlobularFrame.RelativeStage.extendBy_old line 135