Issues

• Make build: strict-test always fails; Categories files missing from timing-html/dep-graph targets; other small issues

  HoTT/Coq-HoTT#2425 · Filter by author jdchristensen opened on Oct 9, 2026

• Full subcategories as induced categories

  HoTT/Coq-HoTT#2391 · Filter by author Alizter opened on Sep 5, 2026

• Generalise displayed categories to work over arbitrary total spaces

  HoTT/Coq-HoTT#2390 · Filter by author Alizter opened on Sep 4, 2026

• integrate fcc + alectryon support directly into alectryon and upstream

  HoTT/Coq-HoTT#2375 · Filter by author Alizter opened on Jul 6, 2026

• make https://hott.github.io and https://hott.github.io/Coq-HoTT work

  HoTT/Coq-HoTT#2365 · Filter by author jdchristensen opened on May 12, 2026
  4

  

• use .expected files when dune is 3.22

  HoTT/Coq-HoTT#2345 · Filter by author Alizter opened on Feb 17, 2026

• Generate docs using latest released version of rocq

  HoTT/Coq-HoTT#2343 · Filter by author Alizter opened on Jan 11, 2026

• When Rocq 9.0 is our minimum...

  HoTT/Coq-HoTT#2322 · Filter by author jdchristensen opened on Nov 4, 2025
  3

  

• Dealing with two competing conventions

  HoTT/Coq-HoTT#2273 · Filter by author patrick-nicodemus opened on Apr 9, 2025
  1

• WildCat notation

  HoTT/Coq-HoTT#2271 · Filter by author patrick-nicodemus opened on Mar 31, 2025
  18

• Remove reversible coercions throughout the library

  HoTT/Coq-HoTT#2264 · Filter by author patrick-nicodemus opened on Mar 21, 2025
  5

• Homepage update?

  HoTT/Coq-HoTT#2243 · Filter by author patrick-nicodemus opened on Mar 6, 2025
  4

• Generate timing reports with dune

  HoTT/Coq-HoTT#2230 · Filter by author Alizter opened on Feb 24, 2025

• Files in theories/ folder

  HoTT/Coq-HoTT#2155 · Filter by author jdchristensen opened on Dec 15, 2024
  5

• Stepping through HoTT files in a IDE with an opam installed HoTT (regression)

  regression
  HoTT/Coq-HoTT#2146 · Filter by author MSoegtropIMC opened on Dec 4, 2024
  7

• Deduce 0-groupoid universal properties from GraphQuotient

  HoTT/Coq-HoTT#2136 · Filter by author gio256 opened on Nov 8, 2024

• Equivalences of wild categories

  HoTT/Coq-HoTT#2128 · Filter by author ThomatoTomato opened on Nov 1, 2024
  4

• Host docs for PRs

  cidocumentation
  HoTT/Coq-HoTT#2107 · Filter by author Alizter opened on Oct 4, 2024
  3

• Localization of modules

  algebra
  HoTT/Coq-HoTT#2094 · Filter by author Alizter opened on Sep 20, 2024
  4

• Adapt ring tactic to HoTT

  HoTT/Coq-HoTT#2093 · Filter by author Alizter opened on Sep 20, 2024
  2

• Define free R-module as tensor product of R and free abelian group

  good first issue
  HoTT/Coq-HoTT#2080 · Filter by author Alizter opened on Sep 7, 2024

• Allow subgroups to be defined by predicates that don't take values in h-props

  HoTT/Coq-HoTT#2069 · Filter by author jdchristensen opened on Aug 30, 2024

• Add functorality of cokernels and quotients for AbGroup

  HoTT/Coq-HoTT#2067 · Filter by author Alizter opened on Aug 30, 2024

• Fundamental theorem of arithmetic

  good first issue
  HoTT/Coq-HoTT#2059 · Filter by author Alizter opened on Aug 16, 2024
  3

• Add HasEquivs instance for MatrixCat

  good first issue
  HoTT/Coq-HoTT#2046 · Filter by author Alizter opened on Aug 6, 2024
  1