# Algebra and its Applications—Spring 2023

Earlier sessions are available here.

**Please note that the schedule is still in flux.**

## Schedule

- Jan 12
**Organizational meeting**

- Jan 19 & Jan 26
- Feb 2
- Feb 9
- Feb 16
*Reese Madsen*

- Feb 23
*Brandon Story*

- Mar 2
*Brandon Story*

- Mar 9
*Matthew Winters*

- Mar 16
**No meeting**(Spring Break) - Mar 23
*Matthew Winters*

- Mar 30
- Apr 6
- Apr 13
- Cindy Lester

- Apr 20
- Cindy Lester

- Apr 27

## Talks

### Ettore Aldrovandi

**Title:**Computer based formalization of Group Theory and Categorical Algebra in Homotopy Type Theory.**Abstract:**I describe some work in progress in collaboration with Keri D’angelo (Cornell — CS) to formalize crossed modules of groups, hence groups, in Homotopy Type Theory using the Agda proof assistant. No previous knowledge of Type Theory or Agda is required, and I will sketch the main concepts: types, univalence and h-level. I will also illustrate how to pass to higher h-levels beyond sets, thus enabling one to do “categorical algebra without categories.”