Skip to content

Add additive categories infrastructure#2304

Merged
jdchristensen merged 3 commits into
HoTT:masterfrom
CharlesCNorton:patch-7
Jun 15, 2026
Merged

Add additive categories infrastructure#2304
jdchristensen merged 3 commits into
HoTT:masterfrom
CharlesCNorton:patch-7

Additive: drop unused imports and wrapper lemmas, fix field names

d80705f
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

2 warnings
nix
succeeded Jun 15, 2026 in 2m 19s