OAI/CategoryTheory/Globular/Spines.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Grothendieck.Table.SpineData line 13
  2. def OAI.Grothendieck.Table.SpineData.globe line 26
  3. def OAI.Grothendieck.Table.SpineData.attachHigh line 34
  4. def OAI.Grothendieck.Table.SpineData.attachLow line 87
  5. def OAI.Grothendieck.Table.spine line 143
  6. theorem OAI.Grothendieck.GlobularPresheaf.underlyingMap_injective line 153
  7. theorem OAI.Grothendieck.GlobularPresheaf.existsUnique_factor_low_bijective line 162
  8. theorem OAI.Grothendieck.GlobularPresheaf.precomp_bijective_low line 182
  9. theorem OAI.Grothendieck.TupleSystem.map_bijective_of_low line 199