David Corfield quotient types

The dual problem to how to deal with subsets, which is, e.g., does an element of the type ‘Red Apple’ also belong to the type ‘Apple’? In an intrinsic type theory, this amounts to a projection, omitting the component which is the warrant of redness. So $a: Red\;Apple$, $Tasty(p_1(a)): Prop$.

Now the dual problem: If we have a type which is a set, and then devise an equivalence relation on the set, we can generate a new set by quotienting. The new set and the equivalence relation as groupoid are equivalent. The set of colours and the set of colour impressions as identified are equivalent. When someone says of an abstracted class that it is made up of its instances, they should say instances provided with the new identity relation.

A case of this is book qua physical tome, and book qua information source. When I say “I love this book. Shame it’s in such poor condition”, it seems that I must be referring to the same entity.

“ I love this book. Shame this copy is in such poor condition”. Can I ask “Does ‘this book’ and ‘it’ refer to the same thing? No, they belong to different types. Are these the same book, pointing to two volumes. $Id_{Book_2}(q(b_1), q(b_2))$

When OM points out that we say “Where do you keep War & Peace? On the top shelf.” this is allowable due to factorisation $Book_1 \to Place$. The bookshop staff can say this even if other books, Anna Karenina, are spread throughout.

HoTT book on quotienting, sec. 6.10, uses $q(a)$ for the image of $a$.

$Colour \simeq Colour\;impression/indistinguishable$, (or we might have already factored out to give object stability or at least the identification of impressions from the same place).

We shouldn’t say, e.g., that ‘red’ refers to the class of red impressions, but rather red impressions under indistinguishability. The type of red impressions is the pullback of the point $red:\ast \to Colour$ along the projection.

Philosophy gets itself very confused by this quotienting, how to switch between the groupoid of an equivalence relation and the set of equivalence classes. So you say ‘this direction’ pointing to a line, and it seems hard to realise that you can point to a specific line but as existing in a type where identity is parallelism.

Confusion dates back (at least) to Berkeley criticising Locke’s general ideas: How can there be an idea of a triangle which does have any particular size? How can there be an idea of a triangle which is neither isosceles, nor equiangular, nor right-angled, nor anything in particular at all? How can it be intelligible to indicate something abstract through an instance most of whose properties are irrelevant?

Evidently some quotienting on shapes under different transformation groups occurs. So I can work on an instance of a triangle, but do so with respect to a particular identity.

As with the red apple, it’s easy to use the same term as element of both types.

A type characterises the objects that belong to it by specifying what counts as an element and what counts as an identity between elements.

Is this why we say ‘The wombat is a nocturnal creature’, playing on the loss of identity from the individual animals in situations where the property applies to all of the class? So the map, $Animal \to Prop$ given by ‘is nocturnal’ respects the equivalence $Animal \to Species$. The image of any particular wombat, $q(this\;wombat)$, is glossed as ‘the wombat’.

A free action of a group on a set provides a set quotient, the dependent sum.

I guess this is part of the same story as WLOG. You work on an element of a type, but now considering it as existing under a new identity relation, such as in the bracket type. Then anything you show for $q(a)$ for some element $a: A$ projected to the set quotient $A/R$ applies to all the preimages of $q(a)$.

So why in Pythagoras’s theorem do we start with a specific right angled triangle? Perhaps we work on all triangles identified if their largest angle matches. The technique of only mentioning properties that must hold.

Consider all possible triangles in a plane either with ordered/unordered vertices, triangles in a plane up to congruence, triangles up to similarity. Triangles specified as three distinct nonlinear points in R^2. Triangles in 3-space, and so on.

Then consider possible/actual triangles drawn on a blackboard, where the blackboard does or doesn’t have axes, which are or are not numbered. Then triangles drawn in chalk up to a degree of tolerance, and so on. We have a great many types here, all of which have, in a sense, elements that are triangles.

Take the predicate ‘is isosceles’. It’s not clear where its natural home lies. It’s quite possible to use this predicate for items in any of the kinds above (although it wouldn’t apply to triangles up to projection). Opportunities for predicate versatility and copredication are very abundant.

‘Is right-angled’ is another case. I draw a triangle of 3, 4, 5 units in chalk on the board marked with units, and say that it’s right-angled. It’s ambiguous what I’m referring to. But if I say ‘this triangle was found by the Egyptians to be right-angled’, I mean this triangle up to similarity.

What we have is a web of types and maps between them.

When we have a map between types $A \to B$, any predicate on $B$, (so a map $B \to Prop$), can automatically be made into a predicate on $A$ ($A \to B \to Prop$).

In cases where $A \to B$ is an inclusion, we generally use the same word for the predicate, e.g., we can use the predicate ‘is isosceles’ for the type of triangles drawn in the upper right quadrant of a plane, when we have it for all triangles in the plane.

In cases where $A \to B$ is a surjection formed by identifying certain pairs of elements of $A$, then we often use the same word for the predicate applied to $A$, e.g., we use isosceles for a triangle up to congruence, but also for a particular triangle in the plane.

Going the other way is more involved. For any predicate, $P$, on $A$,there are automatically two predicates on $B$ (whether all or some of the elements in the preimage of $b$ in $B$ satisfy the predicate). Situations where we tend to use the same term for the predicate include those where $A \to B$ is an inclusion, and there’s a natural extension of the predicate to all of $B$ (truth extension is like induction).

Also when $A \to B$ is a surjection formed by identifying certain pairs of elements of $A$, then when a predicate holds for a class of $A$s which are all identified in $B$, then we may apply the predicate to the element in $B$.

We see some of this in action in the case of four types: physical books, books up to information equivalence, physical books in this room, books in this room up to information equivalence.

A predicate on information sources is readily transferred back to any of these types, e.g., ‘is informative’ to physical books or physical books in this room or information sources in this room. A predicate on physical books, e.g., ‘is red’, typically doesn’t transfer to information sources, but in cases such as Mao’s Red book, where all instances are red, this is OK.

In the case of books in the room, it is also OK to send ‘is on the top shelf’ to the same named predicate for information sources if all copies are gathered there. ‘War & Peace is on the top shelf’ stands for ‘All copies of War & Peace in this room are on the top shelf’. But we can’t ask on the latter where precisely on the top shelf, as though seeking a particular tome.

Counting takes place in a type. We have vegetables on a table, and vegetables on a table up to equivalence. Any time we have a set of elements all connected by mutual identities this counts as 1, so in Ofra’s example, the potatoes count as 1 as elements of the second type, but 3 as elements of the first.

(The types of triangles I started with are known as moduli spaces, and have interesting structures.)

Returning to the mathematical case, this predicate variability as you call it is everywhere in informal mathematical speech. It’s interesting then to see mathematicians take on the task of formalising theorem-proving, and notably of late this is taking place using a (dependently) typed language, see, e.g., Kevin Buzzard’s use of Lean in his Xena project that Gavin assisted on.

Lean can’t play fast and loose with the informal practice of sharing predicate names. If you were doing geometry, you would have to specify which type you were referring to when predicating ‘is isosceles’. A predicate can only be defined in terms of the single type it belongs to. But this tallies with how I see things, that in ordinary language there is a huge amount of tacit, non-indicated, typing going on. When it comes to working with computers, we need to make explicit this typing. When we work with a property such as ‘is isosceles’, it will have to be (is isosceles)_X for a range of types X. We see this has practical consequences. If I indicate an isosceles triangle keeping its type tacit, only in some cases can you ask me for the length of the equal sides; only in some cases can you ask me whether the two equal sides are the first two sides; and so on.