transform — Mathlib

Lean4
/-- Functorially transform a `CatCommSqOver F G X` by whiskering it with a
`CatCospanTransform`. -/
@[simps]
def transform (X : Type u₇) [Category.{v₇} X] :
    CatCospanTransform F G F₁ G₁ ⥤ CatCommSqOver F G X ⥤ CatCommSqOver F₁ G₁ X
    where
  obj
    ψ :=
    { obj
        S :=
        { fst := S.fst ⋙ ψ.left
          snd := S.snd ⋙ ψ.right
          iso :=
            (Functor.associator _ _ _) ≪≫
              isoWhiskerLeft S.fst (ψ.squareLeft.iso.symm) ≪≫
                (Functor.associator _ _ _).symm ≪≫
                  isoWhiskerRight S.iso _ ≪≫
                    isoWhiskerLeft S.snd (ψ.squareRight.iso) ≪≫ (Functor.associator _ _ _).symm }
      map {x y}
        f :=
        { fst := whiskerRight f.fst ψ.left
          snd := whiskerRight f.snd ψ.right
          w := by
            ext x
            simp [← Functor.map_comp_assoc] } }
  map {ψ ψ'}
    η :=
    {
      app
        S :=
        { fst := { app y := η.left.app (S.fst.obj y) }
          snd := { app y := η.right.app (S.snd.obj y) }
          w := by
            ext t
            have := ψ.squareLeft.iso.inv.app (S.fst.obj t) ≫= η.left_coherence_app (S.fst.obj t)
            simp only [Iso.inv_hom_id_app_assoc] at this
            simp [this] } }
Похожие утверждения