Library UniMath.CategoryTheory.categories.Cats

The (pre)category of (pre)categories

This file defines the (pre)category of 𝒰-small (pre)categories, i.e. (pre)categories that fit within some fixed universe.
Author: Langston Barrett (@siddharthist), Feb 2018

Contents:

Definitions

The precategory of 𝒰-small precategories (for fixed 𝒰) (precat_precat)


Definition precat_precat : precategory.
Proof.
  use mk_precategory_one_assoc.
  - use tpair; use tpair; cbn.
    + exact precategory.
    + exact functor.
    + exact functor_identity.
    + exact @functor_composite.
  - repeat split; intros.
    + apply functor_identity_right.
    + apply pathsinv0, functor_assoc.
Defined.

The precategory of 𝒰-small categories (cat_precat)

A subcategory can be coerced to a precategory, see carrier_of_sub_precategory.
It's not the case that cat_precat has homsets.

The precategory of 𝒰-small univalent categories (univalent_cat_precat)

This can also be seen as a subcategory of cat_precat. An isommorphism between them would be useful because it is easier to prove e.g. that cat_precat has products, and then inherit them in univalent_cat_precat.
Two copies of a proposition are as good as one. This is like the structural rule of contraction.
Local Lemma dirprod_with_prop (A : UU) (isa : isaprop A) : A × A A.
Proof.
  apply weqpr1, iscontraprop1; assumption.
Defined.

A variation on the above theme
Local Lemma dirprod_with_prop' (A B : UU) (isa : isaprop A) : A × B × A B × A.
Proof.
  intermediate_weq ((A × B) × A).
  apply invweq, weqtotal2asstor.
  intermediate_weq (A × (A × B)).
  apply weqdirprodcomm.
  intermediate_weq ((A × A) × B).
  apply invweq, weqtotal2asstor.
  intermediate_weq (A × B).
  apply weqdirprodf.
  - apply dirprod_with_prop; assumption.
  - apply idweq.
  - apply weqdirprodcomm.
Defined.

Lemma univalent_cat_precat_subcat_weq :
  univalent_cat_precat univalent_cat_precat'.
Proof.
To get to the actual issue, it helps to do a lot of unfolding.
  cbn; unfold sub_ob; cbn.
  unfold univalent_cat_precat_subtype, univalent_cat_precat_subtype', carrier; cbn.
  unfold sub_ob, cat_precat_subtype.
  unfold sub_precategory_predicate_objects; cbn.
  unfold cat_precat_subtype, carrier; cbn.
  apply invweq.
  intermediate_weq ( x : precategory, has_homsets x × is_univalent x).
  - apply weqtotal2asstor.
  - unfold is_univalent.
    apply weqfibtototal; intro.
    apply dirprod_with_prop'.
    apply isaprop_has_homsets.
Defined.

The category of 𝒰-small set categories (setcat_cat)

The precategory of 𝒰-small categories with objects of hlevel n and homtypes

of hlevel m.

Setcategories, the case where n = m = 2.


Definition setcat_precat : sub_precategories precat_precat := hlevel_precat 2 2.

Lemma has_homsets_setcat_precat : has_homsets setcat_precat.
Proof.
  intros X Y; apply isaset_total2.
  - apply functor_isaset.
    + apply isaset_mor.
    + apply isaset_ob.
  - intro.
    change isaset with (isofhlevel 2).
    apply isofhlevelcontr, iscontrunit.
Defined.

Definition setcat_cat : category := category_pair _ has_homsets_setcat_precat.

Colimits

Initial objects

Initial precategory (InitialPrecat)


Definition InitialPrecat : Initial precat_precat.
Proof.
  use mk_Initial.
  - cbn; exact empty_category.
  - intros ?; apply iscontr_functor_from_empty.
Defined.

Initial category (InitialCat)


Definition InitialCat : Initial cat_precat.
Proof.
  use (initial_in_full_subcategory _ InitialPrecat).
  apply homset_property.
Defined.

Initial univalent category (InitialUniCat)

Initial set category (InitialSetCat)


Definition InitialSetCat : Initial setcat_cat.
Proof.
  use (initial_in_full_subcategory _ InitialPrecat).
  split.
  - apply hlevelntosn, isapropempty.
  - intros a; induction a.
Defined.

Limits

Terminal objects

Terminal (pre)category (TerminalPrecat)


Definition TerminalPrecat : Terminal precat_precat.
Proof.
  use mk_Terminal.
  - cbn; exact unit_category.
  - intros ?; apply iscontr_functor_to_unit.
Defined.

Terminal category (TerminalCat)


Definition TerminalCat : Terminal cat_precat.
Proof.
  use (terminal_in_full_subcategory _ TerminalPrecat).
  apply homset_property.
Defined.

Terminal univalent category (TerminalUniCat)

Terminal setcategory (TerminalSetCat)


Definition TerminalSetCat : Terminal setcat_cat.
Proof.
  use (terminal_in_full_subcategory _ TerminalPrecat).
  split.
  - apply isofhlevelcontr, iscontrunit.
  - intros a b.
    apply isofhlevelcontr; cbn.
    apply isapropunit.
Defined.

Products

Product category (ProductsCat)

We essentially proved the universal property in functor_into_product_weq, an equivalence between A → (product_category B) and (∏ i : I, A → (B i)).
Definition ProductsCat {I : UU} : Products I cat_precat.
Proof.
  intros f; cbn in ×.
  use mk_Product.
  - exact (product_category f).
  - intro i.
    use morphism_in_full_subcat.
    exact (pr_functor I (pr1 f) i).
  - intros other_prod other_proj; cbn in other_proj.
    unfold funcomp; cbn.
    apply (@iscontrweqf (hfiber functor_into_product_weq (λ i, pr1 (other_proj i)))).
    + unfold hfiber.
      unfold sub_precategory_morphisms, sub_precategory_predicate_morphisms; cbn.
      unfold carrier, hProptoType; cbn.
      intermediate_weq
        ( x : (pr1 (pr1 other_prod)) product_precategory_data (λ x : I, pr1 (f x)),
           i, x pr_functor I (λ x0 : I, pr1 (f x0)) i = pr1 (other_proj i)).
      × use weqfibtototal; intro; cbn.
        apply weqtoforallpaths.
      × apply invweq.
        intermediate_weq
          ( ff : pr1 (pr1 other_prod) product_precategory_data (λ x : I, pr1 (f x)),
             i : I, ff pr_functor I (λ x : I, pr1 (f x)) i,, tt = other_proj i).
        {
          refine (weqfp (weqpair pr1 _) _).
          apply isweqpr1.
          intros ?.
          apply iscontrunit.
        }
        {
          apply weqfibtototal; intro.
          apply weqonsecfibers; intro.
          use weqpair.
          × intros eq; exact (maponpaths pr1 eq).
          × refine (isweqmaponpaths (weqpair pr1 _) _ _).
            apply isweqpr1.
            intros.
            apply iscontrunit.
        }
  + apply weqproperty.
Defined.