### Seminars for Pure Mathematics

Jan 19 2023 |

Ettore Aldrovandi (FSU) |

Computer based formalization of Group Theory and Categorical Algebra in Homotopy Type Theory |

Algebra and its Applications |

Time: 3:05 pm |

Location: LOV 0105 |

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... More |

Jan 26 2023 |

Ettore Aldrovandi (FSU) |

Computer based formalization of Group Theory and Categorical Algebra in Homotopy Type Theory (Part II) |

Algebra and its Applications |

Time: 3:05 pm |

Location: 0102 LOV |

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... More |