vcomp — Mathlib

Lean4
/-- Vertical composition of oplax transformations. -/
def vcomp : OplaxTrans F H where
  app a := η.app a ≫ θ.app a
  naturality {a b}
    f := (α_ _ _ _).inv ≫ η.naturality f ▷ θ.app b ≫ (α_ _ _ _).hom ≫ η.app a ◁ θ.naturality f ≫ (α_ _ _ _).inv
  naturality_comp {a b c} f
    g :=
    calc
      _ =
          (α_ _ _ _).inv ≫
            F.mapComp f g ▷ η.app c ▷ θ.app c ≫
              (α_ _ _ _).hom ▷ _ ≫
                (α_ _ _ _).hom ≫
                  F.map f ◁ η.naturality g ▷ θ.app c ≫
                    _ ◁ (α_ _ _ _).hom ≫
                      (α_ _ _ _).inv ≫
                        (F.map f ≫ η.app b) ◁ θ.naturality g ≫
                          η.naturality f ▷ (θ.app b ≫ H.map g) ≫
                            (α_ _ _ _).hom ≫
                              _ ◁ (α_ _ _ _).inv ≫
                                η.app a ◁ θ.naturality f ▷ H.map g ≫ _ ◁ (α_ _ _ _).hom ≫ (α_ _ _ _).inv :=
        by rw [whisker_exchange_assoc]; simp
      _ = _ := by simp
Похожие утверждения