MonoidObject.v

Require Import Basics.Overture Basics.Tactics.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor
  WildCat.NatTrans WildCat.Opposite WildCat.Products.
Require Import abstract_algebra.

(** * Monoids and Comonoids *)

(** Here we define a monoid internal to a monoidal category. Note that we don't actually need the full monoidal structure so we assume only the parts we need. This allows us to keep the definitions general between various flavours of monoidal category.

Many algebraic theories such as groups and rings may also be internalized, however these specifically require a cartesian monoidal structure. The theory of monoids however has no such requirement and can therefore be developed in much greater generality. This can be used to define a range of objects such as R-algebras, H-spaces, Hopf algebras and more. *)

(** * Monoid objects *)

Section MonoidObject.
  Context {A : Type} (tensor : A -> A -> A) {unit : A}
    `{HasEquivs A, !Is0Bifunctor tensor, !Is1Bifunctor tensor}
    `{!Associator tensor, !LeftUnitor tensor unit, !RightUnitor tensor unit}.

  (** An object [x] of [A] is a monoid object if it comes with the following data: *)
  Class IsMonoidObject (x : A) := {
    (** A multiplication map from the tensor product of [x] with itself to [x]. *)
    mo_mult : tensor x x $-> x;
    (** A unit of the multiplication. *)
    mo_unit : unit $-> x;
    (** The multiplication map is associative. *)
    mo_assoc : mo_mult $o fmap10 tensor mo_mult x $o associator x x x
        $== mo_mult $o fmap01 tensor x mo_mult;
    (** The multiplication map is left unital. *)
    mo_left_unit : mo_mult $o fmap10 tensor mo_unit x $== left_unitor x;
    (** The multiplication map is right unital. *)
    mo_right_unit : mo_mult $o fmap01 tensor x mo_unit $== right_unitor x;
  }.

  Context `{!Braiding tensor}.

  (** An object [x] of [A] is a commutative monoid object if: *)
  Class IsCommutativeMonoidObject (x : A) := {
    (** It is a monoid object. *)
    cmo_mo :: IsMonoidObject x;
    (** The multiplication map is commutative. *)
    cmo_comm : mo_mult $o braid x x $== mo_mult;
  }.

End MonoidObject.

Arguments IsMonoidObject {A} tensor unit {_ _ _ _ _ _ _ _ _ _} x.
Arguments IsCommutativeMonoidObject {A} tensor unit {_ _ _ _ _ _ _ _ _ _ _} x.

Section ComonoidObject.
  Context {A : Type} (tensor : A -> A -> A) (unit : A)
    `{HasEquivs A, !Is0Bifunctor tensor, !Is1Bifunctor tensor}
    `{!Associator tensor, !LeftUnitor tensor unit, !RightUnitor tensor unit}.

  (** A comonoid object is a monoid object in the opposite category. *)
  Class IsComonoidObject (x : A)
    := ismonoid_comonoid_op :: IsMonoidObject (A:=A^op) tensor unit x.

  (** We can build comonoid objects from the following data: *)
  Definition Build_IsComonoidObject (x : A)
    (** A comultiplication map. *)
    (co_comult : x $-> tensor x x)
    (** A counit. *)
    (co_counit : x $-> unit)
    (** The comultiplication is coassociative. *)
    (co_coassoc : associator x x x $o fmap01 tensor x co_comult $o co_comult
        $== fmap10 tensor co_comult x $o co_comult)
    (** The comultiplication is left counital. *)
    (co_left_counit : left_unitor x $o fmap10 tensor co_counit x $o co_comult $== Id x)
    (** The comultiplication is right counital. *)
    (co_right_counit : right_unitor x $o fmap01 tensor x co_counit $o co_comult $== Id x)
    : IsComonoidObject x.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
IsComonoidObject x
  Proof.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
IsComonoidObject x
    snapply Build_IsMonoidObject.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
tensor x x $-> x
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
unit $-> x
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
?mo_mult $o fmap10 tensor ?mo_mult x $o
associator_op x x x $==
?mo_mult $o fmap01 tensor x ?mo_mult
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
?mo_mult $o fmap10 tensor ?mo_unit x $==
left_unitor_op unit x
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
?mo_mult $o fmap01 tensor x ?mo_unit $==
right_unitor_op unit x
    -A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
tensor x x $-> x exact co_comult.
    -A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
unit $-> x exact co_counit.
    -A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
co_comult $o fmap10 tensor co_comult x $o
associator_op x x x $==
co_comult $o fmap01 tensor x co_comult napply cate_moveR_eV.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
co_comult $o fmap10 tensor co_comult x $==
co_comult $o fmap01 tensor x co_comult $o
Associator0 (x, x, x)
      symmetry.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
co_comult $o fmap01 tensor x co_comult $o
Associator0 (x, x, x) $==
co_comult $o fmap10 tensor co_comult x
      nrefine (cat_assoc _ _ _ $@ _).A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
co_comult $o
(fmap01 tensor x co_comult $o Associator0 (x, x, x)) $==
co_comult $o fmap10 tensor co_comult x
      rapply co_coassoc.
    -A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
co_comult $o fmap10 tensor co_counit x $==
left_unitor_op unit x simpl; nrefine (_ $@ cat_idr _).A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
fmap10 tensor co_counit x $o co_comult $==
cate_fun' x (tensor unit x)
  (cate_buildequiv' x (tensor unit x)
     (cate_inv' (tensor unit x) x (LeftUnitor0 x))
     (catie_adjointify
        (cate_inv' (tensor unit x) x (LeftUnitor0 x))
        (cate_fun' (tensor unit x) x (LeftUnitor0 x))
        (cate_issect' (tensor unit x) x
           (LeftUnitor0 x))
        (cate_isretr' (tensor unit x) x
           (LeftUnitor0 x)))) $o Id x
      napply cate_moveL_Ve.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
LeftUnitor0 x $o
(fmap10 tensor co_counit x $o co_comult) $== Id x
      nrefine (cat_assoc_opp _ _ _ $@ _).A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
LeftUnitor0 x $o fmap10 tensor co_counit x $o
co_comult $== Id x
      exact co_left_counit.
    -A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
co_comult $o fmap01 tensor x co_counit $==
right_unitor_op unit x simpl; nrefine (_ $@ cat_idr _).A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
fmap01 tensor x co_counit $o co_comult $==
cate_fun' x (tensor x unit)
  (cate_buildequiv' x (tensor x unit)
     (cate_inv' (tensor x unit) x (RightUnitor0 x))
     (catie_adjointify
        (cate_inv' (tensor x unit) x (RightUnitor0 x))
        (cate_fun' (tensor x unit) x (RightUnitor0 x))
        (cate_issect' (tensor x unit) x
           (RightUnitor0 x))
        (cate_isretr' (tensor x unit) x
           (RightUnitor0 x)))) $o Id x
      napply cate_moveL_Ve.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
RightUnitor0 x $o
(fmap01 tensor x co_counit $o co_comult) $== Id x
      nrefine (cat_assoc_opp _ _ _ $@ _).A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
co_comult: x $-> tensor x x
co_counit: x $-> unit
co_coassoc: Associator0 x x x $o
fmap01 tensor x co_comult $o co_comult $==
fmap10 tensor co_comult x $o co_comult
co_left_counit: LeftUnitor0 x $o
fmap10 tensor co_counit x $o
co_comult $== Id x
co_right_counit: RightUnitor0 x $o
fmap01 tensor x co_counit $o
co_comult $== Id x
RightUnitor0 x $o fmap01 tensor x co_counit $o
co_comult $== Id x
      exact co_right_counit.
  Defined.

  (** Comultiplication *)
  Definition co_comult {x : A} `{!IsComonoidObject x} : x $-> tensor x x
   := mo_mult (A:=A^op) tensor (unit:=unit) (x:=x).

  (** Counit *)
  Definition co_counit {x : A} `{!IsComonoidObject x} : x $-> unit
    := mo_unit (A:=A^op) tensor (unit:=unit) (x:=x).

  (** Coassociativity *)
  Definition co_coassoc {x : A} `{!IsComonoidObject x}
    : associator x x x $o fmap01 tensor x co_comult $o co_comult
        $== fmap10 tensor co_comult x $o co_comult.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
