Power objects turn coreflexive equalizers into coequalizers
ID: power-objects-turn-coreflexive-equalizers-into-coequalizers
For a coreflexive pair with equalizer , direct image along the mono satisfies and . Thus any map equalizing obeys . Since , the map is their coequalizer. These identities hold for parameterized subobjects in any elementary topos.
New to topics? Read the docs here!