BEGIN:VCALENDAR
VERSION:2.0
PRODID:ILLC Website
BEGIN:VEVENT
UID:/NewsandEvents/Events/Upcoming-Events/newsitem
/7452/22-June-2016-Colloquium-on-Mathematical-Logi
c-Fabio-Pasquali
DTSTAMP:20160609T000000
SUMMARY:Colloquium on Mathematical Logic, Fabio Pa
squali
ATTENDEE;ROLE=Speaker:Fabio Pasquali
DTSTART:20160622T160000
DTEND:20160622T170000
LOCATION:Room 610 of the Mathematics (Hans Freuden
thal) building, Budapestlaan 6, Utrecht
DESCRIPTION:Maietti and Rosolini generalized the n
otion of exact completion of a category with finit
e limits to that of elementary quotient completion
of hyperdoctrines. A hyperdoctrine will be denote
d by (C,P) and can be thought of as a many-sorted
logic P where sorts are objects of the category C.
The elementary quotient completion of (C,P), deno
ted by (Cq,Pq), is a new hyperdoctrine whose base
Cq is closed under effective quotients of equivale
nce relations expressed in the logic of Pq. In t
his talk we focus on triposes, a special class of
hyperdoctrines, introduced in by Hyland, Johnstone
and Pitts with the purpose (among others) of free
ly creating an elementary topos out of any given t
ripos. This mentioned construction is known under
the name of tripos-to-topos construction. We chara
cterize when the tripos-to-topos construction fact
ors through an elementary quotient completion. We
will show that this happens if and only if the sta
rting tripos validates a form of choice, which we
call rule of epsilon choice as it is inspired by H
ilbert's epsilon operator. For abstracts and more
information, see http://www.staff.science.uu.nl/~
ooste110/seminar.html or contact Benno van den Ber
g (bennovdberg at gmail.com).
X-ALT-DESC;FMTTYPE=text/html:\n Maietti
and Rosolini generalized the notion of exact compl
etion of a category with finite limits to that of
elementary quotient completion of hyperdoctrines.
A hyperdoctrine will be denoted by (C,P) and can b
e thought of as a many-sorted logic P where sorts
are objects of the category C. The elementary quot
ient completion of (C,P), denoted by (Cq,Pq), is a
new hyperdoctrine whose base Cq is closed under e
ffective quotients of equivalence relations expres
sed in the logic of Pq.

\n \n
In this talk we focus on triposes, a special class
of hyperdoctrines, introduced in by Hyland, Johns
tone and Pitts with the purpose (among others) of
freely creating an elementary topos out of any giv
en tripos. This mentioned construction is known u
nder the name of tripos-to-topos construction. We
characterize when the tripos-to-topos construction
factors through an elementary quotient completion
. We will show that this happens if and only if th
e starting tripos validates a form of choice, whic
h we call rule of epsilon choice as it is inspired
by Hilbert's epsilon operator.

\n \n
For abstracts and more information, see http://www.staff.science.u
u.nl/~ooste110/seminar.html or contact Benno v
an den Berg (bennovdberg at gmail.com).

\n
URL:/NewsandEvents/Events/Upcoming-Events/newsitem
/7452/22-June-2016-Colloquium-on-Mathematical-Logi
c-Fabio-Pasquali
END:VEVENT
END:VCALENDAR