CatDat

Properties

Properties from the database

• is discrete

  trivial
• is finite

  trivial
• is inhabited

  trivial

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 essentially discrete

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

  Since it is discrete, we deduce that it is locally small.
• is skeletal

  Since it is discrete, we deduce that it is skeletal.
• is thin

  Since it is essentially discrete, we deduce that it is thin.
• is a groupoid

  Since it is essentially discrete, we deduce that it is a groupoid.
• is locally essentially small

  Since it is essentially discrete, we deduce that it is locally essentially small.
• has connected limits

  Since it is essentially discrete, we deduce that it has connected limits.
• 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.
• has a generator

  Since it is thin and is inhabited, we deduce that it has a generator.
• has wide pullbacks

  Since it has connected limits, we deduce that it has wide pullbacks.
• has pullbacks

  Since it has wide pullbacks, we deduce that it has pullbacks.
• has filtered limits

  Since it has wide pullbacks, we deduce that it has filtered limits.
• is Cauchy complete

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

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

  Since it is a groupoid, we deduce that it is self-dual.
• is mono-regular

  Since it is a groupoid, we deduce that it is mono-regular.
• is well-powered

  Since it is a groupoid, we deduce that it is well-powered.
• is balanced

  Since it is mono-regular, we deduce that it is balanced.
• has connected colimits

  Since it is essentially discrete, we deduce that it has connected colimits.
• 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.
• has wide pushouts

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

  Since it has wide pushouts, we deduce that it has pushouts.
• has filtered colimits

  Since it has wide pushouts, we deduce that it has filtered colimits.
• has sequential colimits

  Since it has filtered colimits, we deduce that it has sequential colimits.
• is epi-regular

  Since it is a groupoid, we deduce that it is epi-regular.
• is well-copowered

  Since it is a groupoid, we deduce that it is well-copowered.

Non-Properties

Non-Properties from the database

• is not connected

Deduced Non-Properties*

• is not complete

  Assume for a contradiction that it is complete. Since it is complete, we deduce that it is finitely complete. Since it is finitely complete, we deduce that it has finite products. Since it has finite products, we deduce that it has a terminal object. Since it has a terminal object, we deduce that it is connected. This is a contradiction since we already know that it is not connected.
• is not cocomplete

  Assume for a contradiction that it is cocomplete. Since it is cocomplete, we deduce that it is finitely cocomplete. Since it is finitely cocomplete, we deduce that it has finite coproducts. Since it has finite coproducts, we deduce that it has an initial object. Since it has an initial object, we deduce that it is connected. This is a contradiction since we already know that it is not connected.
• is not cartesian closed

  Assume for a contradiction that it is cartesian closed. Since it is cartesian closed, we deduce that it has finite products. Since it has finite products, we deduce that it has a terminal object. Since it has a terminal object, we deduce that it is connected. This is a contradiction since we already know that it is not connected.
• does not have zero morphisms

  Assume for a contradiction that it has zero morphisms. Since it has zero morphisms and is inhabited, we deduce that it is connected. This is a contradiction since we already know that it is not connected.
• 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 finitely complete

  Assume for a contradiction that it is finitely complete. Since it is finitely complete, we deduce that it has finite products. Since it has finite products, we deduce that it has a terminal object. Since it has a terminal object, we deduce that it is connected. This is a contradiction since we already know that it is not connected.
• is not finitely cocomplete

  Assume for a contradiction that it is finitely cocomplete. Since it is finitely cocomplete, we deduce that it has finite coproducts. Since it has finite coproducts, we deduce that it has an initial object. Since it has an initial object, we deduce that it is connected. This is a contradiction since we already know that it is not connected.
• 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 locally finitely presentable

  Assume for a contradiction that it is locally finitely presentable. Since it is locally finitely presentable, we deduce that it has exact filtered colimits. Since it has exact filtered colimits, we deduce that it is finitely complete. This is a contradiction since we already know that it is not finitely complete.
