pith. sign in

arxiv: 2401.14106 · v3 · pith:ZH6LRLFGnew · submitted 2024-01-25 · 💻 cs.LO · math.AT· math.CT

Epimorphisms and Acyclic Types in Univalent Foundations

Ulrik Buchholtz , Tom de Jong , Egbert Rijke This is my paper
classification 💻 cs.LO math.ATmath.CT
keywords acyclictheorytypesepimorphismsfoundationsgrouphomotopymaps
0
0 comments X
read the original abstract

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 as developed in univalent foundations. 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.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. RankGraph-2: Lifecycle Co-Design for Billion-Node Graph Learning in Recommendation

    cs.IR 2026-06 unverdicted novelty 4.0

    RankGraph-2 jointly optimizes graph subsampling, pre-computed neighborhoods, and a co-learned cluster index for billion-node recommendation retrieval, reporting 3.8x recall gains and up to +0.96% CTR.

  2. RankGraph-2: Lifecycle Co-Design for Billion-Node Graph Learning in Recommendation

    cs.IR 2026-06 unverdicted novelty 4.0

    RankGraph-2 jointly optimizes graph construction, training, and serving for billion-node recommendation retrieval, reporting 3.8x recall gains and CTR/CVR improvements via subsampling, pre-computed neighborhoods, and ...