OAI/CategoryTheory/Globular/WhiskerUniverse.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Grothendieck.GlobularSet.ulift line 11
  2. theorem OAI.Grothendieck.GlobularSet.ulift_faceMap line 18
  3. theorem OAI.Grothendieck.GlobularSet.ulift_evalFace line 27
  4. def OAI.Grothendieck.GlobularSet.uliftPresheafIso line 34
  5. def OAI.Grothendieck.GlobularSet.uliftWhiskerTo line 42
  6. def OAI.Grothendieck.GlobularSet.uliftWhiskerFrom line 61
  7. def OAI.Grothendieck.GlobularSet.uliftWhiskerIso line 78
  8. def OAI.Grothendieck.GlobularPresheaf.liftSmallWhiskerIso line 98
  9. theorem OAI.Grothendieck.GlobularTheory.Model.cutoffFrame_whisker_hasFillers line 107