From: Benedict Kavanagh <b.i.kavanagh@sms.ed.ac.uk>
To: categories@mta.ca
Subject: LFCS Free Topos Seminar, Phil Scott, 13 July, Edinburgh, Scotland
Date: Mon, 4 Jul 2011 12:21:22 +0100 [thread overview]
Message-ID: <E1QdiGS-0001Rq-9n@mlist.mta.ca> (raw)
If you will be in Scotland on July 13 please consider attending an afternoo=
n of
lectures on the free topos by Philip Scott. You will find the announcement =
below.
-Ben
---------------------------------------------------------------------------=
---
Laboratory for Foundations of Computer Science (LFCS),=20
University of Edinburgh presents:
***** What is the free topos? *****
by Philip Scott, Dept. of Mathematics and Statistics, University of Ottawa
SICSA Distinguished Visiting Fellow
More information available at:
http://wcms.inf.ed.ac.uk/lfcs/events/prof.-phil-scott-free-topos-lecture
Location: Informatics Forum, Room 4.31/33, School of Informatics, Universit=
y of Edinburgh, Scotland.
Time: 14:00-17:00, 13 July 2011.
Abstract:
The free topos is a model of intutionistic higher order
logic, and may be thought of as a universe of sets for a moderate
intuitionist. In this lecture, we give an introduction to free topoi
(on graphs); in particular, we discuss metamathematical properties of
the free topos (generated by the empty graph), which is an initial
object in the category of all toposes with logical functors.
The free topos satisfies many interesting properties corresponding to
proof-theoretic principles of intuitionistic higher-order logic, and
indeed allows us to reprove these properties in an elegant algebraic
way. This includes such familiar properties as the existence and
disjunction properties, uniformity principles, independence of
premisses, as well as various choice principles. We shall discuss
uniform categorical proofs, based on gluing methods of Peter Freyd, as
well as connections with realizability. If time permits, we discuss
more recent results.
-----------------------
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
reply other threads:[~2011-07-04 11:21 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
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=E1QdiGS-0001Rq-9n@mlist.mta.ca \
--to=b.i.kavanagh@sms.ed.ac.uk \
--cc=categories@mta.ca \
/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).