• is not locally presentable

  Assume for a contradiction that it is locally presentable. Since it is locally presentable, we deduce that it is complete. This is a contradiction since we already know that it is not complete.
• is not locally ℵ₁-presentable

  Assume for a contradiction that it is locally ℵ₁-presentable. Since it is locally ℵ₁-presentable, we deduce that it is locally presentable. This is a contradiction since we already know that it is not locally presentable.
• 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 is cartesian closed. This is a contradiction since we already know that it is not cartesian closed.
• 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.
• does not have an initial object

  Assume for a contradiction that it has an initial object. Since it has an initial object, we deduce that it is connected. This is a contradiction since we already know that it is not connected.
• does not have a terminal object

  Assume for a contradiction that it has a terminal object. Since it has a terminal object, we deduce that it is connected. This is a contradiction since we already know that it is not connected.
• does not have products

  Assume for a contradiction that it has products. Since it has products and has equalizers, we deduce that it is complete. This is a contradiction since we already know that it is not complete.
• does not have coproducts

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

  Assume for a contradiction that it has finite products. Since it has finite products and has equalizers, we deduce that it is finitely complete. This is a contradiction since we already know that it is not finitely complete.
• does not have finite coproducts

  Assume for a contradiction that it has finite coproducts. Since it has finite coproducts and has coequalizers, we deduce that it is finitely cocomplete. This is a contradiction since we already know that it is not finitely cocomplete.
• does not have binary products

  Assume for a contradiction that it has binary products. Since it has binary products and is inhabited, we deduce that it is connected. This is a contradiction since we already know that it is not connected.
• does not have binary coproducts

  Assume for a contradiction that it has binary coproducts. Since it has binary coproducts and is inhabited, we deduce that it is connected. This is a contradiction since we already know that it is not connected.
• does not have countable products

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

  Assume for a contradiction that it has countable coproducts. Since it has countable coproducts, we deduce that it has finite coproducts. This is a contradiction since we already know that it does not have finite coproducts.
• does not have a strict initial object

  Assume for a contradiction that it has a strict initial object. Since it has a strict initial object, we deduce that it has an initial object. This is a contradiction since we already know that it does not have an initial object.
• does not have a strict terminal object

  Assume for a contradiction that it has a strict terminal object. Since it has a strict terminal object, we deduce that it has a terminal object. This is a contradiction since we already know that it does not have a terminal object.
• is not finitary algebraic

  Assume for a contradiction that it is finitary algebraic. Since it is finitary algebraic, we deduce that it is locally finitely presentable. This is a contradiction since we already know that it is not locally finitely presentable.
• is not trivial

  Assume for a contradiction that it is trivial. Since it is trivial, we deduce that it is finitary algebraic. This is a contradiction since we already know that it is not finitary algebraic.
• does not have a subobject classifier

  Assume for a contradiction that it has a subobject classifier. Since it has a subobject classifier, we deduce that it is finitely complete. This is a contradiction since we already know that it is not finitely complete.
• is not infinitary distributive

  Assume for a contradiction that it is infinitary distributive. Since it is infinitary distributive, we deduce that it has finite products. This is a contradiction since we already know that it does not have finite products.
• is not distributive

  Assume for a contradiction that it is distributive. Since it is distributive, we deduce that it has finite products. This is a contradiction since we already know that it does not have finite products.
• does not have exact filtered colimits

  Assume for a contradiction that it has exact filtered colimits. Since it has exact filtered colimits, we deduce that it is finitely complete. This is a contradiction since we already know that it is not finitely complete.
• 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, we deduce that it has finite coproducts. This is a contradiction since we already know that it does not have finite coproducts.
• does not have disjoint coproducts

  Assume for a contradiction that it has disjoint coproducts. Since it has disjoint coproducts, we deduce that it has coproducts. This is a contradiction since we already know that it does not have 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 Malcev

  Assume for a contradiction that it is Malcev. Since it is Malcev, we deduce that it is finitely complete. This is a contradiction since we already know that it is not finitely complete.

*This also uses the deduced properties.