IsComonoidObject0: IsComonoidObject x
Associator0 x x x $o fmap01 tensor x co_comult $o
co_comult $== fmap10 tensor co_comult x $o co_comult
  Proof.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
IsComonoidObject0: IsComonoidObject x
Associator0 x x x $o fmap01 tensor x co_comult $o
co_comult $== fmap10 tensor co_comult x $o co_comult
    refine (cat_assoc _ _ _ $@ _).A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
IsComonoidObject0: IsComonoidObject x
Associator0 x x x $o
(fmap01 tensor x co_comult $o co_comult) $==
fmap10 tensor co_comult x $o co_comult
    apply cate_moveR_Me.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
IsComonoidObject0: IsComonoidObject x
fmap01 tensor x co_comult $o co_comult $==
(Associator0 x x x)^-1$ $o
(fmap10 tensor co_comult x $o co_comult)
    symmetry.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
IsComonoidObject0: IsComonoidObject x
(Associator0 x x x)^-1$ $o
(fmap10 tensor co_comult x $o co_comult) $==
fmap01 tensor x co_comult $o co_comult
    exact (mo_assoc (A:=A^op) tensor (unit:=unit) (x:=x)).
  Defined.

  (** Left counitality *)
  Definition co_left_counit {x : A} `{!IsComonoidObject x}
    : left_unitor x $o fmap10 tensor co_counit x $o co_comult $== Id x.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
IsComonoidObject0: IsComonoidObject x
LeftUnitor0 x $o fmap10 tensor co_counit x $o
co_comult $== Id x
  Proof.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
IsComonoidObject0: IsComonoidObject x
LeftUnitor0 x $o fmap10 tensor co_counit x $o
co_comult $== Id x
    refine (cat_assoc _ _ _ $@ _).A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
IsComonoidObject0: IsComonoidObject x
LeftUnitor0 x $o
(fmap10 tensor co_counit x $o co_comult) $== Id x
    apply cate_moveR_Me.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
IsComonoidObject0: IsComonoidObject x
fmap10 tensor co_counit x $o co_comult $==
(LeftUnitor0 x)^-1$ $o Id x
    refine (_ $@ (cat_idr _)^$).A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
IsComonoidObject0: IsComonoidObject x
fmap10 tensor co_counit x $o co_comult $==
(LeftUnitor0 x)^-1$
    exact (mo_left_unit (A:=A^op) tensor (unit:=unit) (x:=x)).
  Defined.

  (** Right counitality *)
  Definition co_right_counit {x : A} `{!IsComonoidObject x}
    : right_unitor x $o fmap01 tensor x co_counit $o co_comult $== Id x.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
