BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:Induction for Cycles - Nicolai Kraus (University o
f Birmingham)
DTSTART:20200131T110000Z
DTEND:20200131T120000Z
UID:TALK4151AT
URL:/talk/index/4151
DESCRIPTION:(Joint work with Jakob von Raumer.)\n\nConsider pa
ths in a given graph. If we want to prove a certai
n property for all paths\, the obvious approach is
to try induction on [the length of] paths. If we
want to prove a certain property for all *closed*
paths a.k.a. cycles (first vertex = last vertex)\,
this does not work since closed paths are not ind
uctively generated (if we remove an edge from a cl
osed path\, it is not closed any more).\n\nWe have
studied this situation because certain coherence
conditions in homotopy type theory can be formulat
ed in terms of cycles. The problem discussed above
then makes it difficult to verify these condition
s in the case of natural applications. \n\nWe buil
d on the observation that\, at least in all those
cases we are interested in\, the graph is given by
the symmetric closure of a locally confluent and
Noetherian (co-well-founded) proof-relevant relati
on. Under these assumptions\, we construct a new N
oetherian relation on cycles which allows co-well-
founded induction. As a consequence\, whenever we
have to prove a property for all cycles\, it suffi
ces to prove the property for the empty cycle and
for those given by local confluence.\n\nAn applica
tion in homotopy type theory is the statement that
the fundamental groups of the free higher group o
ver a set are trivial.
LOCATION:Computer Science\, The Sloman Lounge (UG)
CONTACT:Anupam Das
END:VEVENT
END:VCALENDAR