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.