IsComonoidObject0: IsComonoidObject x
RightUnitor0 x $o fmap01 tensor x co_counit $o
co_comult $== Id x
  Proof.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
IsComonoidObject0: IsComonoidObject x
RightUnitor0 x $o fmap01 tensor x co_counit $o
co_comult $== Id x
    refine (cat_assoc _ _ _ $@ _).A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
IsComonoidObject0: IsComonoidObject x
RightUnitor0 x $o
(fmap01 tensor x co_counit $o co_comult) $== Id x
    apply cate_moveR_Me.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
IsComonoidObject0: IsComonoidObject x
fmap01 tensor x co_counit $o co_comult $==
(RightUnitor0 x)^-1$ $o Id x
    refine (_ $@ (cat_idr _)^$).A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
IsComonoidObject0: IsComonoidObject x
fmap01 tensor x co_counit $o co_comult $==
(RightUnitor0 x)^-1$
    exact (mo_right_unit (A:=A^op) tensor (unit:=unit) (x:=x)).
  Defined.

  Context `{!Braiding tensor}.

  (** A cocommutative comonoid objects is a commutative monoid object in the opposite category. *)
  Class IsCocommutativeComonoidObject (x : A)
    := iscommuatativemonoid_cocomutativemonoid_op
      :: IsCommutativeMonoidObject (A:=A^op) tensor unit x.

  (** We can build cocommutative comonoid objects from the following data: *)
  Definition Build_IsCocommutativeComonoidObject (x : A)
    (** A comonoid. *)
    `{!IsComonoidObject x}
    (** Together with a proof of cocommutativity. *)
    (cco_cocomm : braid x x $o co_comult $== co_comult)
    : IsCocommutativeComonoidObject x.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
IsComonoidObject0: IsComonoidObject x
cco_cocomm: Braiding0 x x $o co_comult $== co_comult
IsCocommutativeComonoidObject x
  Proof.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
IsComonoidObject0: IsComonoidObject x
cco_cocomm: Braiding0 x x $o co_comult $== co_comult
IsCocommutativeComonoidObject x
    snapply Build_IsCommutativeMonoidObject.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
IsComonoidObject0: IsComonoidObject x
cco_cocomm: Braiding0 x x $o co_comult $== co_comult
IsMonoidObject tensor unit x
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
IsComonoidObject0: IsComonoidObject x
cco_cocomm: Braiding0 x x $o co_comult $== co_comult
mo_mult tensor $o braiding_op x x $== mo_mult tensor
    -A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
IsComonoidObject0: IsComonoidObject x
cco_cocomm: Braiding0 x x $o co_comult $== co_comult
IsMonoidObject tensor unit x exact _.
    -A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
IsComonoidObject0: IsComonoidObject x
cco_cocomm: Braiding0 x x $o co_comult $== co_comult
mo_mult tensor $o braiding_op x x $== mo_mult tensor exact cco_cocomm.
  Defined.

  #[export] Instance co_cco {x : A} `{!IsCocommutativeComonoidObject x}
    : IsComonoidObject x.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
IsCocommutativeComonoidObject0: IsCocommutativeComonoidObject
  x
IsComonoidObject x
  Proof.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
IsCocommutativeComonoidObject0: IsCocommutativeComonoidObject
  x
IsComonoidObject x
    srapply cmo_mo.
  Defined.

  (** Cocommutativity *)
  Definition cco_cocomm {x : A} `{!IsCocommutativeComonoidObject x}
    : braid x x $o co_comult $== co_comult.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
IsCocommutativeComonoidObject0: IsCocommutativeComonoidObject
  x
Braiding0 x x $o co_comult $== co_comult
  Proof.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
IsCocommutativeComonoidObject0: IsCocommutativeComonoidObject
  x
Braiding0 x x $o co_comult $== co_comult
    exact (cmo_comm (A:=A^op) tensor (unit:=unit) (x:=x)).
  Defined.

End ComonoidObject.

(** A comonoid object in [A^op] is a monoid object in [A]. *)
Definition mo_co_op {A : Type} {tensor : A -> A -> A} {unit : A}
  `{HasEquivs A, !Is0Bifunctor tensor, !Is1Bifunctor tensor}
  `{!Associator tensor, !LeftUnitor tensor unit, !RightUnitor tensor unit}
  {x : A} `{C : !IsComonoidObject (A:=A^op) tensor unit x}
  : IsMonoidObject tensor unit x.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
IsMonoidObject tensor unit x
Proof.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
IsMonoidObject tensor unit x
  snapply Build_IsMonoidObject.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
tensor x x $-> x
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
unit $-> x
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
?mo_mult $o fmap10 tensor ?mo_mult x $o
Associator0 x x x $==
?mo_mult $o fmap01 tensor x ?mo_mult
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
?mo_mult $o fmap10 tensor ?mo_unit x $== LeftUnitor0 x
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
?mo_mult $o fmap01 tensor x ?mo_unit $==
RightUnitor0 x
  -A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
