# Library UniMath.CategoryTheory.categories.FinSet

# The category of finite sets

## Contents:

- The univalent category FinSet of finite sets/types
- (Co)limits
- Colimits
- Binary coproducts

- Limits
- Binary products

- Colimits

Require Import UniMath.Foundations.PartD.

Require Import UniMath.Combinatorics.FiniteSets.

Require Import UniMath.CategoryTheory.Core.Categories.

Require Import UniMath.CategoryTheory.Core.Univalence.

Require Import UniMath.CategoryTheory.Core.Functors.

Require Import UniMath.CategoryTheory.categories.HSET.Core.

Require Import UniMath.CategoryTheory.categories.HSET.Limits.

Require Import UniMath.CategoryTheory.categories.HSET.Colimits.

Require Import UniMath.CategoryTheory.categories.HSET.Univalence.

Require Import UniMath.CategoryTheory.Subcategory.Core.

Require Import UniMath.CategoryTheory.Subcategory.Full.

Require Import UniMath.CategoryTheory.Subcategory.Limits.

Require Import UniMath.CategoryTheory.limits.binproducts.

Require Import UniMath.CategoryTheory.limits.bincoproducts.

Local Open Scope cat.

Local Open Scope functions.

## The univalent category FinSet of finite sets/types

Definition finite_subtype : hsubtype (ob HSET) := isfinite ∘ pr1hSet.

Definition FinSet : univalent_category :=

subcategory_univalent HSET_univalent_category finite_subtype.

Definition FinSet : univalent_category :=

subcategory_univalent HSET_univalent_category finite_subtype.

## (Co)limits

### Colimits

#### Binary coproducts

Definition BinCoproductsFinSet : BinCoproducts FinSet.

Proof.

apply (@bin_coproducts_in_full_subcategory HSET_univalent_category

finite_subtype BinCoproductsHSET).

intros; apply isfinitecoprod; assumption.

Defined.

Proof.

apply (@bin_coproducts_in_full_subcategory HSET_univalent_category

finite_subtype BinCoproductsHSET).

intros; apply isfinitecoprod; assumption.

Defined.

### Limits

#### Binary products

Definition BinProductsFinSet : BinProducts FinSet.

Proof.

apply (@bin_products_in_full_subcategory HSET_univalent_category

finite_subtype BinProductsHSET).

intros; apply isfinitedirprod; assumption.

Defined.

Proof.

apply (@bin_products_in_full_subcategory HSET_univalent_category

finite_subtype BinProductsHSET).

intros; apply isfinitedirprod; assumption.

Defined.