Library UniMath.CategoryTheory.Categories.StandardCategories
Standard categories
Contents:
- The path groupoid (path_groupoid)
- Discrete categories
- Characterization of discrete categories
- The discrete univalent_category on n objects (cat_n)
- The category with one object (unit_category)
- The category with no objects (empty_category)
- The directed interval
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.PartA.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Setcategories.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Groupoids.
Require Import UniMath.CategoryTheory.Limits.Initial.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.exponentials.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.catiso.
Local Open Scope cat.
Definition compose' { C:precategory_data } { a b c:ob C }
(g:b --> c) (f:a --> b) : a --> c.
Show proof.
The path/fundamental groupoid of a type
Definition path_pregroupoid (X:UU) (iobj : isofhlevel 3 X) : pregroupoid.
use make_pregroupoid.
- use tpair.
{
use make_precategory_one_assoc; use tpair.
+ exact (X,, λ x y, x = y).
+ use make_dirprod.
* exact (λ _, idpath _).
* intros a b c; exact pathscomp0.
+ use make_dirprod.
* reflexivity.
* intros; apply pathscomp0rid.
+ intros ? ? ? ? ? ?; apply path_assoc.
}
intros ? ? ? ? ? ?.
apply iobj.
- intros x y path.
exists (!path).
split.
+ apply pathsinv0r.
+ apply pathsinv0l.
Defined.
use make_pregroupoid.
- use tpair.
{
use make_precategory_one_assoc; use tpair.
+ exact (X,, λ x y, x = y).
+ use make_dirprod.
* exact (λ _, idpath _).
* intros a b c; exact pathscomp0.
+ use make_dirprod.
* reflexivity.
* intros; apply pathscomp0rid.
+ intros ? ? ? ? ? ?; apply path_assoc.
}
intros ? ? ? ? ? ?.
apply iobj.
- intros x y path.
exists (!path).
split.
+ apply pathsinv0r.
+ apply pathsinv0l.
Defined.
If X isofhlevel 3, then in particular, its path types are sets
Definition has_homsets_path_pregroupoid {X : UU} (iobj : isofhlevel 3 X) :
has_homsets (path_pregroupoid X iobj).
Show proof.
Definition path_groupoid (X : UU) (iobj : isofhlevel 3 X) : groupoid.
Show proof.
has_homsets (path_pregroupoid X iobj).
Show proof.
Definition path_groupoid (X : UU) (iobj : isofhlevel 3 X) : groupoid.
Show proof.
use make_groupoid.
- use make_category.
+ exact (path_pregroupoid X iobj).
+ apply (has_homsets_path_pregroupoid); assumption.
- apply (pregroupoid_is_pregroupoid (path_pregroupoid X iobj)).
- use make_category.
+ exact (path_pregroupoid X iobj).
+ apply (has_homsets_path_pregroupoid); assumption.
- apply (pregroupoid_is_pregroupoid (path_pregroupoid X iobj)).
In this case, the path pregroupoid is further univalent.
Lemma is_univalent_path_pregroupoid (X : UU) (iobj : isofhlevel 3 X) :
is_univalent_pregroupoid (path_pregroupoid X iobj).
Show proof.
Lemma is_univalent_path_groupoid (X:UU) (i : isofhlevel 3 X) :
is_univalent (path_groupoid X i).
Show proof.
Definition path_univalent_groupoid
{X : UU}
(i3 : isofhlevel 3 X)
: univalent_groupoid.
Show proof.
Definition path_groupoid_hset (X : hSet) : univalent_groupoid :=
(path_univalent_groupoid (isofhlevelssnset 1 _ (setproperty X))).
is_univalent_pregroupoid (path_pregroupoid X iobj).
Show proof.
split.
- intros a b.
assert (k : idfun (a = b) ~ idtomor a b).
{ intro p; destruct p; reflexivity. }
apply (isweqhomot _ _ k). apply idisweq.
- apply has_homsets_path_pregroupoid; assumption.
- intros a b.
assert (k : idfun (a = b) ~ idtomor a b).
{ intro p; destruct p; reflexivity. }
apply (isweqhomot _ _ k). apply idisweq.
- apply has_homsets_path_pregroupoid; assumption.
Lemma is_univalent_path_groupoid (X:UU) (i : isofhlevel 3 X) :
is_univalent (path_groupoid X i).
Show proof.
Definition path_univalent_groupoid
{X : UU}
(i3 : isofhlevel 3 X)
: univalent_groupoid.
Show proof.
use make_univalent_groupoid.
- exact (make_univalent_category _ (is_univalent_path_groupoid X i3)).
- apply (groupoid_is_pregroupoid _).
- exact (make_univalent_category _ (is_univalent_path_groupoid X i3)).
- apply (groupoid_is_pregroupoid _).
Definition path_groupoid_hset (X : hSet) : univalent_groupoid :=
(path_univalent_groupoid (isofhlevelssnset 1 _ (setproperty X))).
When X is a set, its path pregroupoid is the discrete category on its elements.
Definition path_groupoid_hset_is_discrete (X : hSet) :
is_discrete (path_groupoid_hset X).
Show proof.
Definition discrete_category_hset (X : hSet) : discrete_category :=
make_discrete_category (path_groupoid_hset X) (path_groupoid_hset_is_discrete X).
is_discrete (path_groupoid_hset X).
Show proof.
split; split.
- apply setproperty.
- apply homset_property.
- apply pregroupoid_is_pregroupoid.
- apply univalent_category_is_univalent.
- apply setproperty.
- apply homset_property.
- apply pregroupoid_is_pregroupoid.
- apply univalent_category_is_univalent.
Definition discrete_category_hset (X : hSet) : discrete_category :=
make_discrete_category (path_groupoid_hset X) (path_groupoid_hset_is_discrete X).
To define a functor out of a path pregroupoid, it suffices to give
its values on objects. Compare to functor_discrete_categories.
Lemma functor_path_pregroupoid
{X : UU} {D : category} (i : isofhlevel 3 X) (f : X → ob D) :
functor (path_pregroupoid X i) D.
Show proof.
{X : UU} {D : category} (i : isofhlevel 3 X) (f : X → ob D) :
functor (path_pregroupoid X i) D.
Show proof.
use make_functor.
- use make_functor_data.
+ apply f.
+ intros a b aeqb.
exact (transportf (λ z, D ⟦ f a, z ⟧) (maponpaths f aeqb) (identity _)).
- split.
+ intro; reflexivity.
+ intros a b c g h; cbn.
refine (maponpaths (λ p, transportf _ p _) (maponpathscomp0 _ _ _) @ _).
refine (!transport_f_f _ (maponpaths f g) (maponpaths f h) _ @ _).
abstract (induction h; cbn; apply pathsinv0; apply id_right).
- use make_functor_data.
+ apply f.
+ intros a b aeqb.
exact (transportf (λ z, D ⟦ f a, z ⟧) (maponpaths f aeqb) (identity _)).
- split.
+ intro; reflexivity.
+ intros a b c g h; cbn.
refine (maponpaths (λ p, transportf _ p _) (maponpathscomp0 _ _ _) @ _).
refine (!transport_f_f _ (maponpaths f g) (maponpaths f h) _ @ _).
abstract (induction h; cbn; apply pathsinv0; apply id_right).
A natural transformation of functors out of a path groupoid is given by any
family of morphisms
Definition is_nat_trans_discrete_precategory
{X : UU} {i : isofhlevel 3 X} {D : category}
{f g : functor_category (path_pregroupoid X i) D}
(F : ∏ x : X, (pr1 f) x --> (pr1 g) x)
: is_nat_trans (pr1 f) (pr1 g) F.
Show proof.
Definition nat_trans_functor_path_pregroupoid
{X : UU} {i : isofhlevel 3 X} {D : category} {F G : functor (path_pregroupoid X i) D}
(ϕ : ∏ x : X, F x --> G x) : nat_trans F G.
Show proof.
{X : UU} {i : isofhlevel 3 X} {D : category}
{f g : functor_category (path_pregroupoid X i) D}
(F : ∏ x : X, (pr1 f) x --> (pr1 g) x)
: is_nat_trans (pr1 f) (pr1 g) F.
Show proof.
intros x y h; cbn in h.
induction h.
change (idpath x) with (identity x).
assert (k := ! functor_id f x).
unfold functor_data_from_functor in k.
induction k.
assert (k := ! functor_id g x).
unfold functor_data_from_functor in k.
induction k.
intermediate_path (F x).
- apply id_left.
- apply pathsinv0. apply id_right.
induction h.
change (idpath x) with (identity x).
assert (k := ! functor_id f x).
unfold functor_data_from_functor in k.
induction k.
assert (k := ! functor_id g x).
unfold functor_data_from_functor in k.
induction k.
intermediate_path (F x).
- apply id_left.
- apply pathsinv0. apply id_right.
Definition nat_trans_functor_path_pregroupoid
{X : UU} {i : isofhlevel 3 X} {D : category} {F G : functor (path_pregroupoid X i) D}
(ϕ : ∏ x : X, F x --> G x) : nat_trans F G.
Show proof.
Characterization of discrete categories
Lemma discrete_category_iso_path_groupoid (C : discrete_category) :
catiso C (discrete_category_hset
(setcategory_objects_set (_,, discrete_category_is_setcategory C))).
Show proof.
use tpair.
- use make_functor.
+ use make_functor_data.
* exact (idfun _).
* intros a b f.
apply isotoid.
-- apply univalent_category_is_univalent.
-- exact (@pregroupoid_hom_weq_iso C _ _ f).
+ use make_dirprod.
* intro; apply setproperty.
* intros ? ? ? ? ?; apply setproperty.
- use make_dirprod.
+ intros a b.
use isweq_iso.
* intros f.
apply idtoiso.
assumption.
* intro; apply discrete_category_hom_prop.
* intro; apply setproperty.
+ apply idisweq.
- use make_functor.
+ use make_functor_data.
* exact (idfun _).
* intros a b f.
apply isotoid.
-- apply univalent_category_is_univalent.
-- exact (@pregroupoid_hom_weq_iso C _ _ f).
+ use make_dirprod.
* intro; apply setproperty.
* intros ? ? ? ? ?; apply setproperty.
- use make_dirprod.
+ intros a b.
use isweq_iso.
* intros f.
apply idtoiso.
assumption.
* intro; apply discrete_category_hom_prop.
* intro; apply setproperty.
+ apply idisweq.
The discrete univalent_category on n objects (cat_n)
Require Import UniMath.Combinatorics.StandardFiniteSets.
Definition cat_n (n:nat): univalent_groupoid.
apply path_groupoid_hset; use make_hSet.
- exact (stn n).
- apply isasetstn.
Defined.
Lemma is_discrete_cat_n (n : nat) : is_discrete (cat_n n).
Show proof.
The category with one object (unit_category)
Definition unit_category : univalent_category.
Show proof.
Section FunctorToUnit.
Context (A : precategory).
Definition functor_to_unit_data : functor_data A unit_category.
Show proof.
Definition is_functor_to_unit : is_functor functor_to_unit_data.
Show proof.
Definition functor_to_unit : functor A _ := make_functor _ is_functor_to_unit.
Lemma iscontr_functor_to_unit : iscontr (functor A unit_category).
Show proof.
use make_iscontr.
- exact functor_to_unit.
- intro F.
apply functor_eq.
+ apply (homset_property unit_category).
+ use total2_paths_f.
* apply funextsec. intro. cbn.
apply proofirrelevance.
apply isapropunit.
* do 3 (apply funextsec; intro).
apply proofirrelevance.
simpl.
apply hlevelntosn.
apply isapropunit.
End FunctorToUnit.- exact functor_to_unit.
- intro F.
apply functor_eq.
+ apply (homset_property unit_category).
+ use total2_paths_f.
* apply funextsec. intro. cbn.
apply proofirrelevance.
apply isapropunit.
* do 3 (apply funextsec; intro).
apply proofirrelevance.
simpl.
apply hlevelntosn.
apply isapropunit.
Functors from the unit category
Definition functor_from_unit_data
{C : category}
(x : C)
: functor_data unit_category C.
Show proof.
Definition functor_from_unit_is_functor
{C : category}
(x : C)
: is_functor (functor_from_unit_data x).
Show proof.
Definition functor_from_unit
{C : category}
(x : C)
: unit_category ⟶ C.
Show proof.
Definition nat_trans_from_unit_is_nat_trans
{C : category}
{x y : C}
(f : x --> y)
: is_nat_trans
(functor_from_unit x)
(functor_from_unit y)
(λ _, f).
Show proof.
Definition nat_trans_from_unit
{C : category}
{x y : C}
(f : x --> y)
: functor_from_unit x ⟹ functor_from_unit y.
Show proof.
Definition unit_category_nat_trans
{C : category}
(F G : C ⟶ unit_category)
: F ⟹ G.
Show proof.
Lemma nat_trans_to_unit_eq
{X : category}
(F G : X ⟶ unit_category)
(α β : F ⟹ G)
: α = β.
Show proof.
{C : category}
(x : C)
: functor_data unit_category C.
Show proof.
Definition functor_from_unit_is_functor
{C : category}
(x : C)
: is_functor (functor_from_unit_data x).
Show proof.
Definition functor_from_unit
{C : category}
(x : C)
: unit_category ⟶ C.
Show proof.
Definition nat_trans_from_unit_is_nat_trans
{C : category}
{x y : C}
(f : x --> y)
: is_nat_trans
(functor_from_unit x)
(functor_from_unit y)
(λ _, f).
Show proof.
Definition nat_trans_from_unit
{C : category}
{x y : C}
(f : x --> y)
: functor_from_unit x ⟹ functor_from_unit y.
Show proof.
Definition unit_category_nat_trans
{C : category}
(F G : C ⟶ unit_category)
: F ⟹ G.
Show proof.
use make_nat_trans.
- exact (λ _, pr1 (isapropunit _ _)).
- abstract
(intro ; intros ;
apply isasetunit).
- exact (λ _, pr1 (isapropunit _ _)).
- abstract
(intro ; intros ;
apply isasetunit).
Lemma nat_trans_to_unit_eq
{X : category}
(F G : X ⟶ unit_category)
(α β : F ⟹ G)
: α = β.
Show proof.
Morphisms are the same as certain natural transformations
Definition nat_trans_from_unit_weq_morphisms
{C : category}
(x y : C)
: x --> y ≃ (functor_from_unit x ⟹ functor_from_unit y).
Show proof.
{C : category}
(x y : C)
: x --> y ≃ (functor_from_unit x ⟹ functor_from_unit y).
Show proof.
use make_weq.
- exact nat_trans_from_unit.
- use isweq_iso.
+ exact (λ n, n tt).
+ abstract
(intro f ;
apply idpath).
+ abstract
(intros n ;
use nat_trans_eq ; [ apply homset_property | ] ;
intro z ; cbn ;
induction z ;
apply idpath).
- exact nat_trans_from_unit.
- use isweq_iso.
+ exact (λ n, n tt).
+ abstract
(intro f ;
apply idpath).
+ abstract
(intros n ;
use nat_trans_eq ; [ apply homset_property | ] ;
intro z ; cbn ;
induction z ;
apply idpath).
The category with no objects (empty_category)
Definition empty_category : univalent_category.
Show proof.
Section FunctorFromEmpty.
Context (A : precategory).
Definition functor_from_empty_data : functor_data empty_category A.
Show proof.
Definition is_functor_from_empty : is_functor functor_from_empty_data.
Show proof.
Definition functor_from_empty : functor empty_category A :=
make_functor _ is_functor_from_empty.
Compare to isaprop_is_functor. For a functor from the empty_category,
it's not necessary that the codomain has homsets.
Lemma isaprop_is_functor_from_empty
(F : functor_data empty_category A) : isaprop (is_functor F).
Show proof.
Lemma iscontr_functor_from_empty : iscontr (functor empty_category A).
Show proof.
(F : functor_data empty_category A) : isaprop (is_functor F).
Show proof.
apply isapropdirprod.
- unfold functor_idax.
apply impred; intro e; induction e.
- unfold functor_compax.
apply impred; intro e; induction e.
- unfold functor_idax.
apply impred; intro e; induction e.
- unfold functor_compax.
apply impred; intro e; induction e.
Lemma iscontr_functor_from_empty : iscontr (functor empty_category A).
Show proof.
use make_iscontr.
- exact functor_from_empty.
- intro F.
use total2_paths_f.
+ use total2_paths_f;
apply funextsec; intro empt; induction empt.
+ apply proofirrelevance, isaprop_is_functor_from_empty.
End FunctorFromEmpty.- exact functor_from_empty.
- intro F.
use total2_paths_f.
+ use total2_paths_f;
apply funextsec; intro empt; induction empt.
+ apply proofirrelevance, isaprop_is_functor_from_empty.
Natural transformations for the empty category
Definition nat_trans_from_empty
{C : category}
(F G : empty_category ⟶ C)
: nat_trans F G.
Show proof.
Definition nat_trans_to_empty
{C₁ C₂ : category}
(F : C₁ ⟶ empty_category)
(G : empty_category ⟶ C₂)
(H : C₁ ⟶ C₂)
: H ⟹ F ∙ G.
Show proof.
Definition nat_trans_to_empty_is_nat_z_iso
{C₁ C₂ : category}
(F : C₁ ⟶ empty_category)
(G : empty_category ⟶ C₂)
(H : C₁ ⟶ C₂)
: is_nat_z_iso (nat_trans_to_empty F G H).
Show proof.
Definition directed_interval_precategory_ob_mor
: precategory_ob_mor.
Show proof.
Definition directed_interval_precategory_data
: precategory_data.
Show proof.
Definition directed_interval_precategory_is_precategory
: is_precategory directed_interval_precategory_data.
Show proof.
Definition directed_interval_precategory
: precategory.
Show proof.
Definition directed_interval_category_has_homprops
(x y : directed_interval_precategory_ob_mor)
: isaprop (x --> y).
Show proof.
Definition directed_interval_category_has_homsets
: has_homsets directed_interval_precategory_ob_mor.
Show proof.
Definition directed_interval_category
: category.
Show proof.
Definition is_univalent_directed_interval
: is_univalent directed_interval_category.
Show proof.
Definition directed_interval
: univalent_category.
Show proof.
{C : category}
(F G : empty_category ⟶ C)
: nat_trans F G.
Show proof.
Definition nat_trans_to_empty
{C₁ C₂ : category}
(F : C₁ ⟶ empty_category)
(G : empty_category ⟶ C₂)
(H : C₁ ⟶ C₂)
: H ⟹ F ∙ G.
Show proof.
Definition nat_trans_to_empty_is_nat_z_iso
{C₁ C₂ : category}
(F : C₁ ⟶ empty_category)
(G : empty_category ⟶ C₂)
(H : C₁ ⟶ C₂)
: is_nat_z_iso (nat_trans_to_empty F G H).
Show proof.
Definition directed_interval_precategory_ob_mor
: precategory_ob_mor.
Show proof.
use make_precategory_ob_mor.
- exact bool.
- intros x y.
induction x ; induction y.
+ exact unit.
+ exact unit.
+ exact empty.
+ exact unit.
- exact bool.
- intros x y.
induction x ; induction y.
+ exact unit.
+ exact unit.
+ exact empty.
+ exact unit.
Definition directed_interval_precategory_data
: precategory_data.
Show proof.
use make_precategory_data.
- exact directed_interval_precategory_ob_mor.
- intro x.
induction x.
+ exact tt.
+ exact tt.
- intros x y z f g.
induction x ; induction y ; induction z ; cbn in *.
+ exact tt.
+ exact tt.
+ exact tt.
+ exact tt.
+ exact f.
+ exact tt.
+ exact g.
+ exact tt.
- exact directed_interval_precategory_ob_mor.
- intro x.
induction x.
+ exact tt.
+ exact tt.
- intros x y z f g.
induction x ; induction y ; induction z ; cbn in *.
+ exact tt.
+ exact tt.
+ exact tt.
+ exact tt.
+ exact f.
+ exact tt.
+ exact g.
+ exact tt.
Definition directed_interval_precategory_is_precategory
: is_precategory directed_interval_precategory_data.
Show proof.
use make_is_precategory_one_assoc.
- intros x y f.
induction x ; induction y ; cbn in *.
+ apply isapropunit.
+ apply isapropunit.
+ exact (fromempty f).
+ apply isapropunit.
- intros x y f.
induction x ; induction y ; cbn in *.
+ apply isapropunit.
+ apply isapropunit.
+ exact (fromempty f).
+ apply isapropunit.
- intros w x y z f g h.
induction w ; induction x ; induction y ; induction z ; cbn in * ; try (apply idpath).
exact (fromempty f).
- intros x y f.
induction x ; induction y ; cbn in *.
+ apply isapropunit.
+ apply isapropunit.
+ exact (fromempty f).
+ apply isapropunit.
- intros x y f.
induction x ; induction y ; cbn in *.
+ apply isapropunit.
+ apply isapropunit.
+ exact (fromempty f).
+ apply isapropunit.
- intros w x y z f g h.
induction w ; induction x ; induction y ; induction z ; cbn in * ; try (apply idpath).
exact (fromempty f).
Definition directed_interval_precategory
: precategory.
Show proof.
use make_precategory.
- exact directed_interval_precategory_data.
- exact directed_interval_precategory_is_precategory.
- exact directed_interval_precategory_data.
- exact directed_interval_precategory_is_precategory.
Definition directed_interval_category_has_homprops
(x y : directed_interval_precategory_ob_mor)
: isaprop (x --> y).
Show proof.
induction x ; induction y.
- apply isapropunit.
- apply isapropunit.
- apply isapropempty.
- apply isapropunit.
- apply isapropunit.
- apply isapropunit.
- apply isapropempty.
- apply isapropunit.
Definition directed_interval_category_has_homsets
: has_homsets directed_interval_precategory_ob_mor.
Show proof.
Definition directed_interval_category
: category.
Show proof.
use make_category.
- exact directed_interval_precategory.
- exact directed_interval_category_has_homsets.
- exact directed_interval_precategory.
- exact directed_interval_category_has_homsets.
Definition is_univalent_directed_interval
: is_univalent directed_interval_category.
Show proof.
intros x y.
use isweqimplimpl.
- intro f.
induction x ; induction y ; cbn in *.
+ apply idpath.
+ apply (fromempty (inv_from_z_iso f)).
+ apply (fromempty (pr1 f)).
+ apply idpath.
- apply isasetbool.
- use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)).
+ apply directed_interval_category_has_homprops.
+ intro.
apply isaprop_is_z_isomorphism.
use isweqimplimpl.
- intro f.
induction x ; induction y ; cbn in *.
+ apply idpath.
+ apply (fromempty (inv_from_z_iso f)).
+ apply (fromempty (pr1 f)).
+ apply idpath.
- apply isasetbool.
- use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)).
+ apply directed_interval_category_has_homprops.
+ intro.
apply isaprop_is_z_isomorphism.
Definition directed_interval
: univalent_category.
Show proof.
use make_univalent_category.
- exact directed_interval_category.
- exact is_univalent_directed_interval.
- exact directed_interval_category.
- exact is_univalent_directed_interval.