The presentations will take place via Zoom. Links and Meeting ID's can be found below.

 

9:30-10:30

Link: https://stockholmuniversity.zoom.us/j/788997020

Meeting ID: 788 997 020

Formalizing Cartesian Cubical Sets in UniMath, Elisabeth Bonnevier

Homotopy type theory is a new formal system for doing constructive mathematics. As a system for logical deductions, its consistency must be verified by models. We will look at an axiomatization of constructive presheaf models of homotopy type theory and show that cartesian cubical sets satisfy four of these axioms. These results are formalized using the UniMath library for the proof assistant Coq, to which we also give an introduction.

Supervisor: Anders Mörtberg

 

11:00-12:00

Link: https://stockholmuniversity.zoom.us/j/678046973

Meeting ID: 678 046 973

An Analysis of Curiens Explicit Syntax for Dependent Type Theory, Philip Stassen

Categorical models of dependent type theories have been extensively studied over the years. A difficulty that arises is the coherence between syntactical and semantical substitution: The on-the-nose equalities of the syntax collide with the up-to-isomorphism equalities of categories. We say a model is ''strict'' if this mismatch is resolved and that it is ''weak'' if the mismatch persists.We present two dependent type theories, one of which has an additional term constructor, the explicit coercion. Pierre-Louis Curien has proven that locally cartesian closed categories provide strict models for the latter syntax without having to strictify the pullback – thereby resolving the mismatch by destrictifying the syntax instead. The type theory with explicit coercions can thus be used as intermediate step towards weak models for normal dependent type theories. We construct a lift from the normal type theory into the type theory that has explicit coercions. This function can then be used to prove coherence theorems and by that could serve as a tool to construct weak models for dependent type theories.

Supervisor: Peter Lumsdaine, Guillaume Brunerie

 

14:00-15:00

Link: https://stockholmuniversity.zoom.us/j/642223267

Meeting ID: 642 223 267

Kedjebråk, Fareyföljder och Fordcirklar, Olavus Rogowski

Inom matematikens historia så har bråk förekommit inom matematikens begynnelse och många matematiker världen över har jobbat med bråk. Idag så lär vi oss om bråk i grundskolan som ett steg i att kunna lära oss om högre nivå av matematik. Vi blickar ständigt framåt men i detta arbete så ska vi ta och stanna vid bråken och se vad vi kan lära oss om bråken om vi ändrar det förhållande vi har med dem. Vad händer om vi skulle utföra bråk addition genom att inte hitta först gemensam nämnare utan att direkt addera täljarna och nämnarna för sig, vad kan vi få ut av detta?
Vi har tidigare kunnat visualiserat bråk med hjälp av tårtdiagram eller kvadratdiagram men kan vi visualisera det på något annat sätt och går det att visualisera ett kedjebråk? I detta arbete så kommer vi att studera bråk utifrån dessa frågor där vi ser närmare på kedjebråk, Fareyföljder och Fordcirklar.

Supervisor: Håkan Granath, Annemarie Luger