∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {W : Type u_5}
  [inst_2 : TopologicalSpace W] (f : C(W, X)) (g : C(X, Y)),
  LocallyConstant.comap (g.comp f) = LocallyConstant.comap f ∘ LocallyConstant.comap g