FunctorObjectIteration.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.functorObjectIteration line 13
Source documentation
An actual natural isomorphism identifies every objectwise iterate.
```
def functorObjectIteration (e : F ≅ G) (r : ℕ) (Y : C) :
    (F.obj^[r]) Y ≅ (G.obj^[r]) Y := by
…
```
def OAI.LittleFinitistic.mapObjectIteration line 22
Source documentation
Transport an object isomorphism through an actual repeated functor.
```
def mapObjectIteration (F : C ⥤ C) {X Y : C} (e : X ≅ Y) (r : ℕ) :
    (F.obj^[r]) X ≅ (F.obj^[r]) Y := by
…
```