Skip to content

¬lextensive not deduced from ¬extensive for Set^op #64

@diracdeltafunk

Description

@diracdeltafunk

The entry for Set^op says that Set^op is not extensive. It also says that it cannot tell whether or not Set^op is lextensive. However, CatDat is supposed to know that lextensive is equivalent to extensive + finitely complete! (see https://catdat.app/category-property/lextensive)

So it should deduce that Set^op is not lextensive... unless I'm missing something, of course.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions