Commit 2026-03-09 11:53 4317fcb5

View on Github →

chore: make SimplicialObject and SSet abbrevs (#35298) Currently, use of projections like X.obj and X.map when X : SSet constitutes a defeq abuse at reducible transparency, because SSet is a def instead of an abbrev. It makes more sense to have it as an abbrev. The same applies to the related SimplicialObject and their Truncated variants.

Estimated changes