∀ {X Y Z : DistLat} (f : X ⟶ Y) (g : Y ⟶ Z),
  DistLat.ofHom (LatticeHom.dual (DistLat.Hom.hom (CategoryTheory.CategoryStruct.comp f g))) =
    CategoryTheory.CategoryStruct.comp (DistLat.ofHom (LatticeHom.dual (DistLat.Hom.hom f)))
      (DistLat.ofHom (LatticeHom.dual (DistLat.Hom.hom g)))