∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β]
  [inst_2 : SemilatticeSup γ] (f : SupHom β γ) (g : SupHom α β), (f.comp g).withTop = f.withTop.comp g.withTop