∀ {X : Type u_5} {Y : Type u_6} [inst : TopologicalSpace X] [inst_1 : SizeOf X] [inst_2 : SizeOf Y] (toFun : X → Y)
  (isLocallyConstant : IsLocallyConstant toFun), sizeOf { toFun := toFun, isLocallyConstant := isLocallyConstant } = 1