Library UniMath.CategoryTheory.Categories.HSET.Core
Category of hSets
Contents:
- Category HSET of hSets (hset_category)
- Some particular HSETs
- Hom functors
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.MoreFoundations.PartA.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Local Open Scope cat.
Category HSET of hSets (hset_category)
Section HSET_precategory.
Definition hset_precategory_ob_mor : precategory_ob_mor :=
make_precategory_ob_mor
hSet
(λ A B : hSet, A -> B).
Definition hset_precategory_data : precategory_data :=
make_precategory_data 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.
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.
Definition hset_category : category := (HSET ,, has_homsets_HSET).
End HSET_precategory.
Notation "'HSET'" := hset_category : cat.
Notation "'SET'" := hset_category : cat.
Definition hset_precategory_ob_mor : precategory_ob_mor :=
make_precategory_ob_mor
hSet
(λ A B : hSet, A -> B).
Definition hset_precategory_data : precategory_data :=
make_precategory_data 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.
Definition hset_category : category := (HSET ,, has_homsets_HSET).
End HSET_precategory.
Notation "'HSET'" := hset_category : cat.
Notation "'SET'" := hset_category : cat.
Definition emptyHSET : HSET.
Show proof.
Definition unitHSET : HSET.
Show proof.
Definition natHSET : HSET.
Show proof.
Section HomSetFunctors.
Context {C : category}.
Definition homSet_functor_data :
functor_data (category_binproduct (C^op) C) hset_category.
Show proof.
use make_functor_data.
+ intros pair.
induction pair as (p1, p2).
use make_hSet.
- exact (C ⟦ p1, p2 ⟧).
- use (homset_property C).
+ intros x y fg h.
induction fg as (fg1, fg2).
cbn in fg1.
exact (fg1 · h · fg2).
+ intros pair.
induction pair as (p1, p2).
use make_hSet.
- exact (C ⟦ p1, p2 ⟧).
- use (homset_property C).
+ intros x y fg h.
induction fg as (fg1, fg2).
cbn in fg1.
exact (fg1 · h · fg2).
Lemma is_functor_homSet_functor_type : is_functor homSet_functor_data.
Show proof.
use make_dirprod.
- intro; cbn.
apply funextsec; intro.
refine (id_right _ @ _).
apply id_left.
- repeat intro.
apply funextsec; intro; cbn.
do 3 rewrite assoc.
reflexivity.
- intro; cbn.
apply funextsec; intro.
refine (id_right _ @ _).
apply id_left.
- repeat intro.
apply funextsec; intro; cbn.
do 3 rewrite assoc.
reflexivity.
Definition homSet_functor : functor (category_binproduct (C^op) C) hset_category :=
make_functor _ is_functor_homSet_functor_type.
Context (c : C).
Definition cov_homSet_functor : functor C hset_category :=
functor_fix_fst_arg (C^op) _ _ homSet_functor c.
Definition contra_homSet_functor : functor (C^op) hset_category :=
functor_fix_snd_arg (C^op) _ _ homSet_functor c.
End HomSetFunctors.