From: Thomas Streicher <streicher@mathematik.tu-darmstadt.de>
To: Leopold Schlicht <schlicht.leopold@gmail.com>
Cc: categories@mta.ca
Subject: Re: Bottom line to: Does equality between sets contradict the philosophy behind structural set theory?
Date: Tue, 28 Feb 2017 15:24:55 +0100 [thread overview]
Message-ID: <E1cj9cC-0001jh-86@mlist.mta.ca> (raw)
In-Reply-To: <E1ciWzW-0007aE-0e@mlist.mta.ca>
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/ ]
next prev parent reply other threads:[~2017-02-28 14:24 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-02-27 20:40 Leopold Schlicht
2017-02-28 14:24 ` Thomas Streicher [this message]
2017-02-28 5:56 Patrik Eklund
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=E1cj9cC-0001jh-86@mlist.mta.ca \
--to=streicher@mathematik.tu-darmstadt.de \
--cc=categories@mta.ca \
--cc=schlicht.leopold@gmail.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).