tensor x x $-> x exact (co_comult (A:=A^op) tensor unit).
  -A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
unit $-> x exact (co_counit (A:=A^op) tensor unit).
  -A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
co_comult tensor unit $o
fmap10 tensor (co_comult tensor unit) x $o
Associator0 x x x $==
co_comult tensor unit $o
fmap01 tensor x (co_comult tensor unit) apply cate_moveR_eM.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
co_comult tensor unit $o
fmap10 tensor (co_comult tensor unit) x $==
co_comult tensor unit $o
fmap01 tensor x (co_comult tensor unit) $o
(Associator0 x x x)^-1$
    symmetry.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
co_comult tensor unit $o
fmap01 tensor x (co_comult tensor unit) $o
(Associator0 x x x)^-1$ $==
co_comult tensor unit $o
fmap10 tensor (co_comult tensor unit) x
    exact (cat_assoc _ _ _ $@ co_coassoc (A:=A^op) tensor unit (x:=x)).
  -A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
co_comult tensor unit $o
fmap10 tensor (co_counit tensor unit) x $==
LeftUnitor0 x simpl; nrefine (_ $@ cat_idl _).A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
co_comult tensor unit $o
fmap10 tensor (co_counit tensor unit) x $==
Id x $o LeftUnitor0 x
    apply cate_moveL_eM.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
co_comult tensor unit $o
fmap10 tensor (co_counit tensor unit) x $o
(LeftUnitor0 x)^-1$ $== Id x
    refine (cat_assoc _ _ _ $@ _).A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
co_comult tensor unit $o
(fmap10 tensor (co_counit tensor unit) x $o
 (LeftUnitor0 x)^-1$) $== Id x
    exact (co_left_counit (A:=A^op) tensor unit (x:=x)).
  -A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
co_comult tensor unit $o
fmap01 tensor x (co_counit tensor unit) $==
RightUnitor0 x simpl; nrefine (_ $@ cat_idl _).A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
co_comult tensor unit $o
fmap01 tensor x (co_counit tensor unit) $==
Id x $o RightUnitor0 x
    apply cate_moveL_eM.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
co_comult tensor unit $o
fmap01 tensor x (co_counit tensor unit) $o
(RightUnitor0 x)^-1$ $== Id x
    refine (cat_assoc _ _ _ $@ _).A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
x: A
C: IsComonoidObject tensor unit x
co_comult tensor unit $o
(fmap01 tensor x (co_counit tensor unit) $o
 (RightUnitor0 x)^-1$) $== Id x
    exact (co_right_counit (A:=A^op) tensor unit (x:=x)).
Defined.

