Library UniMath.CategoryTheory.categories.grs

Category of grs

Contents

  • Precategory of grs
  • Category of grs

Precategory of grs

Section def_gr_precategory.

  Definition gr_fun_space (A B : gr) : hSet := make_hSet (monoidfun A B) (isasetmonoidfun A B).

  Definition gr_precategory_ob_mor : precategory_ob_mor :=
    tpair (λ ob : UU, ob -> ob -> UU) gr (λ A B : gr, gr_fun_space A B).

  Definition gr_precategory_data : precategory_data :=
    make_precategory_data
      gr_precategory_ob_mor (λ (X : gr), ((idmonoidiso X) : monoidfun X X))
      (fun (X Y Z : gr) (f : monoidfun X Y) (g : monoidfun Y Z) => monoidfuncomp f g).

  Local Lemma gr_id_left (X Y : gr) (f : monoidfun X Y) : monoidfuncomp (idmonoidiso X) f = f.
  Show proof.
    use monoidfun_paths. use idpath.
  Opaque gr_id_left.

  Local Lemma gr_id_right (X Y : gr) (f : monoidfun X Y) : monoidfuncomp f (idmonoidiso Y) = f.
  Show proof.
    use monoidfun_paths. use idpath.
  Opaque gr_id_right.

  Local Lemma gr_assoc (X Y Z W : gr) (f : monoidfun X Y) (g : monoidfun Y Z) (h : monoidfun Z W) :
    monoidfuncomp f (monoidfuncomp g h) = monoidfuncomp (monoidfuncomp f g) h.
  Show proof.
    use monoidfun_paths. use idpath.
  Opaque gr_assoc.

  Lemma is_precategory_gr_precategory_data : is_precategory gr_precategory_data.
  Show proof.
    use make_is_precategory_one_assoc.
    - intros a b f. use gr_id_left.
    - intros a b f. use gr_id_right.
    - intros a b c d f g h. use gr_assoc.

  Definition gr_precategory : precategory :=
    make_precategory gr_precategory_data is_precategory_gr_precategory_data.

  Lemma has_homsets_gr_precategory : has_homsets gr_precategory.
  Show proof.
    intros X Y. use isasetmonoidfun.

End def_gr_precategory.

Category of grs

(monoidiso X Y) ≃ (iso X Y)


  Lemma gr_iso_is_equiv (A B : ob gr_category) (f : z_iso A B) : isweq (pr1 (pr1 f)).
  Show proof.
    use isweq_iso.
    - exact (pr1monoidfun _ _ (inv_from_z_iso f)).
    - intros x.
      use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_inv_after_z_iso f)) x).
      intros x0. use isapropismonoidfun.
    - intros x.
      use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_after_z_iso_inv f)) x).
      intros x0. use isapropismonoidfun.
  Opaque gr_iso_is_equiv.

  Lemma gr_iso_equiv (X Y : ob gr_category) : z_iso X Y -> monoidiso (X : gr) (Y : gr).
  Show proof.
    intro f.
    use make_monoidiso.
    - exact (make_weq (pr1 (pr1 f)) (gr_iso_is_equiv X Y f)).
    - exact (pr2 (pr1 f)).

  Lemma gr_equiv_is_iso (X Y : ob gr_category) (f : monoidiso (X : gr) (Y : gr)) :
    @is_z_isomorphism gr_precategory X Y (monoidfunconstr (pr2 f)).
  Show proof.
    exists (monoidfunconstr (pr2 (invmonoidiso f))).
    use make_is_inverse_in_precat.
    - use monoidfun_paths. use funextfun. intros x. use homotinvweqweq.
    - use monoidfun_paths. use funextfun. intros y. use homotweqinvweq.
  Opaque gr_equiv_is_iso.

  Lemma gr_equiv_iso (X Y : ob gr_category) : monoidiso (X : gr) (Y : gr) -> z_iso X Y.
  Show proof.
    intros f. exact (_,,gr_equiv_is_iso X Y f).

  Lemma gr_iso_equiv_is_equiv (X Y : gr_category) : isweq (gr_iso_equiv X Y).
  Show proof.
    use isweq_iso.
    - exact (gr_equiv_iso X Y).
    - intros x. use z_iso_eq. use monoidfun_paths. use idpath.
    - intros y. use monoidiso_paths. use subtypePath.
      + intros x0. use isapropisweq.
      + use idpath.
  Opaque gr_iso_equiv_is_equiv.

  Definition gr_iso_equiv_weq (X Y : ob gr_category) :
    weq (z_iso X Y) (monoidiso (X : gr) (Y : gr)).
  Show proof.
    use make_weq.
    - exact (gr_iso_equiv X Y).
    - exact (gr_iso_equiv_is_equiv X Y).

  Lemma gr_equiv_iso_is_equiv (X Y : ob gr_category) : isweq (gr_equiv_iso X Y).
  Show proof.
    use isweq_iso.
    - exact (gr_iso_equiv X Y).
    - intros y. use monoidiso_paths. use subtypePath.
      + intros x0. use isapropisweq.
      + use idpath.
    - intros x. apply z_iso_eq. use monoidfun_paths. use idpath.
  Opaque gr_equiv_iso_is_equiv.

  Definition gr_equiv_weq_iso (X Y : ob gr_category) :
    (monoidiso (X : gr) (Y : gr)) (z_iso X Y).
  Show proof.
    use make_weq.
    - exact (gr_equiv_iso X Y).
    - exact (gr_equiv_iso_is_equiv X Y).

Category of grs


  Definition gr_precategory_isweq (X Y : ob gr_category) : isweq (λ p : X = Y, idtoiso p).
  Show proof.
    use (@isweqhomot
           (X = Y) (z_iso X Y)
           (pr1weq (weqcomp (gr_univalence X Y) (gr_equiv_weq_iso X Y)))
           _ _ (weqproperty (weqcomp (gr_univalence X Y) (gr_equiv_weq_iso X Y)))).
    intros e. induction e.
    use (pathscomp0 weqcomp_to_funcomp_app).
    use total2_paths_f.
    - use idpath.
    - use proofirrelevance. use isaprop_is_z_isomorphism.
  Opaque gr_precategory_isweq.

  Definition gr_category_is_univalent : is_univalent gr_category.
  Show proof.
    intros X Y. exact (gr_precategory_isweq X Y).

  Definition gr_univalent_category : univalent_category
    := make_univalent_category gr_category gr_category_is_univalent.

End def_gr_category.