Re: [HoTT] Re: Where is the problem with initiality?

[Richard Williamson <rwilli...@gmail.com>]

> Actually I am teaching Python (by choice)

Nice!

> And second the untyped version is only the first step before I
> understand what I am doing at which point I am able to make the
> concepts involved more precise.

Interesting! If I understood you correctly, I would say that I
program in Python in the opposite way: I always have the types in
my mind, and these guide the code, even though I do not write
them down explicitly. In other words, I think that I program in
the way as you have in mind in the following sentence, but there
are benefits (flexibility, development time, etc) to me in
writing the code in Python rather than in a statically typed
language.

> In particular in a mathematical development I would expect that
> the objects involved are understood and hence can be given a
> specific type.

I like the following analogy...

> Actually, Python is dynamically typed, which is why I always compare it to
> set theory. Python has predicates to test wether an object belongs to an
> arbitrary type. This corresponds to the element relation in set theory. In
> contrast, strongly typed languages don't have predicates like this because
> you know statically what the type of an object is. In the same way in Type
> Theory typing is static hence it doesn't make sense to have an element
> relation.

...and the following is also true...

> I would think that once I understand the concepts involved in my
> construction I should be able to assign static types to them. That is
> certainly the case in programming but even more so for mathematical
> constructions.

...but I disagree with the implied conclusion that one will
always wish to write down those static types.

Suppose I wish to formalise a quick argument involving words in a
free group for instance. Does it really matter to me whether I am
actually working in a free group? Maybe any group would do for my
present purposes. Indeed, maybe any monoid would do. It is going
to save me a lot of time, and give more flexibility with regard
to how I incorporate my argument in a larger argument later, if I
can just jump in and start manipulating those words without
worrying yet about what type they have, even if I have a
particular type, or more than one type, in mind.

One might even argue that such a view is philosophically closer
to much mathematical practise, especially that influenced by
category theory: we are typically concerned with the properties
of an object (what we can do with it), not exactly with what it
is. To misappropriate the classic slogan: if it quacks like a
free group, it might as well be a free group.