All issues

Search results

Update Dependencies fails nightly: the mathlib pin has moved off master

Status: Open.

#202 In emilyriehl/infinity-cosmos;

· alejandro-soto-franco opened on Aug 12, 2026

Bumping mathlib to fcdfe22 would break the build

dependency-incompatibilityAutomated tracker opened by downstream-reportsAutomated tracker opened by downstream-reports

Status: Open.

#201 In emilyriehl/infinity-cosmos;

· github-actions opened on Aug 7, 2026

Updates available but manual intervention required

auto-update-lean-failAuto update for Lean dependenciesAuto update for Lean dependencies

Status: Open.

#132 In emilyriehl/infinity-cosmos;

· github-actions opened on Jun 22, 2025

Brown factorization lemma

Status: Open.

#117 In emilyriehl/infinity-cosmos;

· emilyriehl opened on Mar 21, 2025

equivalences are homotopy equivalences

Status: Open.

#116 In emilyriehl/infinity-cosmos;

· emilyriehl opened on Mar 21, 2025

stability of trivial fibrations under Leibniz cotensor with monomorphisms

Status: Open.

#115 In emilyriehl/infinity-cosmos;

· emilyriehl opened on Mar 21, 2025

stability of trivial fibrations under conical cosmological limits

Status: Open.

#114 In emilyriehl/infinity-cosmos;

· emilyriehl opened on Mar 21, 2025

define the underlying category of an ∞-cosmos

Status: Open.

#113 In emilyriehl/infinity-cosmos;

· emilyriehl opened on Mar 21, 2025

define equivalences and trivial fibrations in an ∞-cosmos

Status: Open.

#112 In emilyriehl/infinity-cosmos;

· emilyriehl opened on Mar 21, 2025

define equivalences (and trivial fibrations) of quasi-categories

Status: Open.

#111 In emilyriehl/infinity-cosmos;

· emilyriehl opened on Mar 21, 2025

conical limits from unenriched limits and tensors

Status: Open.

#110 In emilyriehl/infinity-cosmos;

· emilyriehl opened on Mar 21, 2025

tensors in an enriched ordinary category

Status: Open.

#109 In emilyriehl/infinity-cosmos;

· emilyriehl opened on Mar 21, 2025