Skip to content

Pullbacks imply coreflexive equalizers - #368

Merged
ScriptRaccoon merged 1 commit into
mainfrom
pullbacks-imply-coreflexive-equalizers
Sep 11, 2026
Merged

Pullbacks imply coreflexive equalizers#368
ScriptRaccoon merged 1 commit into
mainfrom
pullbacks-imply-coreflexive-equalizers

Conversation

@ScriptRaccoon

Copy link
Copy Markdown
Owner

Any category with pullbacks has coreflexive equalizers. Dually, any category with pushouts has reflexive coequalizers. This result was missing and has now been added. Unfortunately, no property assignments have become redundant after adding this. But: the number of consistent combinations without witnesses has decreased from 481 to 467, which contributes to this milestone. This is because the following 14 combinations have become inconsistent, so that they do not require any witnesses anymore.

locally cartesian closed ∧ ¬coquotients of cocongruences
locally cartesian closed ∧ ¬coreflexive equalizers
locally cocartesian coclosed ∧ ¬quotients of congruences
locally cocartesian coclosed ∧ ¬reflexive coequalizers
locally poly-presentable ∧ ¬coquotients of cocongruences
locally poly-presentable ∧ ¬coreflexive equalizers
pullbacks ∧ ¬coquotients of cocongruences
pullbacks ∧ ¬coreflexive equalizers
pushouts ∧ ¬quotients of congruences
pushouts ∧ ¬reflexive coequalizers
wide pullbacks ∧ ¬coquotients of cocongruences
wide pullbacks ∧ ¬coreflexive equalizers
wide pushouts ∧ ¬quotients of congruences
wide pushouts ∧ ¬reflexive coequalizers

@ScriptRaccoon
ScriptRaccoon merged commit 0a57a8f into main Sep 11, 2026
1 check passed
@ScriptRaccoon
ScriptRaccoon deleted the pullbacks-imply-coreflexive-equalizers branch September 11, 2026 19:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant