BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Calum Hughes (University of Manchester)
DTSTART:20240517T100000Z
DTEND:20240517T110000Z
DTSTAMP:20260409T225506Z
UID:TheoryCSBham/15
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/TheoryCSBham
 /15/">Models of Martin-Löf Type Theory and Algebraic Model Structures</a>
 \nby Calum Hughes (University of Manchester) as part of University of Birm
 ingham theoretical computer science seminar\n\nLecture held in Aston Webb\
 , WG12.\n\nAbstract\nKnown models of Martin-Löf Type Theory (MLTT) includ
 e isofibrations in the category of groupoids and Kan fibrations in the cat
 egory of simplicial sets. It is an open problem to prove constructively th
 at Kan fibrations model Homotopy Type Theory. One suggested way to approac
 h this problem is with an algebraic perspective\; the idea being that by k
 eeping track of the algebraic data throughout calculations\, proofs become
  more constructive. Classically\, normal isofibrations are the algebras fo
 r the right class of a type theoretic algebraic weak factorisation system 
 which form part of an algebraic model structure. Constructively\, however\
 , this link breaks down as this algebraic model structure fails to exist.\
 n\nIn this talk\, I will show how we can re-establish this connection by p
 roving constructively that cloven isofibrations are the algebras for the r
 ight class of a type theoretic algebraic weak factorisation system which f
 orm part of an algebraic model structure. I will also briefly discuss how 
 this result holds more generally\, providing an internal-groupoidal model 
 of MLTT with links to an algebraic model structure.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/15/
END:VEVENT
END:VCALENDAR