(** A cocommutative comonoid object in [A^op] is a commutative monoid object in [A]. *)
Definition cmo_coco_op {A : Type} {tensor : A -> A -> A} {unit : A}
  `{HasEquivs A, !Is0Bifunctor tensor, !Is1Bifunctor tensor}
  `{!Associator tensor, !LeftUnitor tensor unit, !RightUnitor tensor unit,
    !Braiding tensor}
  {x : A} `{C : !IsCocommutativeComonoidObject (A:=A^op) tensor unit x}
  : IsCommutativeMonoidObject tensor unit x.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
C: IsCocommutativeComonoidObject tensor unit x
IsCommutativeMonoidObject tensor unit x
Proof.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
C: IsCocommutativeComonoidObject tensor unit x
IsCommutativeMonoidObject tensor unit x
  snapply Build_IsCommutativeMonoidObject.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
C: IsCocommutativeComonoidObject tensor unit x
IsMonoidObject tensor unit x
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
C: IsCocommutativeComonoidObject tensor unit x
mo_mult tensor $o Braiding0 x x $== mo_mult tensor
  -A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
C: IsCocommutativeComonoidObject tensor unit x
IsMonoidObject tensor unit x napply mo_co_op.A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
C: IsCocommutativeComonoidObject tensor unit x
IsComonoidObject tensor unit x
    rapply co_cco.
  -A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is0Bifunctor0: Is0Bifunctor tensor
Is1Bifunctor0: Is1Bifunctor tensor
Associator0: Associator tensor
LeftUnitor0: LeftUnitor tensor unit
RightUnitor0: RightUnitor tensor unit
Braiding0: Braiding tensor
x: A
C: IsCocommutativeComonoidObject tensor unit x
mo_mult tensor $o Braiding0 x x $== mo_mult tensor exact (cco_cocomm (A:=A^op) tensor unit).
Defined.

(** ** Monoid enrichment *)

(** A hom [x $-> y] in a cartesian category where [y] is a monoid object has the structure of a monoid. Equivalently, a hom [x $-> y] in a cartesian category where [x] is a comonoid object has the structure of a monoid. *)

Section MonoidEnriched.
  Context {A : Type} `{HasEquivs A} `{!HasBinaryProducts A}
    (I : A) `{!IsTerminal I} {x y : A}
    `{!HasMorExt A} `{forall x y : A, IsHSet (x $-> y)}.

  Section Monoid.

    Context `{!IsMonoidObject cat_binprod I y}.

    Local Instance sgop_hom : SgOp (x $-> y)
      := fun f g => mo_mult cat_binprod $o cat_binprod_corec f g.

    Local Instance monunit_hom : MonUnit (x $-> y) := mo_unit cat_binprod $o mor_terminal _ _.

    Local Instance associative_hom : Associative sgop_hom.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
Associative sgop_hom
    Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
Associative sgop_hom
      intros f g h.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f, g, h: x $-> y
sgop_hom f (sgop_hom g h) = sgop_hom (sgop_hom f g) h
      unfold sgop_hom.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f, g, h: x $-> y
mo_mult cat_binprod $o
cat_binprod_corec f
  (mo_mult cat_binprod $o cat_binprod_corec g h) =
mo_mult cat_binprod $o
cat_binprod_corec
  (mo_mult cat_binprod $o cat_binprod_corec f g) h
      rapply path_hom.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f, g, h: x $-> y
mo_mult cat_binprod $o
cat_binprod_corec f
  (mo_mult cat_binprod $o cat_binprod_corec g h) $==
mo_mult cat_binprod $o
cat_binprod_corec
  (mo_mult cat_binprod $o cat_binprod_corec f g) h
      refine ((_ $@L cat_binprod_fmap01_corec _ _ _)^$ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f, g, h: x $-> y
mo_mult cat_binprod $o
(fmap01 (fun x y : A => cat_binprod x y) y
   (mo_mult cat_binprod) $o
 cat_binprod_corec f (cat_binprod_corec g h)) $==
mo_mult cat_binprod $o
cat_binprod_corec
  (mo_mult cat_binprod $o cat_binprod_corec f g) h
      nrefine (cat_assoc_opp _ _ _ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f, g, h: x $-> y
mo_mult cat_binprod $o
fmap01 (fun x y : A => cat_binprod x y) y
  (mo_mult cat_binprod) $o
cat_binprod_corec f (cat_binprod_corec g h) $==
mo_mult cat_binprod $o
cat_binprod_corec
  (mo_mult cat_binprod $o cat_binprod_corec f g) h
      refine ((mo_assoc cat_binprod $@R _)^$ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f, g, h: x $-> y
mo_mult cat_binprod $o
fmap10 cat_binprod (mo_mult cat_binprod) y $o
cat_tensor_associator y y y $o
cat_binprod_corec f (cat_binprod_corec g h) $==
mo_mult cat_binprod $o
cat_binprod_corec
  (mo_mult cat_binprod $o cat_binprod_corec f g) h
      nrefine (_ $@ (_ $@L cat_binprod_fmap10_corec _ _ _)).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f, g, h: x $-> y
mo_mult cat_binprod $o
fmap10 cat_binprod (mo_mult cat_binprod) y $o
cat_tensor_associator y y y $o
cat_binprod_corec f (cat_binprod_corec g h) $==
mo_mult cat_binprod $o
(fmap10 (fun x y : A => cat_binprod x y)
   (mo_mult cat_binprod) y $o
 cat_binprod_corec (cat_binprod_corec f g) h)
      refine (cat_assoc _ _ _ $@ (_ $@L _) $@ cat_assoc _ _ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f, g, h: x $-> y
cat_tensor_associator y y y $o
cat_binprod_corec f (cat_binprod_corec g h) $==
cat_binprod_corec (cat_binprod_corec f g) h
      napply cat_binprod_associator_corec.
    Defined.

    Local Instance leftidentity_hom : LeftIdentity sgop_hom mon_unit.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
LeftIdentity sgop_hom mon_unit
    Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
LeftIdentity sgop_hom mon_unit
      intros f.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
sgop_hom mon_unit f = f
      unfold sgop_hom, mon_unit.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
mo_mult cat_binprod $o cat_binprod_corec monunit_hom f =
f
      rapply path_hom.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
mo_mult cat_binprod $o cat_binprod_corec monunit_hom f $==
f
      refine ((_ $@L (cat_binprod_fmap10_corec _ _ _)^$) $@ cat_assoc_opp _ _ _ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
mo_mult cat_binprod $o
fmap10 (fun x y : A => cat_binprod x y)
  (mo_unit cat_binprod) y $o
cat_binprod_corec (mor_terminal x I) f $== f
      nrefine (((mo_left_unit cat_binprod $@ _) $@R _) $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
cat_tensor_left_unitor y $== ?Goal
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
?Goal $o cat_binprod_corec (mor_terminal x I) f $== f
      1: napply cate_buildequiv_fun.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
{|
  trans_nattrans :=
    fun a : A =>
    right_unitor_binprod I a $o
    symmetricbraiding_binprod I a;
  is1natural_nattrans :=
    Build_Is1Natural
      (fun a : A =>
       right_unitor_binprod I a $o
       symmetricbraiding_binprod I a)
      (fun (a b : A) (f : a $-> b) =>
       Square.vconcat (braid_nat_r f)
         (is1natural_natequiv (right_unitor_binprod I)
            a b f))
|} y $o cat_binprod_corec (mor_terminal x I) f $== f
      unfold trans_nattrans.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
right_unitor_binprod I y $o
symmetricbraiding_binprod I y $o
cat_binprod_corec (mor_terminal x I) f $== f
      nrefine ((((_ $@R _) $@ _) $@R _) $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
right_unitor_binprod I y $== ?Goal0
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
?Goal0 $o symmetricbraiding_binprod I y $== ?Goal
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
?Goal $o cat_binprod_corec (mor_terminal x I) f $== f
      1: napply cate_buildequiv_fun.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
cat_pr1 $o symmetricbraiding_binprod I y $== ?Goal
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
?Goal $o cat_binprod_corec (mor_terminal x I) f $== f
      1: napply cat_binprod_beta_pr1.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
cat_pr2 $o cat_binprod_corec (mor_terminal x I) f $==
f
      napply cat_binprod_beta_pr2.
    Defined.

    Local Instance rightidentity_hom : RightIdentity sgop_hom mon_unit.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
RightIdentity sgop_hom mon_unit
    Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
RightIdentity sgop_hom mon_unit
      intros f.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
sgop_hom f mon_unit = f
      unfold sgop_hom, mon_unit.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
mo_mult cat_binprod $o cat_binprod_corec f monunit_hom =
f
      rapply path_hom.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
mo_mult cat_binprod $o cat_binprod_corec f monunit_hom $==
f
      refine ((_ $@L (cat_binprod_fmap01_corec _ _ _)^$) $@ cat_assoc_opp _ _ _ $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
mo_mult cat_binprod $o
fmap01 (fun x y : A => cat_binprod x y) y
  (mo_unit cat_binprod) $o
cat_binprod_corec f (mor_terminal x I) $== f
      nrefine (((mo_right_unit cat_binprod $@ _) $@R _) $@ _).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
cat_tensor_right_unitor y $== ?Goal
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
?Goal $o cat_binprod_corec f (mor_terminal x I) $== f
      1: napply cate_buildequiv_fun.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsMonoidObject0: IsMonoidObject cat_binprod I y
f: x $-> y
cat_pr1 $o cat_binprod_corec f (mor_terminal x I) $==
f
      napply cat_binprod_beta_pr1.
    Defined.

    Local Instance issemigroup_hom : IsSemiGroup (x $-> y) := {}.
    Local Instance ismonoid_hom : IsMonoid (x $-> y) := {}.

  End Monoid.

  Context `{!IsCommutativeMonoidObject cat_binprod I y}.
  Local Existing Instances sgop_hom monunit_hom ismonoid_hom.

  Local Instance commutative_hom : Commutative sgop_hom.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsCommutativeMonoidObject0: IsCommutativeMonoidObject
  cat_binprod I y
