LOGIKSEMINARIET STOCKHOLM-UPPSALA

Peter Aczel (Manchester och SCAS)

       Identity Types and Type Setups

Kl 10.30, 18 februari i sal Eng 2-0022, Uppsala universitet (i 
Filosofiska institutionens lokaler vid Engelska parken).

Abstract:  In the first part of my talk I will review some of the
rules for identity types that have been considered and discuss how
they are related to each other when Pi and Sigma types are not
available in the type theory.

In the second part of the talk I will introduce the notion of a type
setup.  This is an abstraction from the notion of a (dependent) type
theory in which types and terms are abstract while contexts are kept
as sequences of variable declarations.  The notion is closely related
to Peter Dybjer's notion of a category with families.  But while that
notion treats contexts as abstract objects of a category and is
intended as giving a notion of possible mathematical semantics for
type theories, the notion of a type setup is intended to capture an
abstract syntactic notion of type theory at a more concrete level of
abstraction.  I believe that the notion of a type setup can be used to
conveniently express some results of Richard Garner concerning
identity contexts.