OAI/CategoryTheory/Globular/RelativeLifting.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Grothendieck.GlobularSet.LiftsBoundary line 9
  2. structure OAI.Grothendieck.GlobularSet.RelativeLiftStage line 13
  3. theorem OAI.Grothendieck.GlobularSet.RelativeLiftStage.exists_cell line 22
  4. def OAI.Grothendieck.GlobularSet.RelativeLiftStage.zero line 50
  5. def OAI.Grothendieck.GlobularSet.RelativeLiftStage.succ line 73
  6. theorem OAI.Grothendieck.GlobularSet.RelativeLiftStage.succ_old line 104
  7. theorem OAI.Grothendieck.GlobularSet.relative_lift line 115
  8. theorem OAI.Grothendieck.GlobularPresheaf.relative_lift line 142
  9. theorem OAI.Grothendieck.GlobularTheory.Model.cutoffFreeGlobular_map_cofibration line 159
  10. theorem OAI.Grothendieck.GlobularTheory.Model.cutoff_hasLimits line 188
  11. theorem OAI.Grothendieck.GlobularTheory.Model.cutoff_hasFillers_iff line 193
  12. theorem OAI.Grothendieck.lifting_terminal_iff line 216
  13. structure OAI.Grothendieck.GlobularTheory.Model.CutoffPathData line 232
  14. theorem OAI.Grothendieck.GlobularTheory.Model.CutoffPathData.joint_rlp line 245
  15. theorem OAI.Grothendieck.GlobularTheory.Model.expansionContraction_of_paths line 263
  16. theorem OAI.Grothendieck.GlobularSet.ExactBoundaryTest.of_retract_factor line 310
  17. theorem OAI.Grothendieck.GlobularTheory.Model.weakEquivalence_of_cutoff_path line 330