Library UniMath.CategoryTheory.categories.commrigs

Category of commrigs

Contents

  • Precategory of commrigs
  • Category of commrigs

Precategory of commrigs

Section def_commrig_precategory.

  Definition commrig_fun_space (A B : commrig) : hSet := make_hSet (rigfun A B) (isasetrigfun A B).

  Definition commrig_precategory_ob_mor : precategory_ob_mor :=
    tpair (λ ob : UU, ob -> ob -> UU) commrig (λ A B : commrig, commrig_fun_space A B).

  Definition commrig_precategory_data : precategory_data :=
    make_precategory_data
      commrig_precategory_ob_mor (λ (X : commrig), (rigisotorigfun (idrigiso X)))
      (fun (X Y Z : commrig) (f : rigfun X Y) (g : rigfun Y Z) => rigfuncomp f g).

  Local Lemma commrig_id_left (X Y : commrig) (f : rigfun X Y) :
    rigfuncomp (rigisotorigfun (idrigiso X)) f = f.
  Show proof.
    use rigfun_paths. apply idpath.
  Opaque commrig_id_left.

  Local Lemma commrig_id_commright (X Y : commrig) (f : rigfun X Y) :
    rigfuncomp f (rigisotorigfun (idrigiso Y)) = f.
  Show proof.
    use rigfun_paths. apply idpath.
  Opaque commrig_id_commright.

  Local Lemma commrig_assoc (X Y Z W : commrig) (f : rigfun X Y) (g : rigfun Y Z) (h : rigfun Z W) :
    rigfuncomp f (rigfuncomp g h) = rigfuncomp (rigfuncomp f g) h.
  Show proof.
    use rigfun_paths. apply idpath.
  Opaque commrig_assoc.

  Lemma is_precategory_commrig_precategory_data : is_precategory commrig_precategory_data.
  Show proof.
    use make_is_precategory_one_assoc.
    - intros a b f. use commrig_id_left.
    - intros a b f. use commrig_id_commright.
    - intros a b c d f g h. use commrig_assoc.

  Definition commrig_precategory : precategory :=
    make_precategory commrig_precategory_data is_precategory_commrig_precategory_data.

  Lemma has_homsets_commrig_precategory : has_homsets commrig_precategory.
  Show proof.
    intros X Y. use isasetrigfun.

End def_commrig_precategory.

Category of commrigs

(rigiso X Y) ≃ (z_iso X Y)


  Lemma commrig_iso_is_equiv (A B : ob commrig_category) (f : z_iso A B) : isweq (pr1 (pr1 f)).
  Show proof.
    use isweq_iso.
    - exact (pr1rigfun _ _ (inv_from_z_iso f)).
    - intros x.
      use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_inv_after_z_iso f)) x).
      intros x0. use isapropisrigfun.
    - intros x.
      use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_after_z_iso_inv f)) x).
      intros x0. use isapropisrigfun.
  Opaque commrig_iso_is_equiv.

  Lemma commrig_iso_equiv (X Y : ob commrig_category) :
    z_iso X Y -> rigiso (X : commrig) (Y : commrig).
  Show proof.
    intro f.
    use make_rigiso.
    - exact (make_weq (pr1 (pr1 f)) (commrig_iso_is_equiv X Y f)).
    - exact (pr2 (pr1 f)).

  Lemma commrig_equiv_is_z_iso (X Y : ob commrig_category)
        (f : rigiso (X : commrig) (Y : commrig)) :
    @is_z_isomorphism commrig_precategory X Y (rigfunconstr (pr2 f)).
  Show proof.
    exists (rigfunconstr (pr2 (invrigiso f))).
    use make_is_inverse_in_precat.
    - use rigfun_paths. use funextfun. intros x. use homotinvweqweq.
    - use rigfun_paths. use funextfun. intros y. use homotweqinvweq.
  Opaque commrig_equiv_is_z_iso.

  Lemma commrig_equiv_iso (X Y : ob commrig_category) :
    rigiso (X : commrig) (Y : commrig) -> z_iso X Y.
  Show proof.
    intros f. exact (_,,commrig_equiv_is_z_iso X Y f).

  Lemma commrig_iso_equiv_is_equiv (X Y : commrig_category) : isweq (commrig_iso_equiv X Y).
  Show proof.
    use isweq_iso.
    - exact (commrig_equiv_iso X Y).
    - intros x. use z_iso_eq. use rigfun_paths. apply idpath.
    - intros y. use rigiso_paths. use subtypePath.
      + intros x0. use isapropisweq.
      + apply idpath.
  Opaque commrig_iso_equiv_is_equiv.

  Definition commrig_iso_equiv_weq (X Y : ob commrig_category) :
    weq (z_iso X Y) (rigiso (X : commrig) (Y : commrig)).
  Show proof.
    use make_weq.
    - exact (commrig_iso_equiv X Y).
    - exact (commrig_iso_equiv_is_equiv X Y).

  Lemma commrig_equiv_iso_is_equiv (X Y : ob commrig_category) : isweq (commrig_equiv_iso X Y).
  Show proof.
    use isweq_iso.
    - exact (commrig_iso_equiv X Y).
    - intros y. use rigiso_paths. use subtypePath.
      + intros x0. use isapropisweq.
      + apply idpath.
    - intros x. use z_iso_eq. use rigfun_paths. apply idpath.
  Opaque commrig_equiv_iso_is_equiv.

  Definition commrig_equiv_weq_iso (X Y : ob commrig_category) :
    (rigiso (X : commrig) (Y : commrig)) (z_iso X Y).
  Show proof.
    use make_weq.
    - exact (commrig_equiv_iso X Y).
    - exact (commrig_equiv_iso_is_equiv X Y).

Category of commrigs


  Definition commrig_category_isweq (X Y : ob commrig_category) :
    isweq (λ p : X = Y, idtoiso p).
  Show proof.
    use (@isweqhomot
           (X = Y) (z_iso X Y)
           (pr1weq (weqcomp (commrig_univalence X Y) (commrig_equiv_weq_iso X Y)))
           _ _ (weqproperty (weqcomp (commrig_univalence X Y) (commrig_equiv_weq_iso X Y)))).
    intros e. induction e.
    use (pathscomp0 weqcomp_to_funcomp_app).
    use total2_paths_f.
    - apply idpath.
    - use proofirrelevance. use isaprop_is_z_isomorphism.
  Opaque commrig_category_isweq.

 Definition commrig_category_is_univalent : is_univalent commrig_category.
  Show proof.
    intros X Y. exact (commrig_category_isweq X Y).

  Definition commrig_univalent_category : univalent_category :=
    make_univalent_category commrig_category commrig_category_is_univalent.

End def_commrig_category.