Library UniMath.CategoryTheory.categories.abmonoids

Category of abmonoids

Contents

  • Precategory of abmonoids
  • Category of abmonoids

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.Foundations.UnivalenceAxiom.

Require Import UniMath.Algebra.BinaryOperations.
Require Import UniMath.Algebra.Monoids.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Local Open Scope cat.

Precategory of abmonoids

Section def_abmonoid_precategory.

  Definition abmonoid_fun_space (A B : abmonoid) : hSet :=
    hSetpair (monoidfun A B) (isasetmonoidfun A B).

  Definition abmonoid_precategory_ob_mor : precategory_ob_mor :=
    tpair (λ ob : UU, ob -> ob -> UU) abmonoid (λ A B : abmonoid, abmonoid_fun_space A B).

  Definition abmonoid_precategory_data : precategory_data :=
    precategory_data_pair
      abmonoid_precategory_ob_mor (λ (X : abmonoid), ((idmonoidiso X) : monoidfun X X))
      (fun (X Y Z : abmonoid) (f : monoidfun X Y) (g : monoidfun Y Z) => monoidfuncomp f g).

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

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

  Local Lemma abmonoid_assoc (X Y Z W : abmonoid) (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 abmonoid_assoc.

  Lemma is_precategory_abmonoid_precategory_data : is_precategory abmonoid_precategory_data.
  Show proof.
    use mk_is_precategory_one_assoc.
    - intros a b f. use abmonoid_id_left.
    - intros a b f. use abmonoid_id_right.
    - intros a b c d f g h. use abmonoid_assoc.

  Definition abmonoid_precategory : precategory :=
    mk_precategory abmonoid_precategory_data is_precategory_abmonoid_precategory_data.

  Lemma has_homsets_abmonoid_precategory : has_homsets abmonoid_precategory.
  Show proof.
    intros X Y. use isasetmonoidfun.

End def_abmonoid_precategory.

Category of abmonoids

Section def_abmonoid_category.

(monoidsiso X Y) ≃ (iso X Y)


  Lemma abmonoid_iso_is_equiv (A B : ob abmonoid_precategory) (f : iso A B) : isweq (pr1 (pr1 f)).
  Show proof.
    use isweq_iso.
    - exact (pr1monoidfun _ _ (inv_from_iso f)).
    - intros x.
      use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (iso_inv_after_iso f)) x).
      intros x0. use isapropismonoidfun.
    - intros x.
      use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (iso_after_iso_inv f)) x).
      intros x0. use isapropismonoidfun.
  Opaque abmonoid_iso_is_equiv.

  Lemma abmonoid_iso_equiv (X Y : ob abmonoid_precategory) :
    iso X Y -> monoidiso (X : abmonoid) (Y : abmonoid).
  Show proof.
    intro f.
    use monoidisopair.
    - exact (weqpair (pr1 (pr1 f)) (abmonoid_iso_is_equiv X Y f)).
    - exact (pr2 (pr1 f)).

  Lemma abmonoid_equiv_is_iso (X Y : ob abmonoid_precategory)
        (f : monoidiso (X : abmonoid) (Y : abmonoid)) :
    @is_iso abmonoid_precategory X Y (monoidfunconstr (pr2 f)).
  Show proof.
    use is_iso_qinv.
    - exact (monoidfunconstr (pr2 (invmonoidiso f))).
    - use mk_is_inverse_in_precat.
      + use monoidfun_paths. use funextfun. intros x. use homotinvweqweq.
      + use monoidfun_paths. use funextfun. intros y. use homotweqinvweq.
  Opaque abmonoid_equiv_is_iso.

  Lemma abmonoid_equiv_iso (X Y : ob abmonoid_precategory) :
    monoidiso (X : abmonoid) (Y : abmonoid) -> iso X Y.
  Show proof.
    intros f. exact (@isopair abmonoid_precategory X Y (monoidfunconstr (pr2 f))
                              (abmonoid_equiv_is_iso X Y f)).

  Lemma abmonoid_iso_equiv_is_equiv (X Y : ob abmonoid_precategory) :
    isweq (abmonoid_iso_equiv X Y).
  Show proof.
    use isweq_iso.
    - exact (abmonoid_equiv_iso X Y).
    - intros x. use eq_iso. use monoidfun_paths. use idpath.
    - intros y. use monoidiso_paths. use subtypeEquality.
      + intros x0. use isapropisweq.
      + use idpath.
  Opaque abmonoid_iso_equiv_is_equiv.

  Definition abmonoid_iso_equiv_weq (X Y : ob abmonoid_precategory) :
    weq (iso X Y) (monoidiso (X : abmonoid) (Y : abmonoid)).
  Show proof.
    use weqpair.
    - exact (abmonoid_iso_equiv X Y).
    - exact (abmonoid_iso_equiv_is_equiv X Y).

  Lemma abmonoid_equiv_iso_is_equiv (X Y : ob abmonoid_precategory) :
    isweq (abmonoid_equiv_iso X Y).
  Show proof.
    use isweq_iso.
    - exact (abmonoid_iso_equiv X Y).
    - intros y. use monoidiso_paths. use subtypeEquality.
      + intros x0. use isapropisweq.
      + use idpath.
    - intros x. use eq_iso. use monoidfun_paths. use idpath.
  Opaque abmonoid_equiv_iso_is_equiv.

  Definition abmonoid_equiv_weq_iso (X Y : ob abmonoid_precategory) :
    (monoidiso (X : abmonoid) (Y : abmonoid)) ≃ (iso X Y).
  Show proof.
    use weqpair.
    - exact (abmonoid_equiv_iso X Y).
    - exact (abmonoid_equiv_iso_is_equiv X Y).

Category of abmonoids


  Definition abmonoid_precategory_isweq (X Y : ob abmonoid_precategory) :
    isweq (λ p : X = Y, idtoiso p).
  Show proof.
    use (@isweqhomot
           (X = Y) (iso X Y)
           (pr1weq (weqcomp (abmonoid_univalence X Y) (abmonoid_equiv_weq_iso X Y)))
           _ _ (weqproperty (weqcomp (abmonoid_univalence X Y) (abmonoid_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_iso.
  Opaque abmonoid_precategory_isweq.

  Definition abmonoid_precategory_is_univalent : is_univalent abmonoid_precategory.
  Show proof.
    use mk_is_univalent.
    - intros X Y. exact (abmonoid_precategory_isweq X Y).
    - exact has_homsets_abmonoid_precategory.

  Definition abmonoid_category : univalent_category :=
    mk_category abmonoid_precategory abmonoid_precategory_is_univalent.

End def_abmonoid_category.