Library UniMath.CategoryTheory.Groupoids

  intros ig.
  intros a b.
  use (isofhlevelff 0 idtoiso (morphism_from_z_iso _ _)).
  + use (isweqhomot (idtomor _ _)).
    * intro p; destruct p; reflexivity.
    * apply ig.
  + apply (morphism_from_iso_is_incl pgpd).

Lemmas

In a pregroupoid, the hom-types are equivalent to the type of isomorphisms.

Lemma pregroupoid_hom_weq_iso {pgpd : pregroupoid} (a b : pgpd) : (a --> b ) ≃ z_iso a b.
Show proof.

  use weq_iso.
  - intros f; refine (f,, _); apply pregroupoid_is_pregroupoid.
  - apply pr1.
  - reflexivity.
  - intro; apply z_iso_eq; reflexivity.

Lemma pregroupoid_hom_weq_iso_idtoiso {pgpd : pregroupoid} (a : pgpd) :
pregroupoid_hom_weq_iso a a (identity a) = idtoiso (idpath a).
Show proof.

apply z_iso_eq; reflexivity.

Lemma pregroupoid_hom_weq_iso_comp {pgpd : pregroupoid} {a b c : ob pgpd}
      (f : a --> b) (g : b --> c) :
  z_iso_comp (pregroupoid_hom_weq_iso _ _ f) (pregroupoid_hom_weq_iso _ _ g) =
  (pregroupoid_hom_weq_iso _ _ (f · g)).
Show proof.

apply z_iso_eq; reflexivity.

If D is a groupoid, then a functor category into it is as well.

Lemma is_pregroupoid_functor_cat {C : precategory} {D : category}
(gr_D : is_pregroupoid D)
: is_pregroupoid (functor_category C D).
Show proof.

intros F G α; apply nat_trafo_z_iso_if_pointwise_z_iso.
intros c; apply gr_D.

In a univalent groupoid, arrows are equivalent to paths

Lemma univalent_groupoid_arrow_weq_path {ugpd : univalent_groupoid} {a b : ob ugpd} :
(a --> b ) ≃ a = b.
Show proof.

  intermediate_weq (z_iso a b).
  - apply (@pregroupoid_hom_weq_iso ugpd).
  - apply invweq; use make_weq.
    + exact idtoiso.
    + apply univalent_category_is_univalent.

Subgroupoids

Every category has a subgroupoid of all the objects and only the isos.

Definition maximal_subgroupoid {C : category} : pregroupoid.
Show proof.

  use make_pregroupoid.
  - use make_category.
    + use make_precategory; use tpair.
      * use tpair.
        -- exact (ob C).
        -- exact (λ a b , ∑ f : a --> b , is_z_isomorphism f).
      * unfold precategory_id_comp; cbn.
        use make_dirprod.
        -- exact (λ a , identity a ,, identity_is_z_iso _).
        -- intros ? ? ? f g; exact (z_iso_comp f g).
      * use make_dirprod;
        intros;
        apply z_iso_eq.
        -- apply id_left.
        -- apply id_right.
      * use make_dirprod; intros; apply z_iso_eq.
        -- apply assoc.
        -- apply assoc'.
    + cbn. intros a b. cbn. apply isaset_z_iso.
  - intros ? ? f. exists (z_iso_inv_from_z_iso f).
    use make_dirprod; apply z_iso_eq.
    + apply z_iso_inv_after_z_iso.
    + apply z_iso_after_z_iso_inv.

Goal ∏ C :category , pregroupoid_to_precategory (@maximal_subgroupoid (C ^op ))
= (@maximal_subgroupoid C )^op.
Show proof.

Fail reflexivity.
Abort.
Goal ∏ (C :category ) (a b :C ) (f : C ⟦ b , a ⟧), @is_z_isomorphism C ^op a b f = @is_z_isomorphism C b a f.
Proof.
Fail reflexivity.
Abort.

Discrete categories

See Categories.categories.StandardCategories for a proof that any discrete category is equivalent to the path groupoid of its objects.

A discrete category is a univalent pregroupoid with an underlying setcategory. Why? In this case, all arrows must be identities: every arrow has an inverse, and isos induce equality (by univalence).

Definition is_discrete (C : category) :=
  (is_setcategory C × is_pregroupoid C × is_univalent C).

Definition discrete_category : UU := ∑ C : category , is_discrete C.
Definition make_discrete_category :
  ∏ C : category , is_discrete C → discrete_category := tpair is_discrete.
Definition discrete_category_to_univalent_groupoid :
  discrete_category -> univalent_groupoid :=
  λ disc , make_univalent_groupoid
            (make_univalent_category (pr1 disc) (dirprod_pr2 (dirprod_pr2 (pr2 disc))))
            (dirprod_pr1 (dirprod_pr2 (pr2 disc))).
Coercion discrete_category_to_univalent_groupoid :
  discrete_category >-> univalent_groupoid.
Definition discrete_category_is_discrete :
  ∏ C : discrete_category , is_discrete C := pr2.
Definition discrete_category_is_setcategory :
  ∏ C : discrete_category , is_setcategory C := λ C , dirprod_pr1 (pr2 C).

Lemma isaprop_is_discrete (C : category) : isaprop (is_discrete C).
Proof.
  apply isapropdirprod; [|apply isapropdirprod].
  - apply isaprop_is_setcategory.
  - apply isaprop_is_pregroupoid.
  - apply isaprop_is_univalent.

In a discrete category, hom-types are propositions.

Lemma discrete_category_hom_prop {disc : discrete_category} {a b : ob disc} :
isaprop (a --> b).
Show proof.

  apply (@isofhlevelweqf _ (a = b)).
  - apply invweq, (@univalent_groupoid_arrow_weq_path disc).
  - apply (isaset_ob (_ ,, discrete_category_is_setcategory _)).

A functor between discrete categories is given by a function on their objects.

Lemma discrete_functor {C D : discrete_category} (f : ob C → ob D) :
functor C D.
Show proof.

  use make_functor.
  - use make_functor_data.
    + apply f.
    + intros a b atob.
      pose (aeqb := @univalent_groupoid_arrow_weq_path C _ _ atob).
      exact (transportf (λ z , _ ⟦ f a, z ⟧) (maponpaths f aeqb) (identity _)).
  - split.
    + intro; apply discrete_category_hom_prop.
    + intros ? ? ? ? ?; apply discrete_category_hom_prop.

Definition discrete_cat_nat_trans {C : precategory} {D : discrete_category}
{F G : functor C D} (t : ∏ x : ob C , F x --> G x) : is_nat_trans F G t.
Show proof.

intros ? ? ?; apply discrete_category_hom_prop.

Library UniMath.CategoryTheory.Groupoids

Groupoids

Contents

Definitions

Lemmas

Subgroupoids

Discrete categories