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

• $World Patch: Type$
• $Colour: Type$
• $ColourOf: [World Patch \to Colour]$
• $X: Type \vdash This X: X$
• $This Colour = ColourOf(ThisWorld Patch)$ (judgemental equality)
• $Prussian Blue: Colour$
• $This Colour = Prussian Blue : Colour$ (judgemental equality, way to define Prussian Blue by pointing to sample)
• $\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 $Colour$ 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.

Introduction/Elimination

How does identity fit with the way a type is given via introduction/elimination/computation?

Product type

Do I know what is $Id_{A \times B}(s, t)$, given $s, t: A \times B$.

So $r(s): Id_{A \times B}(s, s)$.

The elimination rule then says that if:

1. for any $s,t:A \times B$ and any reason $p:Id_{A \times B}(s,t)$ why they are the same, we have a type $C(s,t,p)$, and
2. if $s$ and $t$ are actually identical and $p:Id_{A \times B}(s,s)$ is the reflexivity proof $r(s)$, then we have a specified term $v:C(s,s,r(s))$,

then we can construct a canonically defined term $J(v;s,t,p):C(s,t,p)$ for any $s$, $t$, and $p:Id_{A \times B}(s,t)$, by “transporting” the term $v$ along the proof of equality $p$.

So let $C(s, t, p) = Id_A(\pi_1(s), \pi_1(t))$, and $r(\pi_1(s)): Id_A(\pi_1(s), \pi_1(s))$, then there is $J: Id_A(\pi_1(s), \pi_1(t))$.

Similarly for $\pi_2$.

Sum type

Do I know what is $Id_{A + B}(s, t)$, given $s, t: A + B$.

So $r(s): Id_{A + B}(s, s)$.

The elimination rule then says that if:

1. for any $s,t:A + B$ and any reason $p:Id_{A + B}(s,t)$ why they are the same, we have a type $C(s,t,p)$, and
2. if $s$ and $t$ are actually identical and $p:Id_{A + B}(s,s)$ is the reflexivity proof $r(s)$, then we have a specified term $v:C(s,s,r(s))$,

then we can construct a canonically defined term $J(v;s,t,p):C(s,t,p)$ for any $s$, $t$, and $p:Id_A(s,t)$, by “transporting” the term $v$ along the proof of equality $p$.

So let $C(s, t, p) =$, and $r(\pi_1(s)): Id_A(, )$, then there is $J: Id_A(, )$.