OAI/CategoryTheory/Globular/FrameRealization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Grothendieck.GlobularFrame.homGlob_faceMap line 12
  2. theorem OAI.Grothendieck.GlobularFrame.homGlob_eval line 23
  3. def OAI.Grothendieck.GlobularFrame.homGlobPresheafIso line 29
  4. abbrev OAI.Grothendieck.GlobularFrame.realization line 39
  5. abbrev OAI.Grothendieck.GlobularFrame.cell line 40
  6. def OAI.Grothendieck.GlobularFrame.desc line 43
  7. theorem OAI.Grothendieck.GlobularFrame.cell_desc line 48
  8. theorem OAI.Grothendieck.GlobularFrame.cell_face line 58
  9. def OAI.Grothendieck.GlobularFrame.cellMap line 72
  10. def OAI.Grothendieck.GlobularFrame.realizeHom line 86
  11. theorem OAI.Grothendieck.GlobularFrame.hom_ext line 90
  12. theorem OAI.Grothendieck.GlobularFrame.realizeHom_desc line 93
  13. theorem OAI.Grothendieck.GlobularFrame.desc_realizeHom line 98