Theorems · Theorem · category theory

CategoryTheory.toOverIteratedSliceForwardIsoPullback_inv_app_left

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X Y : C}
  (f : Y ⟶ X) (X_1 : CategoryTheory.Over X),
  ((CategoryTheory.toOverIteratedSliceForwardIsoPullback f).inv.app X_1).left =
    CategoryTheory.Over.Hom.left
      ((((((((CategoryTheory.Over.mk f).iteratedSliceBackward.comp
                                  (CategoryTheory.Over.forget (CategoryTheory.Over.mk f))).leftUnitor.symm.homCongr
                          (CategoryTheory.Over.map f).rightUnitor.symm).trans
                      (CategoryTheory.TwoSquare.equivNatTrans (CategoryTheory.Functor.id (CategoryTheory.Over Y))
                          (CategoryTheory.Over.map f)
                          ((CategoryTheory.Over.mk f).iteratedSliceBackward.comp
                            (CategoryTheory.Over.forget (CategoryTheory.Over.mk f)))
                          (CategoryTheory.Functor.id (CategoryTheory.Over X))).symm).trans
                  (CategoryTheory.mateEquiv (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f)
                    ((CategoryTheory.Over.mk f).iteratedSliceEquiv.symm.toAdjunction.comp
                      (CategoryTheory.forgetAdjToOver (CategoryTheory.Over.mk f))))).trans
              (CategoryTheory.TwoSquare.equivNatTrans (CategoryTheory.ChosenPullbacksAlong.pullback f)
                (CategoryTheory.Functor.id (CategoryTheory.Over X)) (CategoryTheory.Functor.id (CategoryTheory.Over Y))
                ((CategoryTheory.toOver (CategoryTheory.Over.mk f)).comp
                  (CategoryTheory.Over.mk f).iteratedSliceForward)))
            (CategoryTheory.eqToHom ⋯)).app
        X_1)

Defined in

Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Cited by

0 results in Mathlib

Foundations

Depth 41 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.ChosenPullbacks