Stockholm–Göteborg meeting on Wednesday, 12 December 2018 in Göteborg


11:30–12:15Erik PalmgrenA setoid model of extensional Martin-Löf type theory in Agda
13:15–13:45Thierry CoquandA remark on sheaf models of type theory
13:45–14:15Andreas AbelLessons learnt from implementing a runnable well-typed interpreter for C-- in Agda
14:15–15:00Menno de BoerThe gluing construction for path categories
15:30–15:50Peter LeFanu LumsdaineA Coq formalisation of the initiality conjecture
15:50–16:30Guillaume BrunerieAn Agda formalization of the initiality conjecture
16:30–17:15Hugo MoeneclaeyFinitary higher inductive types in the groupoid model
18:00 dinner