Commutative sgop_hom
  Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsCommutativeMonoidObject0: IsCommutativeMonoidObject
  cat_binprod I y
Commutative sgop_hom
    intros f g.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsCommutativeMonoidObject0: IsCommutativeMonoidObject
  cat_binprod I y
f, g: x $-> y
sgop_hom f g = sgop_hom g f
    unfold sgop_hom.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsCommutativeMonoidObject0: IsCommutativeMonoidObject
  cat_binprod I y
f, g: x $-> y
mo_mult cat_binprod $o cat_binprod_corec f g =
mo_mult cat_binprod $o cat_binprod_corec g f
    rapply path_hom.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsCommutativeMonoidObject0: IsCommutativeMonoidObject
  cat_binprod I y
f, g: x $-> y
mo_mult cat_binprod $o cat_binprod_corec f g $==
mo_mult cat_binprod $o cat_binprod_corec g f
    refine ((_ $@L _^$) $@ cat_assoc_opp _ _ _ $@ (cmo_comm cat_binprod $@R _)).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasBinaryProducts0: HasBinaryProducts A
I: A
IsTerminal0: IsTerminal I
x, y: A
HasMorExt0: HasMorExt A
H1: forall x y : A, IsHSet (x $-> y)
IsCommutativeMonoidObject0: IsCommutativeMonoidObject
  cat_binprod I y
f, g: x $-> y
cat_symm_tensor_braiding y y $o cat_binprod_corec g f $->
cat_binprod_corec f g
    napply cat_binprod_swap_corec. 
  Defined.

  Local Instance iscommutativemonoid_hom : IsCommutativeMonoid (x $-> y) := {}.

End MonoidEnriched.

(** ** Preservation of monoid objects by lax monoidal functors *)

