OAI/CategoryTheory/Thomason/Presentations.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Presentations.

  1. def OAI.Thomason.OmegaCategory.coneOld line 14
  2. lemma OAI.Thomason.OmegaCategory.coneOld_old line 20
  3. lemma OAI.Thomason.OmegaCategory.old_coneOld line 23
  4. def OAI.Thomason.OmegaCategory.coneOldFunctor line 31
  5. def OAI.Thomason.OmegaCategory.coneRestrict line 55
  6. lemma OAI.Thomason.OmegaCategory.old_coneRestrict line 60
  7. lemma OAI.Thomason.OmegaCategory.coneRestrict_extend line 66
  8. lemma OAI.Thomason.OmegaCategory.coneExtend_restrict line 75
  9. def OAI.Thomason.OmegaCategory.zeroFiberConeHomEquiv line 102
  10. def OAI.Thomason.OmegaCategory.zeroFiberConeAdjunction line 122
  11. instance OAI.Thomason.OmegaCategory.zeroFiber_preservesColimits line 146
  12. lemma OAI.Thomason.OmegaCategory.Presentation.Equiv.refl line 176
  13. lemma OAI.Thomason.OmegaCategory.Presentation.Equiv.symm line 177
  14. lemma OAI.Thomason.OmegaCategory.Presentation.Equiv.trans line 178
  15. lemma OAI.Thomason.OmegaCategory.Presentation.Equiv.source line 180
  16. lemma OAI.Thomason.OmegaCategory.Presentation.Equiv.target line 182
  17. lemma OAI.Thomason.OmegaCategory.Presentation.Equiv.composable_congr line 184
  18. lemma OAI.Thomason.OmegaCategory.Presentation.Equiv.comp line 188
  19. lemma OAI.Thomason.OmegaCategory.Presentation.eval_dimension line 196
  20. lemma OAI.Thomason.OmegaCategory.Presentation.compTerm_equiv line 214
  21. lemma OAI.Thomason.OmegaCategory.Presentation.cells_ext line 226
  22. lemma OAI.Thomason.OmegaCategory.Presentation.evaluate_source line 232
  23. lemma OAI.Thomason.OmegaCategory.Presentation.evaluate_target line 237
  24. lemma OAI.Thomason.OmegaCategory.Presentation.evaluate_composable line 242
  25. lemma OAI.Thomason.OmegaCategory.Presentation.evaluate_comp line 247
  26. lemma OAI.Thomason.OmegaCategory.Presentation.generator_bounded line 273
  27. lemma OAI.Thomason.OmegaCategory.Presentation.lift_generator line 279
  28. lemma OAI.Thomason.OmegaCategory.Presentation.mk_source line 282
  29. lemma OAI.Thomason.OmegaCategory.Presentation.mk_target line 285
  30. lemma OAI.Thomason.OmegaCategory.Presentation.mk_comp line 288
  31. lemma OAI.Thomason.OmegaCategory.Presentation.functor_ext line 296
  32. lemma OAI.Thomason.OmegaCategory.Presentation.evaluate_generator line 330
  33. lemma OAI.Thomason.OmegaCategory.truncation_isTruncated line 359
  34. lemma OAI.Thomason.OmegaCategory.truncationLift_generator line 368
  35. lemma OAI.Thomason.OmegaCategory.truncation_functor_ext line 372
  36. instance OAI.Thomason.OmegaCategory.truncation_preservesColimits line 382
  37. lemma OAI.Thomason.OmegaCategory.uliftUp_down line 397
  38. lemma OAI.Thomason.OmegaCategory.uliftDown_up line 400
  39. instance OAI.Thomason.raisedOrientals_hasLeftKan line 432
  40. instance OAI.Thomason.categorification_preservesColimits line 438
  41. instance OAI.Thomason.categorificationFinite_preservesColimits line 442
  42. instance OAI.Thomason.OmegaCategory.nCategoryInclusion_full line 458
  43. instance OAI.Thomason.OmegaCategory.nCategoryInclusion_faithful line 461
  44. instance OAI.Thomason.OmegaCategory.nCategoryInclusion_reflective line 464
  45. instance OAI.Thomason.OmegaCategory.nCategory_hasColimits line 469
  46. lemma OAI.Thomason.WeakHomotopy.loopMap_homotopic line 500
  47. def OAI.Thomason.thomasonFibrations line 519
  48. def OAI.Thomason.thomasonCofibrations line 522
  49. def OAI.Thomason.thomasonFibrationsFinite line 526
  50. def OAI.Thomason.thomasonCofibrationsFinite line 530