Re: Bottom line to: Does equality between sets contradict the philosophy behind structural set theory?

Re: Bottom line to: Does equality between sets contradict the philosophy behind structural set theory?

[Patrik Eklund]

Dear Leopold,

Now I do want to reply to your posting, since you explicitly suggest
"one should use the definition from *dependent type theory*", and I
disagree.

Under this mailing list I have posted a number of times about formal
term constructions including the formal lambda term construction. We all
know that if we comply with the classical natural language based
definition of lambda terms, we will have unwanted terms. There are
tricks to deal with that, but it's not a very clean way to do it.

In dependent type theory you would have to make '->' as a binary
operator which provides ->(x,y) as a new type, assuming x and y are
types. However, this type constructor does not fit into the original
signature, so you magically bring it in from the outside, so as to say.
What you would need to do is to split into levels of signatures, so that
all type constructors are integrated as operators, and for which you
need semantics. Then you will be able to handle 'lambda' as the informal
symbol it is (as Church said in 1940). This approach is not yet fully
developed, but there are ways to proceed.

What I basically say is that creating informal and impredicative
dependent type theory as a kind of a supervisor for CT, will just add to
the problems you already mentioned. Fixing one problem by simply (or
dependently in this case) adding another problem, is typical for
computer scientists (I'm of them), and doesn't support constructive
dialogue between math and comp sci. This is my credo.

What I perfectly agree upon is your saying that we need to distinguish
things by considering types. I fully support that view. Eventually we
need then to deal with the 'powertype', and in CS type theory we do not
have a satisfactory solution for it, I would say. Others will say other
things, I know.

All the best,

Patrik

www.glioc.com

PS CT readers feeling not yet so well worsed in type handling in
programming languages might want to read something about types e.g. in
ML and Haskell, and other sibling languages, in order to realize how CS
struggles with type constructors. In the end, compilation through
intermediate languages already give hints that problems may arise, and
once we get to compiling into machine code, it's basically a mess, from
math and logic point of view.



On 2017-02-27 22:40, Leopold Schlicht wrote:
> I'm thankful for all the both private and public emails I got in
> consequence of my question "Does equality between sets contradict the
> philosophy behind structural set theory?", especially the emails I got
> from Ingo Blechschmidt, Fred Linton, Bob Rosebrugh, and Marquis
> Jean-Pierre were helpful.
>
> Let me briefly sum up what I learnt: If one wants to be fussy, and
> looks to the question from a "formal system" point of view, then I'm
> right: Once one puts all morphisms in one big bag and talks about dom
> and codom as "functions" that both specify a *unique* objects, one
> can't get around using an equality between sets, which doesn't make
> sense in a setting of structural set theory. Instead, one should use
> the definition from *dependent type theory*:
>
> a category consists of a collection Ob of objects and for each pair
> (x, y) of objects in Ob a set Hom(x, y) of morphisms x -> y. Writing
> f: x -> y is then just a type declaration (and not a statement that is
> either true or false!) that declares f to be in the collection Hom(x,
> y). We are not supposed to compare morphisms of different type. But
> however, there should be a local equality on each set Hom(x, y) so
> that we can discuss when two morphisms f, g: x -> y of the same type
> are equal.
>
> But, as Fred Linton pointed out, natural language is quite flexible
> and being written in an informal language, as almost all math books
> are, one shouldn't interpret everything literally. Writing dom(f) = A
> for example should just abbreviate that we consider A to be the domain
> of f???the authors didn't intend to seriously discuss whether two sets
> are equal or not, it's just a piece of notation. Thus, there isn't
> really a fault in the book by Lawvere and Rosebrugh.
>
> Thanks again,
> Leopold
>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Bottom line to: Does equality between sets contradict the philosophy behind structural set theory?

[Thomas Streicher]

For categories C internal to a category BB with finite limits equality
on objects is given via the diagonal of Ob(C).
For split fibrations over BB equality of objects is in general not
recognized in the base even in the discrete case.
Homotopy Type Theory is a framework where one cannot speak about
equality of objects in general. This can be seen very clearly in the
groupoid model. Types are groupoids and families of types are isofibrations.
Diagonals of groupoids are not isofibration unless the groupoid is discrete.

Thomas




[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Bottom line to: Does equality between sets contradict the philosophy behind structural set theory?

[Leopold Schlicht]

I'm thankful for all the both private and public emails I got in
consequence of my question "Does equality between sets contradict the
philosophy behind structural set theory?", especially the emails I got
from Ingo Blechschmidt, Fred Linton, Bob Rosebrugh, and Marquis
Jean-Pierre were helpful.

Let me briefly sum up what I learnt: If one wants to be fussy, and
looks to the question from a "formal system" point of view, then I'm
right: Once one puts all morphisms in one big bag and talks about dom
and codom as "functions" that both specify a *unique* objects, one
can't get around using an equality between sets, which doesn't make
sense in a setting of structural set theory. Instead, one should use
the definition from *dependent type theory*:

a category consists of a collection Ob of objects and for each pair
(x, y) of objects in Ob a set Hom(x, y) of morphisms x -> y. Writing
f: x -> y is then just a type declaration (and not a statement that is
either true or false!) that declares f to be in the collection Hom(x,
y). We are not supposed to compare morphisms of different type. But
however, there should be a local equality on each set Hom(x, y) so
that we can discuss when two morphisms f, g: x -> y of the same type
are equal.

But, as Fred Linton pointed out, natural language is quite flexible
and being written in an informal language, as almost all math books
are, one shouldn't interpret everything literally. Writing dom(f) = A
for example should just abbreviate that we consider A to be the domain
of f—the authors didn't intend to seriously discuss whether two sets
are equal or not, it's just a piece of notation. Thus, there isn't
really a fault in the book by Lawvere and Rosebrugh.

Thanks again,
Leopold


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]