∀ {J : Type u_1} {X Y Z : CategoryTheory.Limits.WidePullbackShape J} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.WithTerminal.widePullbackShapeEquivMap✝ X Z) (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.WithTerminal.widePullbackShapeEquivMap✝¹ X Y) f)
      ((CategoryTheory.WithTerminal.widePullbackShapeEquivMap✝² Y Z) g)