Library UniMath.CategoryTheory.Monoidal.Comonoids.Category

In this file, the category of comonoids internal to a monoidal category is defined.

repeat (apply isapropdirprod) ; apply homset_property.

  Definition comonoid_laws_disp_cat
    : disp_cat (total_category disp_cat_of_comonoids_data).
  Show proof.

exact (disp_full_sub _ (λ m , comonoid_laws m)).

  Lemma locally_propositional_comonoid_laws_disp_cat
    : locally_propositional comonoid_laws_disp_cat.
  Show proof.

intro ; intros ; apply isapropunit.

    simple refine ((_ ,, _) ,, _).
    - exact f_δ.
    - exact f_ε.
    - exact tt.

  Definition comonoid_mor (m n : comonoid)
    : UU
    := (total_category disp_cat_of_comonoids )⟦m ,n ⟧.

  Definition is_comonoid_mor_comult
    (m n : comonoid) (f : V ⟦m ,n ⟧) : UU
    := δ_{m } · (f #⊗ f ) = f · δ_{n }.

  Definition comonoid_mor_comult_law
    {m n : comonoid} (f : comonoid_mor m n)
    : is_comonoid_mor_comult m n (pr1 f)

    := pr112 f.

  Definition is_comonoid_mor_counit
    (m n : comonoid) (f : V ⟦m ,n ⟧) : UU
    := f · ε_{n } = ε_{m }.

  Definition comonoid_mor_counit_law
    {m n : comonoid} (f : comonoid_mor m n)
    : is_comonoid_mor_counit m n (pr1 f)

    := ! pr212 f @ id_right _.

  Lemma is_locally_propositional_comonoid
    : locally_propositional disp_cat_of_comonoids.
  Show proof.

    intro ; intros.
    use (isaprop_total2 (_ ,, _) (λ _ , _ ,, isapropunit)).
    apply (isaprop_total2
             (_ ,, homset_property _ _ _ _ _)
             (λ _ , _ ,, homset_property _ _ _ _ _)).

End CategoryOfComonoids.

Module ComonoidNotations.

  Notation "δ_{ m }" := (comonoid_comult _ m).
  Notation "ε_{ m }" := (comonoid_counit _ m).

End ComonoidNotations.

Section CategoryOfCommutativeComonoids.

  Context (V : sym_monoidal_cat).

  Import ComonoidNotations.

  Definition is_commutative (m : comonoid V) : UU
    := δ_{m } · sym_mon_braiding V m m = δ_{m }.

  Definition commutative_comonoids_laws_disp_cat
    : disp_cat (comonoid_category V).
  Show proof.

exact (disp_full_sub _ is_commutative).

    intro ; intros.
    use (isaprop_total2 (_ ,, _) (λ _ , _ ,, isapropunit)).
    use (isaprop_total2 (_ ,, _) (λ _ , _ ,, isapropunit)).
    apply (isaprop_total2
             (_ ,, homset_property _ _ _ _ _)
             (λ _ , _ ,, homset_property _ _ _ _ _)).

  Definition underlying_commutative_comonoid
    : commutative_comonoid_category ⟶ V
    := pr1_category _.
End CategoryOfCommutativeComonoids.

Section CommutativeComonoidsMorBuilder.
  Import ComonoidNotations.

  Context {V : sym_monoidal_cat}
          (C₁ C₂ : commutative_comonoid V)
          (f : underlying_commutative_comonoid _ C₁ --> underlying_commutative_comonoid _ C₂)
          (fδ : δ_{C₁ } · f #⊗ f = f · δ_{C₂ })
          (fε : ε_{C₁ } = f · ε_{C₂ }).

  Definition make_commutative_comonoid_mor
    : C₁ --> C₂.
  Show proof.

    refine (f ,, ((_ ,, _) ,, tt ) ,, tt).
    - exact fδ.
    - abstract
        (cbn ;
         rewrite id_right ;
         exact fε).

End CommutativeComonoidsMorBuilder.

Definition underlying_comonoid_mor
           {V : sym_monoidal_cat}
           {C₁ C₂ : commutative_comonoid V}
           (f : C₁ --> C₂)
  : underlying_commutative_comonoid _ C₁ --> underlying_commutative_comonoid _ C₂
  := pr1 f.

Section CommutativeComonoidsMorProjections.
  Import ComonoidNotations.

  Context {V : sym_monoidal_cat}
          {C₁ C₂ : commutative_comonoid V}
          (f : C₁ --> C₂).

  Proposition underlying_comonoid_mor_comult
    : δ_{C₁ } · underlying_comonoid_mor f #⊗ underlying_comonoid_mor f
      =
      underlying_comonoid_mor f · δ_{C₂ }.
  Show proof.

exact (pr1 (pr112 f)).

  Proposition underlying_comonoid_mor_counit
    : ε_{C₁ } = underlying_comonoid_mor f · ε_{C₂ }.
  Show proof.

refine (_ @ pr2 (pr112 f)).
exact (!(id_right _)).

End CommutativeComonoidsMorProjections.

This gives a more convenient builder for commutative comonoids for the bundled version. Note: only one identity law has to be proven

Section MakeCommutativeComonoid.
  Context {V : sym_monoidal_cat}
          (x : V)
          (δ : x --> x ⊗ x)
          (ε : x --> I_{V })
          (unit_left : δ · (ε #⊗ identity x ) · mon_lunitor x = identity x)
          (assocδ : δ · (δ #⊗ identity x ) · mon_lassociator x x x = δ · (identity x #⊗ δ ))
          (comm : δ · sym_mon_braiding V x x = δ).

  Definition make_commutative_comonoid_data
    : comonoid_data V
    := x ,, δ ,, ε.

  Proposition make_commutative_comonoid_laws
    : comonoid_laws V make_commutative_comonoid_data.
  Show proof.

    repeat split.
    - refine (_ @ unit_left) ; cbn.
      apply maponpaths_2.
      apply maponpaths.
      rewrite tensor_mor_right.
      apply idpath.
    - refine (_ @ unit_left) ; cbn.
      refine (!_).
      etrans.
      {
        do 2 apply maponpaths_2.
        exact (!(comm )).
      }
      rewrite !assoc'.
      apply maponpaths.
      rewrite !assoc.
      rewrite <- tensor_sym_mon_braiding.
      rewrite !assoc'.
      rewrite sym_mon_braiding_lunitor.
      apply maponpaths_2.
      rewrite tensor_mor_left.
      apply idpath.
    - unfold comonoid_laws_assoc ; cbn.
      refine (_ @ assocδ @ _).
      + apply maponpaths_2.
        apply maponpaths.
        rewrite tensor_mor_right.
        apply idpath.
      + apply maponpaths.
        rewrite tensor_mor_left.
        apply idpath.

  Definition make_commutative_comonoid
    : commutative_comonoid V.
  Show proof.

    simple refine (x ,, ((δ ,, ε ) ,, _) ,, _) ; cbn.
    - exact make_commutative_comonoid_laws.
    - exact comm.

End MakeCommutativeComonoid.

Section ComonoidAux.

  Context (M : monoidal_cat).

  Import ComonoidNotations.

  Definition comonoid_laws_assoc'
    (m : comonoid M)
    : δ_{m } · (δ_{m } ⊗^{M }_{r } m ) = δ_{m } · m ⊗^{M }_{l } δ_{m } · mon_rassociator m m m.
  Show proof.

    rewrite <- comonoid_to_law_assoc.
    rewrite ! assoc'.
    etrans.
    2: {
      do 2 apply maponpaths.
      apply pathsinv0.
      apply monoidal_associatorisolaw.
    }
    now rewrite id_right.

  Definition comonoid_laws_unit_left'
    (m : comonoid M)
    : δ_{m } · (ε_{m } ⊗^{M }_{r } m ) = mon_linvunitor m.
  Show proof.

    refine (_ @ id_left _).
    rewrite <- comonoid_to_law_unit_left.
    rewrite ! assoc'.
    etrans.
    2: {
      do 2 apply maponpaths.
      apply pathsinv0.
      apply monoidal_leftunitorisolaw.
    }
    now rewrite id_right.

  Definition comonoid_laws_unit_right'
    (m : comonoid M)
    : δ_{m } · (m ⊗^{M }_{l } ε_{m }) = mon_rinvunitor m.
  Show proof.

    refine (_ @ id_left _).
    rewrite <- (comonoid_to_law_unit_right M _).
    rewrite ! assoc'.
    etrans.
    2: {
      do 2 apply maponpaths.
      apply pathsinv0.
      apply monoidal_rightunitorisolaw.
    }
    now rewrite id_right.

End ComonoidAux.

Section CommutativeComonoids.

  Context (M : sym_monoidal_cat).
  Import ComonoidNotations.

  Lemma comultiplication_comonoid_4times'
    (m : comonoid M)
    : δ_{m } · δ_{m } #⊗ δ_{m }
      = δ_{m } · δ_{m } ⊗^{M }_{r } m · mon_lassociator _ _ _ · δ_{m } ⊗^{M }_{r } _.
  Show proof.

    etrans. {
      apply maponpaths.
      apply (bifunctor_equalwhiskers M).
    }

    unfold functoronmorphisms2.
    rewrite assoc.
    apply maponpaths_2.
    apply pathsinv0.
    apply comonoid_to_law_assoc.

  Lemma comultiplication_comonoid_4times_symmetry
    (m : commutative_comonoid M)
    : δ_{m } · δ_{m } #⊗ δ_{m } · (sym_mon_braiding M m m #⊗ sym_mon_braiding M m m )
      = δ_{m } · δ_{m } #⊗ δ_{m }.
  Show proof.

    rewrite assoc'.
    apply maponpaths.
    refine (! tensor_comp_mor _ _ _ _ @ _).
    now rewrite commutative_comonoid_is_commutative.

  Lemma comultiplication_comonoid_4times_symmetry_left
    (m : commutative_comonoid M)
    : δ_{m } · δ_{m } #⊗ δ_{m } · (sym_mon_braiding M m m ⊗^{M }_{r } (m ⊗_{M } m ))
      = δ_{m } · δ_{m } #⊗ δ_{m }.
  Show proof.

    rewrite assoc'.
    apply maponpaths.
    rewrite <- (when_bifunctor_becomes_rightwhiskering M).
    refine (! tensor_comp_mor _ _ _ _ @ _).
    rewrite id_right.
    apply maponpaths_2.
    apply commutative_comonoid_is_commutative.

  Lemma commutative_symmetric_braiding_using_lwhisker
    (m : commutative_comonoid M)
    : δ_{m } · δ_{m } #⊗ δ_{m } · α ^{M }_{_,_,_}
      = δ_{m } · (m ⊗^{M }_{l } δ_{m }) · (m ⊗^{M }_{l } (m ⊗^{M }_{l } δ_{m })).
  Show proof.

    etrans.
    2: {
      apply maponpaths_2.
      apply comonoid_to_law_assoc.
    }
    rewrite ! assoc'.
    apply maponpaths.
    apply pathsinv0.
    etrans. {
      apply maponpaths.
      apply (monoidal_associatornatleft M).
    }
    now rewrite ! assoc.

  Lemma commutative_symmetric_braiding_using_lrwhisker
    (m : commutative_comonoid M)
    : δ_{m } · (m ⊗^{M }_{l } δ_{m }) · (m ⊗^{M }_{l } (m ⊗^{M }_{l } δ_{m })) · m ⊗^{M }_{l } mon_rassociator _ _ _
      = δ_{m } · (m ⊗^{M }_{l } δ_{m }) · (m ⊗^{M }_{l } (δ_{m } ⊗^{M }_{r } m )).
  Show proof.

    rewrite ! assoc'.
    apply maponpaths.
    rewrite <- (bifunctor_leftcomp M).
    etrans. {
      apply pathsinv0, (bifunctor_leftcomp M).
    }
    etrans.
    2: {
      apply (bifunctor_leftcomp M).
    }
    apply maponpaths.
    refine (_ @ ! comonoid_laws_assoc' M m).
    apply assoc.

  Lemma commutative_symmetric_braiding_using_lrwhisker'
    (m : commutative_comonoid M)
    : δ_{m } · (m ⊗^{M }_{l } δ_{m }) · (m ⊗^{M }_{l } (δ_{m } ⊗^{M }_{r } m )) · m ⊗^{M }_{l } ((sym_mon_braiding M m m ) ⊗^{M }_{r } m )
      = δ_{m } · (m ⊗^{M }_{l } δ_{m }) · (m ⊗^{M }_{l } (δ_{m } ⊗^{M }_{r } m )).
  Show proof.

    rewrite ! assoc'.
    do 2 apply maponpaths.
    rewrite <- (bifunctor_leftcomp M).
    apply maponpaths.
    rewrite <- (bifunctor_rightcomp M).
    apply maponpaths.
    apply commutative_comonoid_is_commutative.

  Lemma commutative_symmetric_braiding_using_lrwhisker''
    (m : commutative_comonoid M)
    : δ_{m } · δ_{m } #⊗ δ_{m } · α ^{M }_{_,_,_} · m ⊗^{M }_{l } mon_rassociator _ _ _ · m ⊗^{M }_{l } ((sym_mon_braiding M m m ) ⊗^{M }_{r } m )
      = δ_{m } · (m ⊗^{M }_{l } δ_{m }) · (m ⊗^{M }_{l } (δ_{m } ⊗^{M }_{r } m )).
  Show proof.

    refine (_ @ commutative_symmetric_braiding_using_lrwhisker' _).
    apply maponpaths_2.
    refine (_ @ commutative_symmetric_braiding_using_lrwhisker _).
    apply maponpaths_2.
    exact (commutative_symmetric_braiding_using_lwhisker _).

  Lemma comultiplication_comonoid_4times
    (m : commutative_comonoid M)
    : δ_{m } · m ⊗^{M }_{l } δ_{ m } · m ⊗^{M }_{l } (δ_{ m } ⊗^{M }_{r } m )
      = δ_{m } · δ_{m } ⊗^{M } δ_{ m } · mon_lassociator _ _ (_ ⊗ m) · m ⊗^{M }_{l } mon_rassociator _ _ _.
  Show proof.

    etrans.
    2: {
      apply maponpaths_2.
      exact (! commutative_symmetric_braiding_using_lwhisker _).
    }

    rewrite ! assoc'.
    apply maponpaths.
    rewrite <- (bifunctor_leftcomp M).
    etrans. {
      apply pathsinv0, (bifunctor_leftcomp M).
    }
    etrans.
    2: {
      apply (bifunctor_leftcomp M).
    }
    apply maponpaths.
    refine (comonoid_laws_assoc' M m @ _).
    apply assoc'.

  Lemma commutative_symmetric_braiding_after_4_copies'
    (m : commutative_comonoid M)
    : δ_{m } · δ_{m } #⊗ δ_{m } · α ^{M }_{_,_,_} · (m ⊗^{M }_{l } αinv ^{M }_{_,_,_}) · (m ⊗^{M }_{l } (sym_mon_braiding M m m ⊗^{M }_{r } m ))
      = δ_{m } · δ_{m } #⊗ δ_{m } · α ^{M }_{_,_,_} · m ⊗^{M }_{l } αinv ^{M }_{_,_,_}.
  Show proof.

refine (commutative_symmetric_braiding_using_lrwhisker'' _ @ _).
exact (comultiplication_comonoid_4times _).

  Lemma commutative_symmetric_braiding_after_4_copies
    (m : commutative_comonoid M)
    : δ_{m } · (δ_{m } #⊗ δ_{m }
                 · (α ^{M }_{ m , m , m ⊗_{ M } m }
                         · (m ⊗^{M }_{l } (αinv ^{M }_{ m , m , m } · (sym_mon_braiding M m m ⊗^{M }_{r } m · α ^{M }_{ m , m , m }))
                              · αinv ^{M }_{m , m , m ⊗_{ M } m })))
      = δ_{m } · δ_{m } #⊗ δ_{m }.
  Show proof.

    rewrite ! assoc.
    etrans. {
      apply maponpaths_2.
      rewrite ! (bifunctor_leftcomp M).
      rewrite ! assoc.
      apply maponpaths_2.
      exact (commutative_symmetric_braiding_after_4_copies' _).
    }

    etrans. {
      apply maponpaths_2.
      rewrite assoc'.
      apply maponpaths.
      rewrite <- (bifunctor_leftcomp M).
      apply maponpaths.
      apply (monoidal_associatorisolaw M m m m).
    }
    rewrite (bifunctor_leftid M).
    rewrite id_right.

    etrans. {
      rewrite assoc'.
      apply maponpaths.
      apply (monoidal_associatorisolaw M m m _).
    }
    apply id_right.

  Lemma comult_before_inner_swap_and_swap
    (mx my : comonoid M)
    : δ_{mx } #⊗ δ_{my } · (inner_swap M _ _ _ _ · sym_mon_braiding M _ _ #⊗ sym_mon_braiding M _ _)
      = δ_{mx } #⊗ δ_{my } · (sym_mon_braiding M (_ ⊗ _) (_ ⊗ _) · inner_swap M _ _ _ _).
  Show proof.

apply maponpaths.
apply inner_swap_commute_with_swap.

End CommutativeComonoids.

Section Univalence.

  Lemma disp_cat_of_comonoids_is_univalent
    (V : monoidal_cat)
    : is_univalent_disp (disp_cat_of_comonoids V).
  Show proof.

    apply is_univalent_sigma_disp.
    - apply dirprod_disp_cat_is_univalent
      ; apply is_univalent_dialgebra_disp_cat.
    - apply disp_full_sub_univalent.
      intro ; apply isaprop_comonoid_laws.

  Lemma disp_cat_of_commutative_comonoids_is_univalent
    (V : sym_monoidal_cat)
    : is_univalent_disp (disp_cat_of_commutative_comonoids V).
  Show proof.

    apply is_univalent_sigma_disp.
    - apply disp_cat_of_comonoids_is_univalent.
    - apply disp_full_sub_univalent.
      intro ; apply homset_property.

End Univalence.