{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d : B} →
      (f : a ⟶ b) →
        (h : c ⟶ d) →
          ((CategoryTheory.Bicategory.precomposing a b c).obj f).comp
              ((CategoryTheory.Bicategory.postcomposing a c d).obj h) ≅
            ((CategoryTheory.Bicategory.postcomposing b c d).obj h).comp
              ((CategoryTheory.Bicategory.precomposing a b d).obj f)