Issues

• Rewrites under both arguments of ≈ cap the hom level at prod_rect through PER_type_morphism (iffT); the cap survives Qed

  jwiegley/category-theory#1371 · Filter by author jwiegley opened on Oct 8, 2026

• Factor the algebraic forgetful functors (Grp, Rng, Mod) through PropSets; quotient and reflexive coequalizers preserved there

  jwiegley/category-theory#1369 · Filter by author jwiegley opened on Oct 8, 2026

• Give the constant functor one light, universe-faithful home (Constant_Functor, const_fun, Point, PointAt)

  jwiegley/category-theory#1367 · Filter by author jwiegley opened on Oct 8, 2026

• Absoluteness as one notion: Constant.v's witnesses at cone level, naming, and separation

  jwiegley/category-theory#1365 · Filter by author jwiegley opened on Oct 8, 2026

• Equalizer conversions at any Parallel-shaped diagram, and Finite.v's remaining rows

  jwiegley/category-theory#1364 · Filter by author jwiegley opened on Oct 8, 2026

• Annotate the universe binders of Compose, Opposite_Functor and the cone vocabulary (hom-level minimization artifacts)

  jwiegley/category-theory#1363 · Filter by author jwiegley opened on Oct 8, 2026
  3

• Generalize LeftInverse.v's ImageIso to full and faithful functors, giving both strict isomorphisms of #475's corestrictions

  jwiegley/category-theory#1361 · Filter by author jwiegley opened on Oct 8, 2026

• Riehl 5.2: the free vector space and maybe monads as witnesses that every algebra is free (conditional)

  jwiegley/category-theory#1359 · Filter by author jwiegley opened on Oct 8, 2026

• A shared Eilenberg–Moore lemma for term-model monads, keeping identity components

  jwiegley/category-theory#1357 · Filter by author jwiegley opened on Oct 8, 2026

• Ab ≅ RMod ℤ, and the free abelian group monad as the R = ℤ case of the free module monad

  jwiegley/category-theory#1356 · Filter by author jwiegley opened on Oct 8, 2026

• Theory/Universal/Arrow.v: ump_universal_arrows is Qed, so counits of adjunctions from universal arrows never compute

  enhancement
  jwiegley/category-theory#1353 · Filter by author jwiegley opened on Oct 7, 2026

• Riehl 5.6.10 by Theorem 5.6.5(ii): U : R-Mod → Ab creates colimits through monadic creation (follow-up of #465, after #1008)

  book:riehlcoverage-gapkind:theory
  jwiegley/category-theory#1341 · Filter by author jwiegley opened on Sep 30, 2026

• Riehl 4.6.13(v): sheaves reflective in presheaves by sheafification (follow-up of #370, after #890)

  book:riehlcoverage-gapkind:theory
  jwiegley/category-theory#1335 · Filter by author jwiegley opened on Sep 27, 2026

• Mac Lane V.6/V.8: the Stone-Cech compactification on the Prop-valued Top (after #1328)

  book:maclanecoverage-gapkind:theory
  jwiegley/category-theory#1329 · Filter by author jwiegley opened on Sep 24, 2026

• Re-encode Top/CompHaus with a Prop-valued topology (homs at the points' universe)

  coverage-gapkind:theory
  jwiegley/category-theory#1328 · Filter by author jwiegley opened on Sep 24, 2026

• Mac Lane V.8 Ex 3: Watt's theorem (covariant) and the SAFT route without Untruncate

  book:maclanecoverage-gapkind:theory
  jwiegley/category-theory#1326 · Filter by author jwiegley opened on Sep 24, 2026

• Riehl 4.7.10: SAFT under Riehl's hypothesis list (intersections), with Corollary 4.7.13 and E.1(iii)

  book:riehlcoverage-gapkind:theory
  jwiegley/category-theory#1324 · Filter by author jwiegley opened on Sep 24, 2026

• A non-circular solution set for Grp_Forget: the generated-subgroup API, and the Set floor that is a DiscreteCat_Functor artifact

  jwiegley/category-theory#1309 · Filter by author jwiegley opened on Sep 12, 2026

• Awodey 8.8: The adjoint triple ∃_f ⊣ f* ⊣ ∀_f on subobjects in a topos

  book:awodeycoverage-gapkind:theory
  jwiegley/category-theory#1272 · Filter by author jwiegley opened on Sep 6, 2026

• Instance/Field.v: F2_Field_dec and Q_Field_dec are Qed, blocking all reduction at consumers that compute

  jwiegley/category-theory#1199 · Filter by author jwiegley opened on Aug 20, 2026

• rocq-dev CI: rocq-equations.dev fails to build against Rocq master (Unbound module Summary.Ref)

  jwiegley/category-theory#1195 · Filter by author jwiegley opened on Aug 20, 2026

• MacLane III.3: Free product in Grp, tensor in CRng, and Riehl 4.6.6 — the remainder of #324

  jwiegley/category-theory#1194 · Filter by author jwiegley opened on Aug 20, 2026
  1

• After the indexed hom bijections: the discrete-opposite translation, and naturality in the remaining variables

  jwiegley/category-theory#1189 · Filter by author jwiegley opened on Aug 20, 2026

• After Kan coyoneda: pricing the Δ-reading upgrade, the presheaf orientation, and naturality in K

  jwiegley/category-theory#1187 · Filter by author jwiegley opened on Aug 20, 2026

• After postcomposition: is faithfulness necessary for fullness, and can the construction reach the Sets-enlargement instance?

  jwiegley/category-theory#1185 · Filter by author jwiegley opened on Aug 19, 2026