Add category of ω-sets - #373

Open

dschepler wants to merge 9 commits into

ScriptRaccoon:mainfrom

dschepler:omega-set

Commits on Sep 19, 2026

Add category of ω-sets
dschepler
committed
4d9da85
Fill in some more proofs
dschepler
committed
331345c
Fix previous rebase merge
dschepler
committed
c2986e7
Apply batched suggestions from code review

dschepler
and
ScriptRaccoon
committed
6bd829f
Revise to use terminology "compatible realizer transformer" instead of vague references to definition of morphism
dschepler
committed
8ff1829
Bring in the proof from the abandoned branch dschepler/CatDat/quasitopos that regular + extensive + quotients of congruences -> effective cocongruences, in order to show omega-Set has effective coc…
dschepler
committed
227a0ce
w-Set has an extremal cogenerator
dschepler
committed
4952c2d
Apply batched suggestions from code review

dschepler
and
ScriptRaccoon
committed
32e2edd

Commits on Sep 20, 2026

w-Set has an extremal generating family; also make a few "low-hanging fruit" adjustments in response to review comments
dschepler
committed
00b0981