OAI/CategoryTheory/Globular/Basic.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Grothendieck.GlobularSet.Hom.id line 10
  2. def OAI.Grothendieck.GlobularSet.Hom.comp line 16
  3. instance OAI.Grothendieck.GlobularSet.(instance at line 21) line 21
  4. theorem OAI.Grothendieck.GlobularSet.Hom.boundary_app line 29
  5. def OAI.Grothendieck.GlobularSet.ExactBoundaryTest line 35
  6. theorem OAI.Grothendieck.GlobularSet.parallel_iff_boundary_eq line 39
  7. theorem OAI.Grothendieck.GlobularSet.ExactBoundaryTest.reflects_joined line 51
  8. theorem OAI.Grothendieck.GlobularSet.Hom.boundaryMap_comp line 63
  9. theorem OAI.Grothendieck.GlobularSet.ExactBoundaryTest.of_mutual_composites line 68
  10. def OAI.Grothendieck.GlobularTheory.Model.cellEquiv line 84
  11. theorem OAI.Grothendieck.GlobularTheory.unit_source line 92
  12. theorem OAI.Grothendieck.GlobularTheory.unit_target line 96
  13. theorem OAI.Grothendieck.GlobularTheory.Model.eval_comp line 103
  14. theorem OAI.Grothendieck.GlobularTheory.Model.eval_id line 111
  15. theorem OAI.Grothendieck.GlobularTheory.Model.unitCell_source line 115
  16. theorem OAI.Grothendieck.GlobularTheory.Model.unitCell_target line 122