(Co)limits in the category of finite types

We show that finite (co)limits exist in FintypeCat and that they are preserved by the natural inclusion FintypeCat.incl.

instance CategoryTheory.Limits.FintypeCat.instFiniteObjToQuiverToCategoryStructTypeToQuiverToCategoryStructTypesToPrefunctorCompFintypeCatInstCategoryFintypeCatIncl {J : Type} [CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J FintypeCat) (j : J) : Finite ((CategoryTheory.Functor.comp K FintypeCat.incl).obj j)

Equations

• (_ : Finite ((CategoryTheory.Functor.comp K FintypeCat.incl).obj j)) = (_ : Finite ((CategoryTheory.Functor.comp K FintypeCat.incl).obj j))

noncomputable instance CategoryTheory.Limits.FintypeCat.finiteLimitOfFiniteDiagram {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J (Type u_1)) [∀ (j : J), Finite (K.obj j)] : Fintype (CategoryTheory.Limits.limit K)

Any functor from a finite category to Types that only involves finite objects, has a finite limit.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteLimits {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.CreatesLimitsOfShape J FintypeCat.incl

Equations

• CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteLimits = CategoryTheory.CreatesLimitsOfShape.mk

instance CategoryTheory.Limits.FintypeCat.instHasLimitsOfShapeFintypeCatInstCategoryFintypeCat {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.Limits.HasLimitsOfShape J FintypeCat

Equations

• (_ : CategoryTheory.Limits.HasLimitsOfShape J FintypeCat) = (_ : CategoryTheory.Limits.HasLimitsOfShape J FintypeCat)

instance CategoryTheory.Limits.FintypeCat.hasFiniteLimits : CategoryTheory.Limits.HasFiniteLimits FintypeCat

Equations

• CategoryTheory.Limits.FintypeCat.hasFiniteLimits = (_ : CategoryTheory.Limits.HasFiniteLimits FintypeCat)

noncomputable instance CategoryTheory.Limits.FintypeCat.inclusionPreservesFiniteLimits : CategoryTheory.Limits.PreservesFiniteLimits FintypeCat.incl

Equations

• CategoryTheory.Limits.FintypeCat.inclusionPreservesFiniteLimits = CategoryTheory.Limits.PreservesFiniteLimits.mk

noncomputable instance CategoryTheory.Limits.FintypeCat.finiteColimitOfFiniteDiagram {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J (Type u_1)) [∀ (j : J), Finite (K.obj j)] : Fintype (CategoryTheory.Limits.colimit K)

Any functor from a finite category to Types that only involves finite objects, has a finite colimit.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteColimits {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.CreatesColimitsOfShape J FintypeCat.incl

Equations

• CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteColimits = CategoryTheory.CreatesColimitsOfShape.mk

instance CategoryTheory.Limits.FintypeCat.instHasColimitsOfShapeFintypeCatInstCategoryFintypeCat {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.Limits.HasColimitsOfShape J FintypeCat

Equations

• (_ : CategoryTheory.Limits.HasColimitsOfShape J FintypeCat) = (_ : CategoryTheory.Limits.HasColimitsOfShape J FintypeCat)

instance CategoryTheory.Limits.FintypeCat.hasFiniteColimits : CategoryTheory.Limits.HasFiniteColimits FintypeCat

Equations

• CategoryTheory.Limits.FintypeCat.hasFiniteColimits = (_ : CategoryTheory.Limits.HasFiniteColimits FintypeCat)

noncomputable instance CategoryTheory.Limits.FintypeCat.inclusionPreservesFiniteColimits : CategoryTheory.Limits.PreservesFiniteColimits FintypeCat.incl

Equations

• CategoryTheory.Limits.FintypeCat.inclusionPreservesFiniteColimits = CategoryTheory.Limits.PreservesFiniteColimits.mk