OAI/CategoryTheory/Globular/Homotopy.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Grothendieck.GlobularSet.Parallel.symm line 13
  2. theorem OAI.Grothendieck.GlobularSet.outer_parallel line 19
  3. def OAI.Grothendieck.GlobularSet.LiftsBoundaries line 30
  4. theorem OAI.Grothendieck.GlobularSet.exactBoundaryTest_endpoint_section line 34
  5. theorem OAI.Grothendieck.Shape.source_source line 66
  6. theorem OAI.Grothendieck.Shape.target_source line 72
  7. theorem OAI.Grothendieck.Shape.seam_inl line 78
  8. theorem OAI.Grothendieck.Shape.globe_seam line 85
  9. def OAI.Grothendieck.GlobularTheory.inversePair line 92
  10. theorem OAI.Grothendieck.GlobularTheory.Model.joined_refl line 110
  11. theorem OAI.Grothendieck.GlobularTheory.Model.joined_symm line 114
  12. def OAI.Grothendieck.GlobularTheory.compositionShape line 134
  13. def OAI.Grothendieck.GlobularTheory.compositionLeft line 137
  14. def OAI.Grothendieck.GlobularTheory.compositionRight line 140
  15. theorem OAI.Grothendieck.GlobularTheory.composition_seam line 143
  16. def OAI.Grothendieck.GlobularTheory.compositionPair line 149
  17. theorem OAI.Grothendieck.GlobularTheory.Model.joined_trans line 179
  18. theorem OAI.Grothendieck.GlobularTheory.Model.joined_equivalence line 206
  19. theorem OAI.Grothendieck.GlobularTheory.Morphism.id_comp line 213
  20. theorem OAI.Grothendieck.GlobularTheory.Morphism.comp_id line 216
  21. theorem OAI.Grothendieck.GlobularTheory.Morphism.comp_assoc line 219
  22. def OAI.Grothendieck.GlobularTheory.Morphism.mapPair line 223
  23. theorem OAI.Grothendieck.GlobularTheory.Fills.map line 244
  24. theorem OAI.Grothendieck.GlobularTheory.IsFreeExtension.hom_ext line 253
  25. def OAI.Grothendieck.GlobularTheory.LiftsFillers line 264
  26. theorem OAI.Grothendieck.GlobularTheory.CellularPresentation.hom_ext line 270
  27. theorem OAI.Grothendieck.GlobularTheory.CellularPresentation.lift line 277
  28. structure OAI.Grothendieck.TupleSystem line 318
  29. def OAI.Grothendieck.TupleSystem.endData line 329
  30. def OAI.Grothendieck.TupleSystem.endEmbedding line 340
  31. def OAI.Grothendieck.TupleSystem.endEmbedding_fullyFaithful line 346
  32. def OAI.Grothendieck.TupleSystem.endTheory line 350
  33. def OAI.Grothendieck.TupleSystem.model line 358
  34. abbrev OAI.Grothendieck.GlobularTheory.Model.tuples line 376
  35. def OAI.Grothendieck.GlobularTheory.Model.interpretation line 380