OAI/CategoryTheory/Globular/Factorization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Grothendieck.GlobularSet.FactorStage line 13
  2. def OAI.Grothendieck.GlobularSet.FactorStage.zero line 25
  3. def OAI.Grothendieck.GlobularSet.FactorStage.nextBoundary line 37
  4. def OAI.Grothendieck.GlobularSet.FactorStage.extend line 47
  5. theorem OAI.Grothendieck.GlobularSet.FactorStage.extend_old line 81
  6. theorem OAI.Grothendieck.GlobularSet.FactorStage.exists_extend line 86
  7. theorem OAI.Grothendieck.GlobularSet.existsUnique_factor_low_bijective line 127
  8. def OAI.Grothendieck.TupleSystem.evaluationIso line 173
  9. theorem OAI.Grothendieck.TupleSystem.hom_ext_globes line 179
  10. def OAI.Grothendieck.TupleSystem.mapFromUnderlying line 199
  11. theorem OAI.Grothendieck.TupleSystem.mapFromUnderlying_globe line 205
  12. theorem OAI.Grothendieck.GlobularTheory.Model.underlyingMap_injective line 227