Definition mo_preserved {A B : Type}
  {tensorA : A -> A -> A} {tensorB : B -> B -> B} {IA : A} {IB : B} 
  (F : A -> B) `{IsMonoidalFunctor A B tensorA tensorB IA IB F} (x : A)
  : IsMonoidObject tensorA IA x -> IsMonoidObject tensorB IB (F x).A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
IsMonoidObject tensorA IA x ->
IsMonoidObject tensorB IB (F x)
Proof.A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
IsMonoidObject tensorA IA x ->
IsMonoidObject tensorB IB (F x)
  intros mo_x.A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
IsMonoidObject tensorB IB (F x)
  snapply Build_IsMonoidObject.A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
tensorB (F x) (F x) $-> F x
A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
IB $-> F x
A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
?mo_mult $o fmap10 tensorB ?mo_mult (F x) $o
cat_tensor_associator (F x) (F x) (F x) $==
?mo_mult $o fmap01 tensorB (F x) ?mo_mult
A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
?mo_mult $o fmap10 tensorB ?mo_unit (F x) $==
cat_tensor_left_unitor (F x)
A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
?mo_mult $o fmap01 tensorB (F x) ?mo_unit $==
cat_tensor_right_unitor (F x)
  -A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
tensorB (F x) (F x) $-> F x exact (fmap F (mo_mult tensorA) $o fmap_tensor F (x, x)).
  -A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
IB $-> F x exact (fmap F (mo_unit tensorA) $o fmap_unit).
  -A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap F (mo_mult tensorA) $o fmap_tensor F (x, x) $o
fmap10 tensorB
  (fmap F (mo_mult tensorA) $o fmap_tensor F (x, x))
  (F x) $o cat_tensor_associator (F x) (F x) (F x) $==
fmap F (mo_mult tensorA) $o fmap_tensor F (x, x) $o
fmap01 tensorB (F x)
  (fmap F (mo_mult tensorA) $o fmap_tensor F (x, x)) refine (((_ $@L (fmap10_comp tensorB _ _ _)) $@R _)
      $@ _ $@ (_ $@L (fmap01_comp tensorB _ _ _)^$)).A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap F (mo_mult tensorA) $o fmap_tensor F (x, x) $o
(fmap10 tensorB (fmap F (mo_mult tensorA)) (F x) $o
 fmap10 tensorB (fmap_tensor F (x, x)) (F x)) $o
cat_tensor_associator (F x) (F x) (F x) $==
fmap F (mo_mult tensorA) $o fmap_tensor F (x, x) $o
(fmap01 tensorB (F x) (fmap F (mo_mult tensorA)) $o
 fmap01 tensorB (F x) (fmap_tensor F (x, x)))
    refine (_ $@ (((_ $@L _^$) $@ cat_assoc_opp _ _ _) $@R _)
      $@ cat_assoc _ _ _).A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap F (mo_mult tensorA) $o fmap_tensor F (x, x) $o
(fmap10 tensorB (fmap F (mo_mult tensorA)) (F x) $o
 fmap10 tensorB (fmap_tensor F (x, x)) (F x)) $o
cat_tensor_associator (F x) (F x) (F x) $==
fmap F (mo_mult tensorA) $o ?Goal0 $o
fmap01 tensorB (F x) (fmap_tensor F (x, x))
A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap_tensor F (x, x) $o
fmap01 tensorB (F x) (fmap F (mo_mult tensorA)) $->
?Goal0
    2: snapply fmap_tensor_nat_r.A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap F (mo_mult tensorA) $o fmap_tensor F (x, x) $o
(fmap10 tensorB (fmap F (mo_mult tensorA)) (F x) $o
 fmap10 tensorB (fmap_tensor F (x, x)) (F x)) $o
cat_tensor_associator (F x) (F x) (F x) $==
fmap F (mo_mult tensorA) $o
(fmap F (fmap01 tensorA x (mo_mult tensorA)) $o
 fmap_tensor F (x, tensorA x x)) $o
fmap01 tensorB (F x) (fmap_tensor F (x, x))
    refine (_ $@ ((fmap2 _ (mo_assoc _) $@ fmap_comp _ _ _) $@R _)
      $@ cat_assoc_opp _ _ _ $@ (cat_assoc _ _ _ $@R _)).A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap F (mo_mult tensorA) $o fmap_tensor F (x, x) $o
(fmap10 tensorB (fmap F (mo_mult tensorA)) (F x) $o
 fmap10 tensorB (fmap_tensor F (x, x)) (F x)) $o
cat_tensor_associator (F x) (F x) (F x) $==
fmap F
  (mo_mult tensorA $o
   fmap10 tensorA (mo_mult tensorA) x $o
   cat_tensor_associator x x x) $o
(fmap_tensor F (x, tensorA x x) $o
 fmap01 tensorB (F x) (fmap_tensor F (x, x)))
    refine (_ $@ ((fmap_comp _ _ _ $@ (fmap_comp _ _ _ $@R _))^$ $@R _)).A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap F (mo_mult tensorA) $o fmap_tensor F (x, x) $o
(fmap10 tensorB (fmap F (mo_mult tensorA)) (F x) $o
 fmap10 tensorB (fmap_tensor F (x, x)) (F x)) $o
cat_tensor_associator (F x) (F x) (F x) $==
fmap F (mo_mult tensorA) $o
fmap F (fmap10 tensorA (mo_mult tensorA) x) $o
fmap F (cat_tensor_associator x x x) $o
(fmap_tensor F (x, tensorA x x) $o
 fmap01 tensorB (F x) (fmap_tensor F (x, x)))
    nrefine (cat_assoc _ _ _ $@ cat_assoc _ _ _ $@ (_ $@L _)
      $@ cat_assoc_opp _ _ _ $@ cat_assoc_opp _ _ _).A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap_tensor F (x, x) $o
(fmap10 tensorB (fmap F (mo_mult tensorA)) (F x) $o
 fmap10 tensorB (fmap_tensor F (x, x)) (F x) $o
 cat_tensor_associator (F x) (F x) (F x)) $==
fmap F (fmap10 tensorA (mo_mult tensorA) x) $o
(fmap F (cat_tensor_associator x x x) $o
 (fmap_tensor F (x, tensorA x x) $o
  fmap01 tensorB (F x) (fmap_tensor F (x, x))))
    refine (_ $@ (_ $@L (_^$ $@ cat_assoc _ _ _))).A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap_tensor F (x, x) $o
(fmap10 tensorB (fmap F (mo_mult tensorA)) (F x) $o
 fmap10 tensorB (fmap_tensor F (x, x)) (F x) $o
 cat_tensor_associator (F x) (F x) (F x)) $==
fmap F (fmap10 tensorA (mo_mult tensorA) x) $o ?Goal0
A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap F (cat_tensor_associator x x x) $o
fmap_tensor F (x, tensorA x x) $o
fmap01 tensorB (F x) (fmap_tensor F (x, x)) $-> 
?Goal0
    2: snapply fmap_tensor_assoc.A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap_tensor F (x, x) $o
(fmap10 tensorB (fmap F (mo_mult tensorA)) (F x) $o
 fmap10 tensorB (fmap_tensor F (x, x)) (F x) $o
 cat_tensor_associator (F x) (F x) (F x)) $==
fmap F (fmap10 tensorA (mo_mult tensorA) x) $o
(fmap_tensor F (tensorA x x, x) $o
 fmap10 tensorB (fmap_tensor F (x, x)) (F x) $o
 cat_tensor_associator (F x) (F x) (F x))
    nrefine (cat_assoc_opp _ _ _ $@ (cat_assoc_opp _ _ _ $@R _)
      $@ (((_ $@R _) $@ cat_assoc _ _ _) $@R _) $@ cat_assoc _ _ _).A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap_tensor F (x, x) $o
fmap10 tensorB (fmap F (mo_mult tensorA)) (F x) $==
fmap F (fmap10 tensorA (mo_mult tensorA) x) $o
fmap_tensor F (tensorA x x, x)
    snapply fmap_tensor_nat_l.
  -A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap F (mo_mult tensorA) $o fmap_tensor F (x, x) $o
fmap10 tensorB (fmap F (mo_unit tensorA) $o fmap_unit)
  (F x) $== cat_tensor_left_unitor (F x) refine ((_ $@L fmap10_comp tensorB _ _ _) $@ cat_assoc _ _ _
      $@ (_ $@L (cat_assoc_opp _ _ _ $@ (_ $@R _))) $@ _).A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap_tensor F (x, x) $o
fmap10 tensorB (fmap F (mo_unit tensorA)) (F x) $==
?Goal
A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap F (mo_mult tensorA) $o
(?Goal $o fmap10 tensorB fmap_unit (F x)) $==
cat_tensor_left_unitor (F x)
    1: snapply fmap_tensor_nat_l.A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap F (mo_mult tensorA) $o
(fmap F (fmap10 tensorA (mo_unit tensorA) x) $o
 fmap_tensor F (IA, x) $o
 fmap10 tensorB fmap_unit (F x)) $==
cat_tensor_left_unitor (F x)
    refine (cat_assoc_opp _ _ _ $@ ((cat_assoc_opp _ _ _ $@
      (((fmap_comp _ _ _)^$ $@ fmap2 _ (mo_left_unit _)) $@R _)) $@R _) $@ _^$).A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
cat_tensor_left_unitor (F x) $->
fmap F (cat_tensor_left_unitor x) $o
fmap_tensor F (IA, x) $o
fmap10 tensorB fmap_unit (F x)
    snapply fmap_tensor_left_unitor.
  -A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap F (mo_mult tensorA) $o fmap_tensor F (x, x) $o
fmap01 tensorB (F x)
  (fmap F (mo_unit tensorA) $o fmap_unit) $==
cat_tensor_right_unitor (F x) refine ((_ $@L fmap01_comp _ _ _ _) $@ cat_assoc _ _ _
      $@ (_ $@L (cat_assoc_opp _ _ _ $@ (_ $@R _))) $@ _).A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap_tensor F (x, x) $o
fmap01 tensorB (F (fst (x, x)))
  (fmap F (mo_unit tensorA)) $== 
?Goal
A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap F (mo_mult tensorA) $o
(?Goal $o fmap01 tensorB (F (fst (x, x))) fmap_unit) $==
cat_tensor_right_unitor (F x)
    1: snapply fmap_tensor_nat_r.A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
fmap F (mo_mult tensorA) $o
(fmap F (fmap01 tensorA x (mo_unit tensorA)) $o
 fmap_tensor F (x, IA) $o
 fmap01 tensorB (F (fst (x, x))) fmap_unit) $==
cat_tensor_right_unitor (F x)
    refine (cat_assoc_opp _ _ _ $@ ((cat_assoc_opp _ _ _ $@
      (((fmap_comp _ _ _)^$ $@ fmap2 _ (mo_right_unit _)) $@R _)) $@R _) $@ _^$).A, B: Type
tensorA: A -> A -> A
tensorB: B -> B -> B
IA: A
IB: B
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensorA IA
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H2: Is1Cat B
H3: HasEquivs B
H4: IsMonoidal B tensorB IB
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
H5: IsMonoidalFunctor F
x: A
mo_x: IsMonoidObject tensorA IA x
cat_tensor_right_unitor (F x) $->
fmap F (cat_tensor_right_unitor x) $o
fmap_tensor F (x, IA) $o
fmap01 tensorB (F (fst (x, x))) fmap_unit
    snapply fmap_tensor_right_unitor.
Defined.