OAI/CategoryTheory/Globular/DiskComparison.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Grothendieck.Globe.faceLE line 13
  2. theorem OAI.Grothendieck.Globe.faceLE_refl line 16
  3. theorem OAI.Grothendieck.Globe.faceLE_of_lt line 20
  4. def OAI.Grothendieck.GlobularPresheaf.faceLE line 28
  5. theorem OAI.Grothendieck.GlobularPresheaf.faceLE_refl line 31
  6. theorem OAI.Grothendieck.GlobularPresheaf.faceLE_of_lt line 35
  7. theorem OAI.Grothendieck.GlobularPresheaf.face_low_bijective line 40
  8. theorem OAI.Grothendieck.GlobularPresheaf.face_low_equal line 63
  9. theorem OAI.Grothendieck.GlobularPresheaf.faceLE_low_bijective line 71
  10. theorem OAI.Grothendieck.GlobularPresheaf.face_comp_faceLE line 80
  11. theorem OAI.Grothendieck.GlobularPresheaf.globeMap_low_equal line 89
  12. theorem OAI.Grothendieck.GlobularPresheaf.disk_hom_ext line 108
  13. theorem OAI.Grothendieck.GlobularPresheaf.pushout_comparison_isIso line 113
  14. theorem OAI.Grothendieck.GlobularPresheaf.faceLE_cap_bijective line 140
  15. theorem OAI.Grothendieck.GlobularPresheaf.face_comp_eq_of_app_eq line 150
  16. def OAI.Grothendieck.Shape.last line 161