CatDat

Properties

Properties from the database

• is finitary algebraic
• is self-dual
• is finite
• is cartesian closed
• is skeletal

  The two objects are not isomorphic

Deduced properties

• is small

  Since it is finite, we deduce that it is small.
• is essentially finite

  Since it is finite, we deduce that it is essentially finite.
• is essentially small

  Since it is essentially finite, we deduce that it is essentially small.
• is locally finitely presentable

  Since it is finitary algebraic, we deduce that it is locally finitely presentable.
• has finite products

  Since it is cartesian closed, we deduce that it has finite products.
• has finite coproducts

  Since it is self-dual and has finite products, we deduce that it has finite coproducts.
• is locally small

  Since it is small, we deduce that it is locally small.
• is well-powered

  Since it is essentially small, we deduce that it is well-powered.
• is well-copowered

  Since it is essentially small, we deduce that it is well-copowered.
• is locally essentially small

  Since it is essentially small, we deduce that it is locally essentially small.
• is thin

  Since it is essentially finite and has finite products, we deduce that it is thin.
• has equalizers

  Since it is thin, we deduce that it has equalizers.
• is left cancellative

  Since it is thin, we deduce that it is left cancellative.
• is finitely complete

  Since it has finite products and has equalizers, we deduce that it is finitely complete.
• has a terminal object

  Since it has finite products, we deduce that it has a terminal object.
• has binary products

  Since it has finite products, we deduce that it has binary products.
• has pullbacks

  Since it has binary products and has equalizers, we deduce that it has pullbacks.
• is connected

  Since it has a terminal object, we deduce that it is connected.
• is Cauchy complete

  Since it has equalizers, we deduce that it is Cauchy complete.
• is distributive

  Since it is cartesian closed and has finite coproducts, we deduce that it is distributive.
• is locally presentable

  Since it is locally finitely presentable, we deduce that it is locally presentable.
• has exact filtered colimits

  Since it is locally finitely presentable, we deduce that it has exact filtered colimits.
• is locally ℵ₁-presentable

  Since it is locally finitely presentable, we deduce that it is locally ℵ₁-presentable.
• is inhabited

  Since it is connected, we deduce that it is inhabited.
• is Malcev

  Since it is thin and is finitely complete, we deduce that it is Malcev.
• has coequalizers

  Since it is thin, we deduce that it has coequalizers.
• is right cancellative

  Since it is thin, we deduce that it is right cancellative.
• has a cogenerator

  Since it is thin and is inhabited, we deduce that it has a cogenerator.
• is finitely cocomplete

  Since it has finite coproducts and has coequalizers, we deduce that it is finitely cocomplete.
• has an initial object

  Since it has finite coproducts, we deduce that it has an initial object.
• has binary coproducts

  Since it has finite coproducts, we deduce that it has binary coproducts.
• has pushouts

  Since it has binary coproducts and has coequalizers, we deduce that it has pushouts.
• has a strict terminal object

  Since it is right cancellative and has a terminal object, we deduce that it has a strict terminal object.
• has a strict initial object

  Since it is self-dual and has a strict terminal object, we deduce that it has a strict initial object.
• has a generator

  Since it is self-dual and has a cogenerator, we deduce that it has a generator.
• has filtered colimits

  Since it has exact filtered colimits, we deduce that it has filtered colimits.
• is complete

  Since it is locally presentable, we deduce that it is complete.
• is cocomplete

  Since it is locally presentable, we deduce that it is cocomplete.
• has wide pushouts

  Since it is cocomplete, we deduce that it has wide pushouts.
• has connected colimits

  Since it is cocomplete, we deduce that it has connected colimits.
• has coproducts

  Since it is cocomplete, we deduce that it has coproducts.
• has countable coproducts

  Since it has coproducts, we deduce that it has countable coproducts.
• has sequential colimits

  Since it has coequalizers and has countable coproducts, we deduce that it has sequential colimits.
• has products

  Since it is self-dual and has coproducts, we deduce that it has products.
• has countable products

  Since it is self-dual and has countable coproducts, we deduce that it has countable products.
• has filtered limits

  Since it is self-dual and has filtered colimits, we deduce that it has filtered limits.
• has sequential limits

  Since it is self-dual and has sequential colimits, we deduce that it has sequential limits.
