Add Barr-exact, Barr-coexact, pretopos properties#103

Closed

dschepler wants to merge 15 commits into

ScriptRaccoon:mainfrom

dschepler:barr-exact

Commits on Apr 18, 2026

Initial addition of Barr-exact, Barr-coexact, pretopos properties and some implications
dschepler
committed
Add a few assignments for Barr-exactness
dschepler
committed
Resolve Barr-coexact for Set*
dschepler
committed
Revert addition of Barr-coexact implication of elemetary topos - it turns out the proof on ncatlab for categories monadic over Set requires the external axiom of choice on Set, so it will only gene…
dschepler
committed
Add manual resolution of Barr-coexact for Set
dschepler
committed
Add a couple cases which were unresolved by removing the faulty implication topos->Barr-coexact, but are still cases of topoi with external axiom of choice
dschepler
committed
Resolve Barr-coexact for Top and Top*
dschepler
committed
Update expected properties
dschepler
committed
Add monadically concrete -> cocomplete implication
dschepler
committed
Add implication pretopos -> balanced
dschepler
committed
Add some related properties, and a bit of background on the relevance of regularity to Barr-exactness
dschepler
committed
Add local essential smallness consequence of monadically concrete
dschepler
committed
Add not Barr-coexact data for Prost
dschepler
committed
Fix garbled language around kernel pairs in some of the proofs
dschepler
committed

Commits on Apr 19, 2026

Merge branch 'ScriptRaccoon:main' into barr-exact
dschepler
authored