# Léo Mangel: Formalisation of Cartier's delooping of the sign homomorphism

Datum objave: 6. 6. 2022
Seminar za temelje matematike in teoretično računalništvo
četrtek
9
junij
Ura:
10.00 - 12.00
Lokacija:
This raises the question what the deloopings of familiar group homomorphisms are. The goal of our project was to find an explicit description of the delooping of the sign homomorphism from $S_n$ to $S_2$. I will present a definition attributed to Cartier, making use of the univalence axiom. All the work presented was formalised with Agda in the agda-unimath library.