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)

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.
intros. exact (compose f g).

The path/fundamental groupoid of a type

The pregroupoid with points in X as objects and paths as morphisms
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.

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.
  apply homset_property.

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)).

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.
  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.

Lemma is_univalent_path_groupoid (X:UU) (i : isofhlevel 3 X) :
  is_univalent (path_groupoid X i).
Show proof.
  apply is_univalent_pregroupoid_is_univalent,
          is_univalent_path_pregroupoid; assumption.

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 _).

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.
  split; split.
  - 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.
  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).

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.
  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.

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.
use make_nat_trans.
- intros z; apply (ϕ z).
- apply (is_nat_trans_discrete_precategory).

Characterization of discrete categories

Discrete categories are isomorphic to the path groupoid on their set of objects. This is analogous to the statement that any skeletal groupoid is discrete.

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.

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.
  apply path_groupoid_hset_is_discrete.

The category with one object (unit_category)


Definition unit_category : univalent_category.
Show proof.
  use path_univalent_groupoid.
  - exact unit.
  - do 2 (apply hlevelntosn). apply isapropunit.

Section FunctorToUnit.
  Context (A : precategory).

  Definition functor_to_unit_data : functor_data A unit_category.
  Show proof.
    use make_functor_data.
    - exact tounit.
    - exact (λ _ _ _, idpath _ ).

  Definition is_functor_to_unit : is_functor functor_to_unit_data.
  Show proof.
    split.
    - intro. apply idpath.
    - intros ? ? ? ? ?; apply idpath.

  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.

Functors from the unit category
Definition functor_from_unit_data
           {C : category}
           (x : C)
  : functor_data unit_category C.
Show proof.
  use make_functor_data.
  - exact (λ _, x).
  - exact (λ _ _ _, identity _).

Definition functor_from_unit_is_functor
           {C : category}
           (x : C)
  : is_functor (functor_from_unit_data x).
Show proof.
  split.
  - intro ; apply idpath.
  - intro ; intros ; cbn.
    rewrite id_left.
    apply idpath.

Definition functor_from_unit
           {C : category}
           (x : C)
  : unit_category ⟶ C.
Show proof.
  use make_functor.
  - exact (functor_from_unit_data x).
  - exact (functor_from_unit_is_functor x).

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.
  intro ; intros ; cbn.
  rewrite id_left, id_right.
  apply idpath.

Definition nat_trans_from_unit
           {C : category}
           {x y : C}
           (f : x --> y)
  : functor_from_unit x ⟹ functor_from_unit y.
Show proof.
  use make_nat_trans.
  - exact (λ _, f).
  - exact (nat_trans_from_unit_is_nat_trans f).

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).

Lemma nat_trans_to_unit_eq
      {X : category}
      (F G : X ⟶ unit_category)
      (α β : F ⟹ G)
  : α = β.
Show proof.
  apply nat_trans_eq.
  - apply homset_property.
  - intro z. apply isasetunit.

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.
  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).

The category with no objects (empty_category)


Definition empty_category : univalent_category.
Show proof.
  use path_univalent_groupoid.
  - exact empty.
  - do 2 (apply hlevelntosn). apply isapropempty.

Section FunctorFromEmpty.
  Context (A : precategory).

  Definition functor_from_empty_data : functor_data empty_category A.
  Show proof.
    use make_functor_data.
    - exact fromempty.
    - intros empt ?; induction empt.

  Definition is_functor_from_empty : is_functor functor_from_empty_data.
  Show proof.
    use tpair; intro a; induction a.

  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.
    apply isapropdirprod.
    - 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.

Natural transformations for the empty category
Definition nat_trans_from_empty
           {C : category}
           (F G : empty_category ⟶ C)
  : nat_trans F G.
Show proof.
  use make_nat_trans.
  - exact (λ z, fromempty z).
  - exact (λ z, fromempty z).

Definition nat_trans_to_empty
           {C₁ C₂ : category}
           (F : C₁ ⟶ empty_category)
           (G : empty_category ⟶ C₂)
           (H : C₁ ⟶ C₂)
  : H ⟹ F ∙ G.
Show proof.
  use make_nat_trans.
  - exact (λ x, fromempty (F x)).
  - exact (λ x y f, fromempty (F x)).

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.
  intro x.
  exact (fromempty (F x)).

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.

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.

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).

Definition directed_interval_precategory
  : precategory.
Show proof.
  use make_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.

Definition directed_interval_category_has_homsets
  : has_homsets directed_interval_precategory_ob_mor.
Show proof.
  intros x y.
  apply isasetaprop.
  exact (directed_interval_category_has_homprops x y).

Definition directed_interval_category
  : category.
Show proof.
  use make_category.
  - 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.

Definition directed_interval
  : univalent_category.
Show proof.
  use make_univalent_category.
  - exact directed_interval_category.
  - exact is_univalent_directed_interval.