• has connected limits

  Since it is self-dual and has connected colimits, we deduce that it has connected limits.
• has wide pullbacks

  Since it is self-dual and has wide pushouts, we deduce that it has wide pullbacks.
• is infinitary distributive

  Since it is cartesian closed and has coproducts, we deduce that it is infinitary distributive.

Non-Properties

Non-Properties from the database

• does not have a subobject classifier

Deduced Non-Properties*

• does not have zero morphisms

  Assume for a contradiction that it has zero morphisms. Since it has zero morphisms and has an initial object, we deduce that it is pointed. Since it is pointed and is cartesian closed, we deduce that it is trivial. Since it is trivial, we deduce that it is a Grothendieck topos. Since it is a Grothendieck topos, we deduce that it is an elementary topos. Since it is an elementary topos, we deduce that it has a subobject classifier. This is a contradiction since we already know that it does not have a subobject classifier.
• is not preadditive

  Assume for a contradiction that it is preadditive. Since it is preadditive, we deduce that it has zero morphisms. This is a contradiction since we already know that it does not have zero morphisms.
• is not additive

  Assume for a contradiction that it is additive. Since it is additive, we deduce that it is preadditive. This is a contradiction since we already know that it is not preadditive.
• is not abelian

  Assume for a contradiction that it is abelian. Since it is abelian, we deduce that it is additive. This is a contradiction since we already know that it is not additive.
• is not pointed

  Assume for a contradiction that it is pointed. Since it is pointed, we deduce that it has zero morphisms. This is a contradiction since we already know that it does not have zero morphisms.
• is not an elementary topos

  Assume for a contradiction that it is an elementary topos. Since it is an elementary topos, we deduce that it has a subobject classifier. This is a contradiction since we already know that it does not have a subobject classifier.
• is not a Grothendieck topos

  Assume for a contradiction that it is a Grothendieck topos. Since it is a Grothendieck topos, we deduce that it is an elementary topos. This is a contradiction since we already know that it is not an elementary topos.
• is not a groupoid

  Assume for a contradiction that it is a groupoid. Since it is thin and is a groupoid, we deduce that it is essentially discrete. Since it is essentially discrete and is connected, we deduce that it is trivial. Since it is trivial, we deduce that it is a Grothendieck topos. This is a contradiction since we already know that it is not a Grothendieck topos.
• is not discrete

  Assume for a contradiction that it is discrete. Since it is discrete, we deduce that it is essentially discrete. Since it is essentially discrete, we deduce that it is a groupoid. This is a contradiction since we already know that it is not a groupoid.
• is not essentially discrete

  Assume for a contradiction that it is essentially discrete. Since it is essentially discrete, we deduce that it is a groupoid. This is a contradiction since we already know that it is not a groupoid.
• is not trivial

  Assume for a contradiction that it is trivial. Since it is trivial, we deduce that it is a Grothendieck topos. This is a contradiction since we already know that it is not a Grothendieck topos.
• is not balanced

  Assume for a contradiction that it is balanced. Since it is left cancellative and is right cancellative and is balanced, we deduce that it is a groupoid. This is a contradiction since we already know that it is not a groupoid.
• is not Grothendieck abelian

  Assume for a contradiction that it is Grothendieck abelian. Since it is Grothendieck abelian, we deduce that it is abelian. This is a contradiction since we already know that it is not abelian.
• does not have disjoint finite coproducts

  Assume for a contradiction that it has disjoint finite coproducts. Since it has disjoint finite coproducts and is thin, we deduce that it is trivial. This is a contradiction since we already know that it is not trivial.
• does not have disjoint coproducts

  Assume for a contradiction that it has disjoint coproducts. Since it has disjoint coproducts, we deduce that it has disjoint finite coproducts. This is a contradiction since we already know that it does not have disjoint finite coproducts.
• is not split abelian

  Assume for a contradiction that it is split abelian. Since it is split abelian, we deduce that it is abelian. This is a contradiction since we already know that it is not abelian.
• is not mono-regular

  Assume for a contradiction that it is mono-regular. Since it is mono-regular, we deduce that it is balanced. This is a contradiction since we already know that it is not balanced.
• is not epi-regular

  Assume for a contradiction that it is epi-regular. Since it is epi-regular, we deduce that it is balanced. This is a contradiction since we already know that it is not balanced.

*This also uses the deduced properties.