Library UniMath.CategoryTheory.categories.HSET.Core

Category of hSets

Started by: Benedikt Ahrens, Chris Kapulkin, Mike Shulman
January 2013
Extended by: Anders Mörtberg (October 2015)

Contents:

  • Category HSET of hSets (hset_category)
  • Some particular HSETs

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.Foundations.UnivalenceAxiom.
Require Import UniMath.Foundations.NaturalNumbers.
Require Import UniMath.Foundations.HLevels.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.

Local Open Scope cat.

Category HSET of hSets (hset_category)

Section HSET_precategory.

Definition hset_fun_space (A B : hSet) : hSet :=
  hSetpair _ (isaset_set_fun_space A B).

Definition hset_precategory_ob_mor : precategory_ob_mor :=
  tpair (λ ob : UU, ob -> ob -> UU) hSet
        (λ A B : hSet, hset_fun_space A B).

Definition hset_precategory_data : precategory_data :=
  precategory_data_pair hset_precategory_ob_mor (fun (A:hSet) (x : A) => x)
     (fun (A B C : hSet) (f : A -> B) (g : B -> C) (x : A) => g (f x)).

Lemma is_precategory_hset_precategory_data :
  is_precategory hset_precategory_data.
Show proof.
repeat split.

Definition hset_precategory : precategory :=
  tpair _ _ is_precategory_hset_precategory_data.

Local Notation "'HSET'" := hset_precategory : cat.

Lemma has_homsets_HSET : has_homsets HSET.
Show proof.
intros a b; apply isaset_set_fun_space.


Definition hset_category : category := (HSET ,, has_homsets_HSET).

End HSET_precategory.

Notation "'HSET'" := hset_precategory : cat.
Notation "'SET'" := hset_category : cat.

Some particular HSETs


Definition emptyHSET : HSET.
Show proof.
  exists empty.
  abstract (apply isasetempty).

Definition unitHSET : HSET.
Show proof.
  exists unit.
  abstract (apply isasetunit).

Definition natHSET : HSET.
Show proof.
  exists nat.
  abstract (apply isasetnat).