Repository navigation

Add the effective topos - #362

Open

dschepler wants to merge 9 commits into

ScriptRaccoon:mainfrom

dschepler:effective-topos

Open

Add the effective topos#362
dschepler wants to merge 9 commits into
ScriptRaccoon:mainfrom
dschepler:effective-topos

Commits on Sep 8, 2026
- Add the effective topos
  dschepler
  committed
  bd3f36d
- Add several instances of topos has limits of a certain shape implies it has colimits of the opposite shape, in order to resolve a property of Eff
  dschepler
  committed
  48c7a0a
Commits on Sep 9, 2026
- Add reference for proof Eff is a topos; also expand description of isomorphisms, inspired by a discussion in that reference
  dschepler
  committed
  2b59fc2
- Small fix to natural numbers object proof
  dschepler
  committed
  d4d8dd1
Commits on Sep 10, 2026
- Add proof that Eff has an extremal generating set
  dschepler
  committed
  a098b4b
- Simplify: I forgot that generating sets in a balanced category are automatically extremal
  dschepler
  committed
  8ff10c9
Commits on Sep 12, 2026