David Corfield
identity

What do we mean when we say

This colour is Prussian Blue?

One of two things (at least):

  • This is what Prussian Blue is (if you don’t know that)
  • Specification of this thing’s colour as prussian Blue

Type theoretic construction

  • WorldPatch:TypeWorld Patch: Type
  • Colour:TypeColour: Type
  • ColourOf:[WorldPatchColour]ColourOf: [World Patch \to Colour]
  • X:TypeThisX:XX: Type \vdash This X: X
  • ThisColour=ColourOf(ThisWorldPatch)This Colour = ColourOf(ThisWorld Patch) (judgemental equality)
  • PrussianBlue:ColourPrussian Blue: Colour
  • ThisColour=PrussianBlue:ColourThis Colour = Prussian Blue : Colour (judgemental equality, way to define Prussian Blue by pointing to sample)
  • p:Id Colour(ThisColour,PrussianBlue)\vdash p:Id_{Colour} (This Colour, Prussian Blue) (proof establishing claim that this colour is Prussian Blue)

What would be a proof of this latter identity? it would depend on the type formation of colour and other presuppositions. A proof might involve matching to a standard sample by transport, which presupposes a huge amount about colour constancy, the nature of objects, etc. Were something to change colour according to temperature, then we wouldn’t be happy taking our sample to an official chart kept in a room where the temperature changes. Rather like the metre rule or the kilogram once in Paris.

Also there is the issue of time. We still say “this colour” when pointing at a light whose hue changes. On the other hand, as Cassirer observed, we see objects as retaining their colour even when moved to other lighting conditions. E.g., a white piece of paper viewed under a green bush is still seen as white, perhaps invariance relative to surrounding light.

The type ColourColour evidently has more structure than merely being a set. For one thing there is a lighter/darker relation, for another there is a specificity ordering, e.g., Prussian Blue to Blue. Third, there is a proximity relation, orange is closer to red than blue is.

Last revised on February 6, 2015 at 11:32:10. See the history of this page for a list of all contributions to it.