University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Epimorphisms and Acyclic Types in Univalent Mathematics

Epimorphisms and Acyclic Types in Univalent Mathematics

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Jon Sterling.

We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of synthetic homotopy theory. We present examples and applications in group theory, such as the acyclicity of the Higman group, through the identification of groups with 0-connected, pointed 1-types. Many of our results are formalized as part of the agda-unimath library.

j.w.w. Ulrik Buchholtz and Egbert Rijke

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity