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

(** * Monoidal Categories *)

(** In this file we define monoidal categories and symmetric monoidal categories. *)

(** ** Typeclasses for common diagrams *)

(** TODO: These should eventually be moved to a separate file in WildCat and used in other places. They can be thought of as a wildcat generalization of the classes in canonical_names.v *)

(** *** Associators *)

Class Associator {A : Type} `{HasEquivs A}
  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F}
  := associator_uncurried
    : NatEquiv (fun '(a, b, c) => F a (F b c)) (fun '(a, b, c) => F (F a b) c).

Arguments associator_uncurried {A _ _ _ _ _ F _ _ _}.

Definition associator {A : Type} `{HasEquivs A} {F : A -> A -> A}
  `{!Is0Bifunctor F, !Is1Bifunctor F, !Associator F}
  : forall a b c, F a (F b c) $<~> F (F a b) c
  := fun a b c => associator_uncurried (a, b, c).
Coercion associator : Associator >-> Funclass.

Definition Build_Associator {A : Type} `{HasEquivs A} (F : A -> A -> A)
  `{!Is0Bifunctor F, !Is1Bifunctor F}
  (associator : forall a b c, F a (F b c) $<~> F (F a b) c)
  (isnat_assoc : Is1Natural
    (fun '(a, b, c) => F a (F b c))
    (fun '(a, b, c) => F (F a b) c)
    (fun '(a, b, c) => associator a b c))
  : Associator F.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
associator: forall a b c : A,
F a (F b c) $<~> F (F a b) c
isnat_assoc: Is1Natural
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F a (F b c))
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F (F a b) c)
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in associator a b c)
Associator F
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
associator: forall a b c : A,
F a (F b c) $<~> F (F a b) c
isnat_assoc: Is1Natural
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F a (F b c))
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F (F a b) c)
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in associator a b c)
Associator F
  snapply Build_NatEquiv.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
associator: forall a b c : A,
F a (F b c) $<~> F (F a b) c
isnat_assoc: Is1Natural
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F a (F b c))
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F (F a b) c)
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in associator a b c)
forall a : A * A * A,
(fun pat : A * A * A =>
 let x := pat in
 let fst := fst x in
 let c := snd x in
 let fst0 := fst in
 let a0 := Overture.fst fst0 in
 let b := snd fst0 in F a0 (F b c)) a $<~>
(fun pat : A * A * A =>
 let x := pat in
 let fst := fst x in
 let c := snd x in
 let fst0 := fst in
 let a0 := Overture.fst fst0 in
 let b := snd fst0 in F (F a0 b) c) a
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
associator: forall a b c : A,
F a (F b c) $<~> F (F a b) c
isnat_assoc: Is1Natural
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F a (F b c))
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F (F a b) c)
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in associator a b c)
Is1Natural
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F a (F b c))
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F (F a b) c)
  (fun a : A * A * A => ?e a)
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
associator: forall a b c : A,
F a (F b c) $<~> F (F a b) c
isnat_assoc: Is1Natural
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F a (F b c))
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F (F a b) c)
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in associator a b c)
forall a : A * A * A,
(fun pat : A * A * A =>
 let x := pat in
 let fst := fst x in
 let c := snd x in
 let fst0 := fst in
 let a0 := Overture.fst fst0 in
 let b := snd fst0 in F a0 (F b c)) a $<~>
(fun pat : A * A * A =>
 let x := pat in
 let fst := fst x in
 let c := snd x in
 let fst0 := fst in
 let a0 := Overture.fst fst0 in
 let b := snd fst0 in F (F a0 b) c) a intros [[a b] c].
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
associator: forall a b c : A,
F a (F b c) $<~> F (F a b) c
isnat_assoc: Is1Natural
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F a (F b c))
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F (F a b) c)
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in associator a b c)
a, b, c: A
(let x := (a, b, c) in
 let fst := fst x in
 let c := snd x in
 let fst0 := fst in
 let a := Overture.fst fst0 in
 let b := snd fst0 in F a (F b c)) $<~>
(let x := (a, b, c) in
 let fst := fst x in
 let c := snd x in
 let fst0 := fst in
 let a := Overture.fst fst0 in
 let b := snd fst0 in F (F a b) c)
    exact (associator a b c).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
associator: forall a b c : A,
F a (F b c) $<~> F (F a b) c
isnat_assoc: Is1Natural
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F a (F b c))
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F (F a b) c)
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in associator a b c)
Is1Natural
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F a (F b c))
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F (F a b) c)
  (fun a : A * A * A =>
   (fun a0 : A * A * A =>
    (fun fst : A * A =>
     (fun a1 b c : A => associator a1 b c)
       (Overture.fst fst) (snd fst)) (fst a0) (snd a0))
     a) exact isnat_assoc.
Defined. 

(** *** Unitors *)

Class LeftUnitor {A : Type} `{HasEquivs A}
  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (unit : A)
  (** A natural isomorphism [left_unitor] witnessing the left unit law of [F]. *)
  := left_unitor : NatEquiv (F unit) idmap.
Coercion left_unitor : LeftUnitor >-> NatEquiv.
Arguments left_unitor {A _ _ _ _ _ F _ _ unit _}.

Class RightUnitor {A : Type} `{HasEquivs A}
  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (unit : A)
  (** A natural isomorphism [right_unitor] witnessing the right unit law of [F]. *)
  := right_unitor : NatEquiv (flip F unit) idmap.
Coercion right_unitor : RightUnitor >-> NatEquiv.
Arguments right_unitor {A _ _ _ _ _ F _ _ unit _}.

(** *** Triangle and Pentagon identities *)

Class TriangleIdentity {A : Type} `{HasEquivs A}
  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F, !Associator F}
  (unit : A) `{!LeftUnitor F unit, !RightUnitor F unit}
  (** The triangle identity for an associator and unitors. *)
  := triangle_identity a b
    : fmap01 F a (left_unitor b)
    $== fmap10 F (right_unitor a) b $o (associator (F := F) a unit b).
Coercion triangle_identity : TriangleIdentity >-> Funclass.
Arguments triangle_identity {A _ _ _ _ _} F {_ _ _} unit {_}.

Class PentagonIdentity {A : Type} `{HasEquivs A}
  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F, !Associator F}
  (** The pentagon identity for an associator. *)
  := pentagon_identity a b c d
    : associator (F a b) c d $o associator a b (F c d)
      $== fmap10 F (associator a b c) d $o associator a (F b c) d
        $o fmap01 F a (associator b c d).
Coercion pentagon_identity : PentagonIdentity >-> Funclass.
Arguments pentagon_identity {A _ _ _ _ _} F {_ _ _}.

(** *** Braiding *)

Class Braiding {A : Type} `{Is1Cat A}
  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F}
  := braid_uncurried : NatTrans (uncurry F) (uncurry (flip F)).

Arguments braid_uncurried {A _ _ _ _ F _ _ _}.

Definition braid {A : Type} `{Is1Cat A} {F : A -> A -> A}
  `{!Is0Bifunctor F, !Is1Bifunctor F, !Braiding F}
  : forall a b, F a b $-> F b a
  := fun a b => braid_uncurried (a, b).
Coercion braid : Braiding >-> Funclass.

Class SymmetricBraiding {A : Type} `{Is1Cat A}
  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} := {
  braiding_symmetricbraiding :: Braiding F;
  braid_braid : forall a b, braid a b $o braid b a $== Id (F b a);
}.
(** We could have used [::>] in [braiding_symmetricbraiding] instead however due to bug https://github.com/coq/coq/issues/18971 the coercion isn't registered, so we have to register it manually instead. *)
Coercion braiding_symmetricbraiding : SymmetricBraiding >-> Braiding.
Arguments braid_braid {A _ _ _ _ F _ _ _} a b.

(** *** Hexagon identity *)

Class HexagonIdentity {A : Type} `{HasEquivs A}
  (F : A -> A -> A)
  `{!Is0Bifunctor F, !Is1Bifunctor F, !Associator F, !Braiding F}
  (** The hexagon identity for an associator and a braiding. *)
  := hexagon_identity a b c
    : fmap10 F (braid b a) c $o associator b a c $o fmap01 F b (braid c a)
      $== associator a b c $o braid (F b c) a $o associator b c a.
Coercion hexagon_identity : HexagonIdentity >-> Funclass.
Arguments hexagon_identity {A _ _ _ _ _} F {_ _}.

(** ** Monoidal Categories *)

(** A monoidal 1-category is a 1-category with equivalences together with the following: *)
Class IsMonoidal (A : Type) `{HasEquivs A}
  (** It has a binary operation [cat_tensor] called the tensor product. *)
  (cat_tensor : A -> A -> A)
  (** It has a unit object [cat_tensor_unit] called the tensor unit. *)
  (cat_tensor_unit : A)
  (** These all satisfy the following properties: *)
  := {
  (** A [cat_tensor] is a 1-bifunctor. *)
  is0bifunctor_cat_tensor :: Is0Bifunctor cat_tensor | 10;
  is1bifunctor_cat_tensor :: Is1Bifunctor cat_tensor | 10;
  (** A natural isomorphism [associator] witnessing the associativity of the tensor product. *)
  cat_tensor_associator :: Associator cat_tensor;
  (** A natural isomorphism [left_unitor] witnessing the left unit law. *)
  cat_tensor_left_unitor :: LeftUnitor cat_tensor cat_tensor_unit;
  (** A natural isomorphism [right_unitor] witnessing the right unit law. *)
  cat_tensor_right_unitor :: RightUnitor cat_tensor cat_tensor_unit;
  (** The triangle identity. *)
  cat_tensor_triangle_identity :: TriangleIdentity cat_tensor cat_tensor_unit;
  (** The pentagon identity. *)
  cat_tensor_pentagon_identity :: PentagonIdentity cat_tensor;
}.

(** TODO: Braided monoidal categories *)

(** ** Symmetric Monoidal Categories *)

(** A symmetric monoidal 1-category is a 1-category with equivalences together with the following: *)
Class IsSymmetricMonoidal (A : Type) `{HasEquivs A}
  (** A binary operation [cat_tensor] called the tensor product. *)
  (cat_tensor : A -> A -> A)
  (** A unit object [cat_tensor_unit] called the tensor unit. *)
  (cat_tensor_unit : A)
  := {
  (** A monoidal structure with [cat_tensor] and [cat_tensor_unit]. *)
  issymmetricmonoidal_ismonoidal :: IsMonoidal A cat_tensor cat_tensor_unit;
  (** A natural transformation [braid] witnessing the symmetry of the tensor product such that [braid] is its own inverse. *)
  cat_symm_tensor_braiding :: SymmetricBraiding cat_tensor;
  (** The hexagon identity. *)
  cat_symm_tensor_hexagon :: HexagonIdentity cat_tensor;
}.

(** *** Theory about [Associator] *)

Section Associator.
  Context {A : Type} `{HasEquivs A} {F : A -> A -> A}
    `{!Is0Bifunctor F, !Is1Bifunctor F, assoc : !Associator F}.

  Definition associator_nat {x x' y y' z z'}
    (f : x $-> x') (g : y $-> y') (h : z $-> z')
    : associator x' y' z' $o fmap11 F f (fmap11 F g h)
      $== fmap11 F (fmap11 F f g) h $o associator x y z.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, x', y, y', z, z': A
f: x $-> x'
g: y $-> y'
h: z $-> z'
assoc x' y' z' $o fmap11 F f (fmap11 F g h) $==
fmap11 F (fmap11 F f g) h $o assoc x y z
  Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, x', y, y', z, z': A
f: x $-> x'
g: y $-> y'
h: z $-> z'
assoc x' y' z' $o fmap11 F f (fmap11 F g h) $==
fmap11 F (fmap11 F f g) h $o assoc x y z
    destruct assoc as [asso nat].
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, x', y, y', z, z': A
f: x $-> x'
g: y $-> y'
h: z $-> z'
asso: forall a : A * A * A,
(let x := a in
 let fst := fst x in
 let c := snd x in
 let fst0 := fst in
 let a0 := Overture.fst fst0 in
 let b := snd fst0 in F a0 (F b c)) $<~>
(let x := a in
 let fst := fst x in
 let c := snd x in
 let fst0 := fst in
 let a0 := Overture.fst fst0 in
 let b := snd fst0 in F (F a0 b) c)
nat: Is1Natural
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F a (F b c))
  (fun pat : A * A * A =>
   let x := pat in
   let fst := fst x in
   let c := snd x in
   let fst0 := fst in
   let a := Overture.fst fst0 in
   let b := snd fst0 in F (F a b) c)
  (fun a : A * A * A => asso a)
{|
  cat_equiv_natequiv := asso;
  is1natural_natequiv := nat
|} x' y' z' $o fmap11 F f (fmap11 F g h) $==
fmap11 F (fmap11 F f g) h $o
{|
  cat_equiv_natequiv := asso;
  is1natural_natequiv := nat
|} x y z
    exact (nat (x, y, z) (x', y', z') (f, g, h)).
  Defined.

  Definition associator_nat_l {x x' : A} (f : x $-> x') (y z : A)
    : associator x' y z $o fmap10 F f (F y z)
      $== fmap10 F (fmap10 F f y) z $o associator x y z.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, x': A
f: x $-> x'
y, z: A
assoc x' y z $o fmap10 F f (F y z) $==
fmap10 F (fmap10 F f y) z $o assoc x y z
  Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, x': A
f: x $-> x'
y, z: A
assoc x' y z $o fmap10 F f (F y z) $==
fmap10 F (fmap10 F f y) z $o assoc x y z
    refine ((_ $@L _^$) $@ _ $@ (_ $@R _)).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, x': A
f: x $-> x'
y, z: A
?Goal $-> fmap10 F f (F y z)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, x': A
f: x $-> x'
y, z: A
assoc x' y z $o ?Goal $== ?Goal2 $o assoc x y z
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, x': A
f: x $-> x'
y, z: A
?Goal2 $== fmap10 F (fmap10 F f y) z
    2: exact (associator_nat f (Id _) (Id _)).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, x': A
f: x $-> x'
y, z: A
fmap11 F f (fmap11 F (Id y) (Id z)) $->
fmap10 F f (F y z)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, x': A
f: x $-> x'
y, z: A
fmap11 F (fmap11 F f (Id y)) (Id z) $==
fmap10 F (fmap10 F f y) z
    -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, x': A
f: x $-> x'
y, z: A
fmap11 F f (fmap11 F (Id y) (Id z)) $->
fmap10 F f (F y z) exact (fmap12 _ _ (fmap11_id _ _ _) $@ fmap10_is_fmap11 _ _ _).
    -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, x': A
f: x $-> x'
y, z: A
fmap11 F (fmap11 F f (Id y)) (Id z) $==
fmap10 F (fmap10 F f y) z exact (fmap21 _ (fmap10_is_fmap11 _ _ _) _ $@ fmap10_is_fmap11 _ _ _).
  Defined.

  Definition associator_nat_m (x : A) {y y' : A} (g : y $-> y') (z : A)
    : associator x y' z $o fmap01 F x (fmap10 F g z)
      $== fmap10 F (fmap01 F x g) z $o associator x y z.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, y': A
g: y $-> y'
z: A
assoc x y' z $o fmap01 F x (fmap10 F g z) $==
fmap10 F (fmap01 F x g) z $o assoc x y z
  Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, y': A
g: y $-> y'
z: A
assoc x y' z $o fmap01 F x (fmap10 F g z) $==
fmap10 F (fmap01 F x g) z $o assoc x y z
    refine ((_ $@L _^$) $@ _ $@ (_ $@R _)).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, y': A
g: y $-> y'
z: A
?Goal $-> fmap01 F x (fmap10 F g z)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, y': A
g: y $-> y'
z: A
assoc x y' z $o ?Goal $== ?Goal2 $o assoc x y z
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, y': A
g: y $-> y'
z: A
?Goal2 $== fmap10 F (fmap01 F x g) z
    2: exact (associator_nat (Id _) g (Id _)).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, y': A
g: y $-> y'
z: A
fmap11 F (Id x) (fmap11 F g (Id z)) $->
fmap01 F x (fmap10 F g z)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, y': A
g: y $-> y'
z: A
fmap11 F (fmap11 F (Id x) g) (Id z) $==
fmap10 F (fmap01 F x g) z
    -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, y': A
g: y $-> y'
z: A
fmap11 F (Id x) (fmap11 F g (Id z)) $->
fmap01 F x (fmap10 F g z) exact (fmap12 _ _ (fmap10_is_fmap11 _ _ _) $@ fmap01_is_fmap11 _ _ _).
    -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, y': A
g: y $-> y'
z: A
fmap11 F (fmap11 F (Id x) g) (Id z) $==
fmap10 F (fmap01 F x g) z exact (fmap21 _ (fmap01_is_fmap11 _ _ _) _ $@ fmap10_is_fmap11 _ _ _).
  Defined.

  Definition associator_nat_r (x y : A) {z z' : A} (h : z $-> z')
    : associator x y z' $o fmap01 F x (fmap01 F y h)
      $== fmap01 F (F x y) h $o associator x y z.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, z, z': A
h: z $-> z'
assoc x y z' $o fmap01 F x (fmap01 F y h) $==
fmap01 F (F x y) h $o assoc x y z
  Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, z, z': A
h: z $-> z'
assoc x y z' $o fmap01 F x (fmap01 F y h) $==
fmap01 F (F x y) h $o assoc x y z
    refine ((_ $@L _^$) $@ _ $@ (_ $@R _)).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, z, z': A
h: z $-> z'
?Goal $-> fmap01 F x (fmap01 F y h)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, z, z': A
h: z $-> z'
assoc x y z' $o ?Goal $== ?Goal2 $o assoc x y z
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, z, z': A
h: z $-> z'
?Goal2 $== fmap01 F (F x y) h
    2: exact (associator_nat (Id _) (Id _) h).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, z, z': A
h: z $-> z'
fmap11 F (Id x) (fmap11 F (Id y) h) $->
fmap01 F x (fmap01 F y h)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, z, z': A
h: z $-> z'
fmap11 F (fmap11 F (Id x) (Id y)) h $==
fmap01 F (F x y) h
    -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, z, z': A
h: z $-> z'
fmap11 F (Id x) (fmap11 F (Id y) h) $->
fmap01 F x (fmap01 F y h) exact (fmap12 _ _ (fmap01_is_fmap11 _ _ _) $@ fmap01_is_fmap11 _ _ _).
    -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
F: A -> A -> A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
assoc: Associator F
x, y, z, z': A
h: z $-> z'
fmap11 F (fmap11 F (Id x) (Id y)) h $==
fmap01 F (F x y) h exact (fmap21 _ (fmap11_id _ _ _) _ $@ fmap01_is_fmap11 F _ _).
  Defined.

  #[export] Instance associator_op : Associator (A:=A^op) F
    := natequiv_inverse (natequiv_op assoc).

End Associator.

Definition associator_op' {A : Type} `{HasEquivs A} {F : A -> A -> A}
  `{!Is0Bifunctor F, !Is1Bifunctor F, assoc : !Associator (A:=A^op) F}
  : Associator F
  := associator_op (A:=A^op) (assoc := assoc).

(** ** Theory about [LeftUnitor] and [RightUnitor] *)

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

  #[export] Instance left_unitor_op : LeftUnitor (A:=A^op) F unit
    := natequiv_inverse (natequiv_op left_unitor).

  #[export] Instance right_unitor_op : RightUnitor (A:=A^op) F unit
    := natequiv_inverse (natequiv_op right_unitor).

End LeftUnitor.

(** ** Theory about [Braiding] *)

Instance braiding_op {A : Type} `{HasEquivs A} {F : A -> A -> A}
  `{!Is0Bifunctor F, !Is1Bifunctor F, braid : !Braiding F}
  : Braiding (A:=A^op) F
  := nattrans_op (nattrans_flip braid).

Definition braiding_op' {A : Type} `{HasEquivs A} {F : A -> A -> A}
  `{!Is0Bifunctor F, !Is1Bifunctor F, braid : !Braiding (A:=A^op) F}
  : Braiding F
  := braiding_op (A:=A^op) (braid := braid).

(** ** Theory about [SymmetricBraid] *)

Section SymmetricBraid.
  Context {A : Type} {F : A -> A -> A} `{SymmetricBraiding A F, !HasEquivs A}.

  (** [braid] is its own inverse and therefore an equivalence. *)
  Instance catie_braid a b : CatIsEquiv (braid a b)
    := catie_adjointify (braid a b) (braid b a) (braid_braid a b) (braid_braid b a).

  (** [braide] is the bundled equivalence whose underlying map is [braid]. *)
  Definition braide a b
    : F a b $<~> F b a
    := Build_CatEquiv (braid a b).

  Definition moveL_braidL {a b c : A} f (g : c $-> _)
    : braid a b $o f $== g -> f $== braid b a $o g.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: c $-> F a b
g: c $-> F b a
H0 a b $o f $== g -> f $== H0 b a $o g
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: c $-> F a b
g: c $-> F b a
H0 a b $o f $== g -> f $== H0 b a $o g
    intros p.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: c $-> F a b
g: c $-> F b a
p: H0 a b $o f $== g
f $== H0 b a $o g
    apply (cate_monic_equiv (braide a b)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: c $-> F a b
g: c $-> F b a
p: H0 a b $o f $== g
braide a b $o f $== braide a b $o (H0 b a $o g)
    refine ((cate_buildequiv_fun _ $@R _) $@ p $@ _ $@ cat_assoc _ _ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: c $-> F a b
g: c $-> F b a
p: H0 a b $o f $== g
g $== braide a b $o H0 b a $o g
    refine ((cat_idl _)^$ $@ (_^$ $@R _)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: c $-> F a b
g: c $-> F b a
p: H0 a b $o f $== g
braide a b $o H0 b a $-> Id (F b a)
    refine ((cate_buildequiv_fun _ $@R _) $@ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: c $-> F a b
g: c $-> F b a
p: H0 a b $o f $== g
H0 a b $o H0 b a $== Id (F b a)
    apply braid_braid.
  Defined.

  Definition moveL_braidR {a b c : A} f (g : _ $-> c)
    : f $o braid a b $== g -> f $== g $o braid b a.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: F b a $-> c
g: F a b $-> c
f $o H0 a b $== g -> f $== g $o H0 b a
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: F b a $-> c
g: F a b $-> c
f $o H0 a b $== g -> f $== g $o H0 b a
    intros p.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: F b a $-> c
g: F a b $-> c
p: f $o H0 a b $== g
f $== g $o H0 b a
    apply (cate_epic_equiv (braide a b)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: F b a $-> c
g: F a b $-> c
p: f $o H0 a b $== g
f $o braide a b $== g $o H0 b a $o braide a b
    refine (_ $@ (cat_assoc _ _ _)^$).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: F b a $-> c
g: F a b $-> c
p: f $o H0 a b $== g
f $o braide a b $== g $o (H0 b a $o braide a b)
    refine (_ $@ (_ $@L ((_ $@L cate_buildequiv_fun _) $@ _)^$)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: F b a $-> c
g: F a b $-> c
p: f $o H0 a b $== g
f $o braide a b $== g $o ?Goal0
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: F b a $-> c
g: F a b $-> c
p: f $o H0 a b $== g
H0 b a $o H0 a b $== ?Goal0
    2: apply braid_braid.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: F b a $-> c
g: F a b $-> c
p: f $o H0 a b $== g
f $o braide a b $== g $o Id (F a b)
    refine ((_ $@L _) $@ _ $@ (cat_idr _)^$).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: F b a $-> c
g: F a b $-> c
p: f $o H0 a b $== g
braide a b $== ?Goal
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: F b a $-> c
g: F a b $-> c
p: f $o H0 a b $== g
f $o ?Goal $== g
    1: apply cate_buildequiv_fun.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: F b a $-> c
g: F a b $-> c
p: f $o H0 a b $== g
f $o H0 a b $== g
    exact p.
  Defined.

  Definition moveR_braidL {a b c : A} f (g : c $-> _)
    : f $== braid b a $o g -> braid a b $o f $== g.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: c $-> F a b
g: c $-> F b a
f $== H0 b a $o g -> H0 a b $o f $== g
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: c $-> F a b
g: c $-> F b a
f $== H0 b a $o g -> H0 a b $o f $== g
    intros p; symmetry; apply moveL_braidL; symmetry; exact p.
  Defined.

  Definition moveR_braidR {a b c : A} f (g : _ $-> c)
    : f $== g $o braid b a -> f $o braid a b $== g.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: F b a $-> c
g: F a b $-> c
f $== g $o H0 b a -> f $o H0 a b $== g
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: F b a $-> c
g: F a b $-> c
f $== g $o H0 b a -> f $o H0 a b $== g
    intros p; symmetry; apply moveL_braidR; symmetry; exact p.
  Defined.

  Definition moveL_fmap01_braidL {a b c d : A} f (g : d $-> _)
    : fmap01 F a (braid b c) $o f $== g
      -> f $== fmap01 F a (braid c b) $o g.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
fmap01 F a (H0 b c) $o f $== g ->
f $== fmap01 F a (H0 c b) $o g
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
fmap01 F a (H0 b c) $o f $== g ->
f $== fmap01 F a (H0 c b) $o g
    intros p.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
p: fmap01 F a (H0 b c) $o f $== g
f $== fmap01 F a (H0 c b) $o g
    apply (cate_monic_equiv (emap01 F a (braide b c))).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
p: fmap01 F a (H0 b c) $o f $== g
emap01 F a (braide b c) $o f $==
emap01 F a (braide b c) $o (fmap01 F a (H0 c b) $o g)
    refine (_ $@ cat_assoc _ _ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
p: fmap01 F a (H0 b c) $o f $== g
emap01 F a (braide b c) $o f $==
emap01 F a (braide b c) $o fmap01 F a (H0 c b) $o g
    refine (_ $@ (_ $@R _)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
p: fmap01 F a (H0 b c) $o f $== g
emap01 F a (braide b c) $o f $== ?Goal0 $o g
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
p: fmap01 F a (H0 b c) $o f $== g
?Goal0 $==
emap01 F a (braide b c) $o fmap01 F a (H0 c b)
    2: {
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
p: fmap01 F a (H0 b c) $o f $== g
?Goal0 $==
emap01 F a (braide b c) $o fmap01 F a (H0 c b) refine (_ $@ (_^$ $@R _)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
p: fmap01 F a (H0 b c) $o f $== g
?Goal0 $== ?Goal2 $o fmap01 F a (H0 c b)
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
p: fmap01 F a (H0 b c) $o f $== g
emap01 F a (braide b c) $-> ?Goal2
      2: apply cate_buildequiv_fun.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
p: fmap01 F a (H0 b c) $o f $== g
?Goal0 $==
fmap01 F a (braide b c) $o fmap01 F a (H0 c b)
      refine ((fmap_id _ _)^$ $@ fmap2 _ _ $@ fmap_comp _ _ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
p: fmap01 F a (H0 b c) $o f $== g
Id (F c b) $== braide b c $o H0 c b
      refine ((_ $@R _) $@ _)^$.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
p: fmap01 F a (H0 b c) $o f $== g
braide b c $== ?Goal0
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
p: fmap01 F a (H0 b c) $o f $== g
?Goal0 $o H0 c b $== Id (F c b)
      1: apply cate_buildequiv_fun.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
p: fmap01 F a (H0 b c) $o f $== g
H0 b c $o H0 c b $== Id (F c b)
      apply braid_braid. }
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
p: fmap01 F a (H0 b c) $o f $== g
emap01 F a (braide b c) $o f $== Id (F a (F c b)) $o g
    refine ((_ $@R _) $@ p $@ (cat_idl _)^$).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
p: fmap01 F a (H0 b c) $o f $== g
emap01 F a (braide b c) $== fmap01 F a (H0 b c)
    refine (_ $@ fmap2 _ _);
    apply cate_buildequiv_fun.
  Defined.

  Definition moveL_fmap01_braidR {a b c d : A} f (g : _ $-> d)
    :  f $o fmap01 F a (braid b c) $== g
      -> f $== g $o fmap01 F a (braid c b).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
f $o fmap01 F a (H0 b c) $== g ->
f $== g $o fmap01 F a (H0 c b)
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
f $o fmap01 F a (H0 b c) $== g ->
f $== g $o fmap01 F a (H0 c b)
    intros p.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
p: f $o fmap01 F a (H0 b c) $== g
f $== g $o fmap01 F a (H0 c b)
    apply (cate_epic_equiv (emap01 F a (braide b c))).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
p: f $o fmap01 F a (H0 b c) $== g
f $o emap01 F a (braide b c) $==
g $o fmap01 F a (H0 c b) $o emap01 F a (braide b c)
    refine (_ $@ (cat_assoc _ _ _)^$).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
p: f $o fmap01 F a (H0 b c) $== g
f $o emap01 F a (braide b c) $==
g $o (fmap01 F a (H0 c b) $o emap01 F a (braide b c))
    refine (_ $@ (_ $@L _)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
p: f $o fmap01 F a (H0 b c) $== g
f $o emap01 F a (braide b c) $== g $o ?Goal0
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
p: f $o fmap01 F a (H0 b c) $== g
?Goal0 $==
fmap01 F a (H0 c b) $o emap01 F a (braide b c)
    2: {
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
p: f $o fmap01 F a (H0 b c) $== g
?Goal0 $==
fmap01 F a (H0 c b) $o emap01 F a (braide b c) refine (_^$ $@ (_ $@L _^$)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
p: f $o fmap01 F a (H0 b c) $== g
fmap01 F a (H0 c b) $o ?Goal2 $-> ?Goal0
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
p: f $o fmap01 F a (H0 b c) $== g
emap01 F a (braide b c) $-> ?Goal2
      2: apply cate_buildequiv_fun.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
p: f $o fmap01 F a (H0 b c) $== g
fmap01 F a (H0 c b) $o fmap01 F a (braide b c) $->
?Goal0
      refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
p: f $o fmap01 F a (H0 b c) $== g
H0 c b $o braide b c $== Id (F b c)
      refine ((_ $@L _) $@ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
p: f $o fmap01 F a (H0 b c) $== g
braide b c $== ?Goal0
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
p: f $o fmap01 F a (H0 b c) $== g
H0 c b $o ?Goal0 $== Id (F b c)
      1: apply cate_buildequiv_fun.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
p: f $o fmap01 F a (H0 b c) $== g
H0 c b $o H0 b c $== Id (F b c)
      apply braid_braid. }
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
p: f $o fmap01 F a (H0 b c) $== g
f $o emap01 F a (braide b c) $== g $o Id (F a (F b c))
    refine ((_ $@L _) $@ p $@ (cat_idr _)^$).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
p: f $o fmap01 F a (H0 b c) $== g
emap01 F a (braide b c) $== fmap01 F a (H0 b c)
    refine (_ $@ fmap2 _ _);
    apply cate_buildequiv_fun.
  Defined.

  Definition moveR_fmap01_braidL {a b c d : A} f (g : d $-> _)
    : f $== fmap01 F a (braid c b) $o g
      -> fmap01 F a (braid b c) $o f $== g.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
f $== fmap01 F a (H0 c b) $o g ->
fmap01 F a (H0 b c) $o f $== g
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: d $-> F a (F b c)
g: d $-> F a (F c b)
f $== fmap01 F a (H0 c b) $o g ->
fmap01 F a (H0 b c) $o f $== g
    intros p; symmetry; apply moveL_fmap01_braidL; symmetry; exact p.
  Defined.

  Definition moveR_fmap01_braidR {a b c d : A} f (g : _ $-> d)
    : f $== g $o fmap01 F a (braid c b)
      -> f $o fmap01 F a (braid b c) $== g.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
f $== g $o fmap01 F a (H0 c b) ->
f $o fmap01 F a (H0 b c) $== g
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: F a (F c b) $-> d
g: F a (F b c) $-> d
f $== g $o fmap01 F a (H0 c b) ->
f $o fmap01 F a (H0 b c) $== g
    intros p; symmetry; apply moveL_fmap01_braidR; symmetry; exact p.
  Defined.

  Definition moveL_fmap01_fmap01_braidL {a b c d e : A} f (g : e $-> _)
    : fmap01 F a (fmap01 F b (braid c d)) $o f $== g
      -> f $== fmap01 F a (fmap01 F b (braid d c)) $o g.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
fmap01 F a (fmap01 F b (H0 c d)) $o f $== g ->
f $== fmap01 F a (fmap01 F b (H0 d c)) $o g
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
fmap01 F a (fmap01 F b (H0 c d)) $o f $== g ->
f $== fmap01 F a (fmap01 F b (H0 d c)) $o g
    intros p.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
f $== fmap01 F a (fmap01 F b (H0 d c)) $o g
    apply (cate_monic_equiv (emap01 F a (emap01 F b (braide c d)))).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
emap01 F a (emap01 F b (braide c d)) $o f $==
emap01 F a (emap01 F b (braide c d)) $o
(fmap01 F a (fmap01 F b (H0 d c)) $o g)
    refine (_ $@ cat_assoc _ _ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
emap01 F a (emap01 F b (braide c d)) $o f $==
emap01 F a (emap01 F b (braide c d)) $o
fmap01 F a (fmap01 F b (H0 d c)) $o g
    refine (_ $@ (_ $@R _)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
emap01 F a (emap01 F b (braide c d)) $o f $==
?Goal0 $o g
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
?Goal0 $==
emap01 F a (emap01 F b (braide c d)) $o
fmap01 F a (fmap01 F b (H0 d c))
    2: {
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
?Goal0 $==
emap01 F a (emap01 F b (braide c d)) $o
fmap01 F a (fmap01 F b (H0 d c)) refine (_ $@ (_^$ $@R _)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
?Goal0 $== ?Goal2 $o fmap01 F a (fmap01 F b (H0 d c))
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
emap01 F a (emap01 F b (braide c d)) $-> ?Goal2
      2: apply cate_buildequiv_fun.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
?Goal0 $==
fmap01 F a (emap01 F b (braide c d)) $o
fmap01 F a (fmap01 F b (H0 d c))
      refine ((fmap_id _ _)^$ $@ fmap2 _ _ $@ fmap_comp _ _ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
Id (F b (F d c)) $==
emap01 F b (braide c d) $o fmap01 F b (H0 d c)
      refine (_ $@ (_^$ $@R _)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
Id (F b (F d c)) $== ?Goal1 $o fmap01 F b (H0 d c)
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
emap01 F b (braide c d) $-> ?Goal1
      2: apply cate_buildequiv_fun.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
Id (F b (F d c)) $==
fmap01 F b (braide c d) $o fmap01 F b (H0 d c)
      refine ((fmap_id _ _)^$ $@ fmap2 _ _ $@ fmap_comp _ _ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
Id (F d c) $== braide c d $o H0 d c
      refine ((_ $@R _) $@ _)^$.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
braide c d $== ?Goal0
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
?Goal0 $o H0 d c $== Id (F d c)
      1: apply cate_buildequiv_fun.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
H0 c d $o H0 d c $== Id (F d c)
      apply braid_braid. }
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
emap01 F a (emap01 F b (braide c d)) $o f $==
Id (F a (F b (F d c))) $o g
    refine ((_ $@R _) $@ p $@ (cat_idl _)^$).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
emap01 F a (emap01 F b (braide c d)) $==
fmap01 F a (fmap01 F b (H0 c d))
    refine (cate_buildequiv_fun _ $@ fmap02 _ _ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
emap01 F b (braide c d) $== fmap01 F b (H0 c d)
    refine (cate_buildequiv_fun _ $@ fmap02 _ _ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
p: fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
braide c d $== H0 c d
    apply cate_buildequiv_fun.
  Defined.

  Definition moveL_fmap01_fmap01_braidR {a b c d e : A} f (g : _ $-> e)
    : f $o fmap01 F a (fmap01 F b (braid c d)) $== g
      -> f $== g $o fmap01 F a (fmap01 F b (braid d c)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
f $o fmap01 F a (fmap01 F b (H0 c d)) $== g ->
f $== g $o fmap01 F a (fmap01 F b (H0 d c))
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
f $o fmap01 F a (fmap01 F b (H0 c d)) $== g ->
f $== g $o fmap01 F a (fmap01 F b (H0 d c))
    intros p.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
f $== g $o fmap01 F a (fmap01 F b (H0 d c))
    apply (cate_epic_equiv (emap01 F a (emap01 F b (braide c d)))).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
f $o emap01 F a (emap01 F b (braide c d)) $==
g $o fmap01 F a (fmap01 F b (H0 d c)) $o
emap01 F a (emap01 F b (braide c d))
    refine (_ $@ (cat_assoc _ _ _)^$).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
f $o emap01 F a (emap01 F b (braide c d)) $==
g $o
(fmap01 F a (fmap01 F b (H0 d c)) $o
 emap01 F a (emap01 F b (braide c d)))
    refine (_ $@ (_ $@L _)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
f $o emap01 F a (emap01 F b (braide c d)) $==
g $o ?Goal0
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
?Goal0 $==
fmap01 F a (fmap01 F b (H0 d c)) $o
emap01 F a (emap01 F b (braide c d))
    2: {
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
?Goal0 $==
fmap01 F a (fmap01 F b (H0 d c)) $o
emap01 F a (emap01 F b (braide c d)) refine (_^$ $@ (_ $@L _^$)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
fmap01 F a (fmap01 F b (H0 d c)) $o ?Goal2 $-> ?Goal0
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
emap01 F a (emap01 F b (braide c d)) $-> ?Goal2
      2: apply cate_buildequiv_fun.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
fmap01 F a (fmap01 F b (H0 d c)) $o
fmap01 F a (emap01 F b (braide c d)) $-> ?Goal0
      refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
fmap01 F b (H0 d c) $o emap01 F b (braide c d) $==
Id (F b (F c d))
      refine ((_ $@L _) $@ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
emap01 F b (braide c d) $== ?Goal0
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
fmap01 F b (H0 d c) $o ?Goal0 $== Id (F b (F c d))
      1: apply cate_buildequiv_fun.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
fmap01 F b (H0 d c) $o fmap01 F b (braide c d) $==
Id (F b (F c d))
      refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
H0 d c $o braide c d $== Id (F c d)
      refine ((_ $@L _) $@ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
braide c d $== ?Goal0
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
H0 d c $o ?Goal0 $== Id (F c d)
      1: apply cate_buildequiv_fun.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
H0 d c $o H0 c d $== Id (F c d)
      apply braid_braid. }
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
f $o emap01 F a (emap01 F b (braide c d)) $==
g $o Id (F a (F b (F c d)))
    refine ((_ $@L _) $@ p $@ (cat_idr _)^$).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
emap01 F a (emap01 F b (braide c d)) $==
fmap01 F a (fmap01 F b (H0 c d))
    refine (cate_buildequiv_fun _ $@ fmap02 _ _ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
emap01 F b (braide c d) $== fmap01 F b (H0 c d)
    refine (cate_buildequiv_fun _ $@ fmap02 _ _ _).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
p: f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
braide c d $== H0 c d
    apply cate_buildequiv_fun.
  Defined.

  Definition moveR_fmap01_fmap01_braidL {a b c d e : A} f (g : e $-> _)
    : f $== fmap01 F a (fmap01 F b (braid d c)) $o g
      -> fmap01 F a (fmap01 F b (braid c d)) $o f $== g.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
f $== fmap01 F a (fmap01 F b (H0 d c)) $o g ->
fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: e $-> F a (F b (F c d))
g: e $-> F a (F b (F d c))
f $== fmap01 F a (fmap01 F b (H0 d c)) $o g ->
fmap01 F a (fmap01 F b (H0 c d)) $o f $== g
    intros p; symmetry; apply moveL_fmap01_fmap01_braidL; symmetry; exact p.
  Defined.

  Definition moveR_fmap01_fmap01_braidR {a b c d e : A} f (g : _ $-> e)
    : f $== g $o fmap01 F a (fmap01 F b (braid d c))
      -> f $o fmap01 F a (fmap01 F b (braid c d)) $== g.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
f $== g $o fmap01 F a (fmap01 F b (H0 d c)) ->
f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d, e: A
f: F a (F b (F d c)) $-> e
g: F a (F b (F c d)) $-> e
f $== g $o fmap01 F a (fmap01 F b (H0 d c)) ->
f $o fmap01 F a (fmap01 F b (H0 c d)) $== g
    intros p; symmetry; apply moveL_fmap01_fmap01_braidR; symmetry; exact p.
  Defined.

  Definition braid_nat {a b c d} (f : a $-> c) (g : b $-> d)
    : braid c d $o fmap11 F f g $== fmap11 F g f $o braid a b.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: a $-> c
g: b $-> d
H0 c d $o fmap11 F f g $== fmap11 F g f $o H0 a b
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c, d: A
f: a $-> c
g: b $-> d
H0 c d $o fmap11 F f g $== fmap11 F g f $o H0 a b
    exact (isnat braid_uncurried (a := (a, b)) (a' := (c, d)) (f, g)).
  Defined.

  Definition braid_nat_l {a b c} (f : a $-> b)
    : braid b c $o fmap10 F f c $== fmap01 F c f $o braid a c.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: a $-> b
H0 b c $o fmap10 F f c $== fmap01 F c f $o H0 a c
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: a $-> b
H0 b c $o fmap10 F f c $== fmap01 F c f $o H0 a c
    refine ((_ $@L (fmap10_is_fmap11 _ _ _)^$) $@ _ $@ (fmap01_is_fmap11 _ _ _ $@R _)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
f: a $-> b
H0 b c $o fmap11 F f (Id c) $==
fmap11 F (Id c) f $o H0 a c
    exact (isnat braid_uncurried (a := (a, c)) (a' := (b, c)) (f, Id _)).
  Defined.

  (** This is just the inverse of above. *)
  Definition braid_nat_r {a b c} (g : b $-> c)
    : braid a c $o fmap01 F a g $== fmap10 F g a $o braid a b.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
g: b $-> c
H0 a c $o fmap01 F a g $== fmap10 F g a $o H0 a b
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
g: b $-> c
H0 a c $o fmap01 F a g $== fmap10 F g a $o H0 a b
    refine ((_ $@L (fmap01_is_fmap11 _ _ _)^$) $@ _ $@ (fmap10_is_fmap11 _ _ _ $@R _)).
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b, c: A
g: b $-> c
H0 a c $o fmap11 F (Id a) g $==
fmap11 F g (Id a) $o H0 a b
    exact (isnat braid_uncurried (a := (a, b)) (a' := (a, c)) (Id _ , g)).
  Defined.

  #[export] Instance symmetricbraiding_op : SymmetricBraiding (A:=A^op) F.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
SymmetricBraiding F
  Proof.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
SymmetricBraiding F
    snapply Build_SymmetricBraiding.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
Braiding F
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
forall a b : A^op,
?braiding_symmetricbraiding a b $o
?braiding_symmetricbraiding b a $== 
Id (F b a)
    -
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
Braiding F exact _.
    -
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
forall a b : A^op,
braiding_op a b $o braiding_op b a $== Id (F b a) intros a b.
A: Type
F: A -> A -> A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
H0: SymmetricBraiding F
HasEquivs0: HasEquivs A
a, b: A^op
braiding_op a b $o braiding_op b a $== Id (F b a)
      rapply braid_braid.
  Defined.

End SymmetricBraid.

Definition symmetricbraiding_op' {A : Type} {F : A -> A -> A}
  `{HasEquivs A, !Is0Bifunctor F, !Is1Bifunctor F,
    H' : !SymmetricBraiding (A:=A^op) F}
  : SymmetricBraiding F
  := symmetricbraiding_op (A:=A^op) (F := F).

(** ** Opposite Monoidal Categories *)

Instance ismonoidal_op {A : Type} (tensor : A -> A -> A) (unit : A)
  `{IsMonoidal A tensor unit}
  : IsMonoidal 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
H1: IsMonoidal A tensor unit
IsMonoidal A^op tensor unit
Proof.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
IsMonoidal A^op tensor unit
  snapply Build_IsMonoidal.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
Is0Bifunctor tensor
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
Is1Bifunctor tensor
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
Associator tensor
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
LeftUnitor 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
H1: IsMonoidal A tensor unit
RightUnitor 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
H1: IsMonoidal A tensor unit
TriangleIdentity 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
H1: IsMonoidal A tensor unit
PentagonIdentity tensor
  1-5: exact _.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
TriangleIdentity 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
H1: IsMonoidal A tensor unit
PentagonIdentity tensor
  -
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
TriangleIdentity tensor unit intros a b; unfold op in a, b; simpl.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
a, b: A
fmap01 tensor a
  (cate_fun' b (tensor unit b)
     (cate_buildequiv' b 
        (tensor unit b)
        (cate_inv' (tensor unit b) b
           (cat_tensor_left_unitor b))
        (catie_adjointify
           (cate_inv' (tensor unit b) b
              (cat_tensor_left_unitor b))
           (cate_fun' (tensor unit b) b
              (cat_tensor_left_unitor b))
           (cate_issect' 
              (tensor unit b) b
              (cat_tensor_left_unitor b))
           (cate_isretr' 
              (tensor unit b) b
              (cat_tensor_left_unitor b))))) $==
cate_fun' (tensor (tensor a unit) b)
  (tensor a (tensor unit b)) 
  (associator_op a unit b) $o
fmap10 tensor
  (cate_fun' a (tensor a unit)
     (cate_buildequiv' a 
        (tensor a unit)
        (cate_inv' (tensor a unit) a
           (cat_tensor_right_unitor a))
        (catie_adjointify
           (cate_inv' (tensor a unit) a
              (cat_tensor_right_unitor a))
           (cate_fun' (tensor a unit) a
              (cat_tensor_right_unitor a))
           (cate_issect' 
              (tensor a unit) a
              (cat_tensor_right_unitor a))
           (cate_isretr' 
              (tensor a unit) a
              (cat_tensor_right_unitor a))))) b
    refine (_^$ $@ _ $@ (_ $@L _)).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
a, b: A
?Goal $->
fmap01 tensor a
  (cate_fun' b (tensor unit b)
     (cate_buildequiv' b 
        (tensor unit b)
        (cate_inv' (tensor unit b) b
           (cat_tensor_left_unitor b))
        (catie_adjointify
           (cate_inv' (tensor unit b) b
              (cat_tensor_left_unitor b))
           (cate_fun' (tensor unit b) b
              (cat_tensor_left_unitor b))
           (cate_issect' 
              (tensor unit b) b
              (cat_tensor_left_unitor b))
           (cate_isretr' 
              (tensor unit b) b
              (cat_tensor_left_unitor b)))))
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
a, b: A
?Goal $==
cate_fun' (tensor (tensor a unit) b)
  (tensor a (tensor unit b)) 
  (associator_op a unit b) $o 
?Goal2
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
a, b: A
?Goal2 $==
fmap10 tensor
  (cate_fun' a (tensor a unit)
     (cate_buildequiv' a 
        (tensor a unit)
        (cate_inv' (tensor a unit) a
           (cat_tensor_right_unitor a))
        (catie_adjointify
           (cate_inv' (tensor a unit) a
              (cat_tensor_right_unitor a))
           (cate_fun' (tensor a unit) a
              (cat_tensor_right_unitor a))
           (cate_issect' 
              (tensor a unit) a
              (cat_tensor_right_unitor a))
           (cate_isretr' 
              (tensor a unit) a
              (cat_tensor_right_unitor a))))) b
    1,3: exact (emap_inv _ _ $@ cate_buildequiv_fun _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
a, b: A
(emap (tensor a) (cat_tensor_left_unitor b))^-1$ $==
cate_fun' (tensor (tensor a unit) b)
  (tensor a (tensor unit b)) 
  (associator_op a unit b) $o
(emap (flip tensor b) (cat_tensor_right_unitor a))^-1$
    nrefine (cate_inv2 _ $@ cate_inv_compose' _ _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
a, b: A
emap (tensor a) (cat_tensor_left_unitor b) $==
emap (flip tensor b) (cat_tensor_right_unitor a) $oE
cat_tensor_associator (a, unit, b)
    refine (cate_buildequiv_fun _ $@ _ $@ ((cate_buildequiv_fun _)^$ $@R _)
      $@ (cate_buildequiv_fun _)^$).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
a, b: A
fmap (tensor a) (cat_tensor_left_unitor b) $==
fmap (flip tensor b) (cat_tensor_right_unitor a) $o
cat_tensor_associator (a, unit, b)
    rapply cat_tensor_triangle_identity.
  -
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
PentagonIdentity tensor intros a b c d; unfold op in a, b, c, d; simpl.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
a, b, c, d: A
cate_fun' (tensor (tensor a b) (tensor c d))
  (tensor a (tensor b (tensor c d)))
  (associator_op a b (tensor c d)) $o
cate_fun' (tensor (tensor (tensor a b) c) d)
  (tensor (tensor a b) (tensor c d))
  (associator_op (tensor a b) c d) $==
fmap01 tensor a
  (cate_fun' (tensor (tensor b c) d)
     (tensor b (tensor c d)) 
     (associator_op b c d)) $o
(cate_fun' (tensor (tensor a (tensor b c)) d)
   (tensor a (tensor (tensor b c) d))
   (associator_op a (tensor b c) d) $o
 fmap10 tensor
   (cate_fun' (tensor (tensor a b) c)
      (tensor a (tensor b c)) 
      (associator_op a b c)) d)
    refine (_ $@ ((_ $@L _) $@@ _)).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
a, b, c, d: A
cate_fun' (tensor (tensor a b) (tensor c d))
  (tensor a (tensor b (tensor c d)))
  (associator_op a b (tensor c d)) $o
cate_fun' (tensor (tensor (tensor a b) c) d)
  (tensor (tensor a b) (tensor c d))
  (associator_op (tensor a b) c d) $==
?Goal0 $o
(cate_fun' (tensor (tensor a (tensor b c)) d)
   (tensor a (tensor (tensor b c) d))
   (associator_op a (tensor b c) d) $o 
 ?Goal1)
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
a, b, c, d: A
?Goal1 $==
fmap10 tensor
  (cate_fun' (tensor (tensor a b) c)
     (tensor a (tensor b c)) 
     (associator_op a b c)) d
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
a, b, c, d: A
?Goal0 $==
fmap01 tensor a
  (cate_fun' (tensor (tensor b c) d)
     (tensor b (tensor c d)) 
     (associator_op b c d))
    2,3: exact (emap_inv _ _ $@ cate_buildequiv_fun _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
a, b, c, d: A
cate_fun' (tensor (tensor a b) (tensor c d))
  (tensor a (tensor b (tensor c d)))
  (associator_op a b (tensor c d)) $o
cate_fun' (tensor (tensor (tensor a b) c) d)
  (tensor (tensor a b) (tensor c d))
  (associator_op (tensor a b) c d) $==
(emap (tensor a) (cat_tensor_associator (b, c, d)))^-1$ $o
(cate_fun' (tensor (tensor a (tensor b c)) d)
   (tensor a (tensor (tensor b c) d))
   (associator_op a (tensor b c) d) $o
 (emap (flip tensor d)
    (cat_tensor_associator (a, b, c)))^-1$)
    refine ((cate_inv_compose' _ _)^$ $@ cate_inv2 _ $@ cate_inv_compose' _ _
      $@ (_ $@L cate_inv_compose' _ _)).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
a, b, c, d: A
cat_tensor_associator (tensor a b, c, d) $oE
cat_tensor_associator (a, b, tensor c d) $==
emap (flip tensor d) (cat_tensor_associator (a, b, c)) $oE
cat_tensor_associator (a, tensor b c, d) $oE
emap (tensor a) (cat_tensor_associator (b, c, d)) 
    refine (cate_buildequiv_fun _ $@ _ $@ ((cate_buildequiv_fun _)^$ $@R _)
      $@ (cate_buildequiv_fun _)^$).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
a, b, c, d: A
cat_tensor_associator (tensor a b, c, d) $o
cat_tensor_associator (a, b, tensor c d) $==
emap (flip tensor d) (cat_tensor_associator (a, b, c)) $o
cat_tensor_associator (a, tensor b c, d) $o
emap (tensor a) (cat_tensor_associator (b, c, d))
    refine (_ $@ (cate_buildequiv_fun _ $@@ (cate_buildequiv_fun _ $@R _))^$).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
a, b, c, d: A
cat_tensor_associator (tensor a b, c, d) $o
cat_tensor_associator (a, b, tensor c d) $==
fmap (flip tensor d) (cat_tensor_associator (a, b, c)) $o
cat_tensor_associator (a, tensor b c, d) $o
fmap (tensor a) (cat_tensor_associator (b, c, d))
    rapply cat_tensor_pentagon_identity.
Defined.

Definition ismonoidal_op' {A : Type} (tensor : A -> A -> A) (unit : A)
  `{HasEquivs A} `{!IsMonoidal A^op tensor unit}
  : IsMonoidal A tensor unit
  := ismonoidal_op (A:=A^op) tensor unit.

Instance issymmetricmonoidal_op {A : Type} (tensor : A -> A -> A) (unit : A)
  `{IsSymmetricMonoidal A tensor unit}
  : IsSymmetricMonoidal 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
H1: IsSymmetricMonoidal A tensor unit
IsSymmetricMonoidal A^op tensor unit
Proof.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
IsSymmetricMonoidal A^op tensor unit
  snapply Build_IsSymmetricMonoidal.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
IsMonoidal 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
H1: IsSymmetricMonoidal A tensor unit
SymmetricBraiding tensor
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
HexagonIdentity tensor
  -
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
IsMonoidal A^op tensor unit rapply ismonoidal_op.
  -
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
SymmetricBraiding tensor exact symmetricbraiding_op.
  -
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
HexagonIdentity tensor intros a b c; unfold op in a, b, c; simpl.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
fmap01 tensor b (braiding_op c a) $o
(cate_fun' (tensor (tensor b a) c)
   (tensor b (tensor a c)) 
   (associator_op b a c) $o
 fmap10 tensor (braiding_op b a) c) $==
cate_fun' (tensor (tensor b c) a)
  (tensor b (tensor c a)) 
  (associator_op b c a) $o
(braiding_op (tensor b c) a $o
 cate_fun' (tensor (tensor a b) c)
   (tensor a (tensor b c)) 
   (associator_op a b c))
    snrefine (_ $@ (_ $@L (_ $@R _))).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
fmap01 tensor b (braiding_op c a) $o
(cate_fun' (tensor (tensor b a) c)
   (tensor b (tensor a c)) 
   (associator_op b a c) $o
 fmap10 tensor (braiding_op b a) c) $==
cate_fun' (tensor (tensor b c) a)
  (tensor b (tensor c a)) 
  (associator_op b c a) $o
(?f $o
 cate_fun' (tensor (tensor a b) c)
   (tensor a (tensor b c)) 
   (associator_op a b c))
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
tensor a (tensor b c) $-> tensor (tensor b c) a
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
?f $== braiding_op (tensor b c) a
    2: exact ((braide _ _)^-1$).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
fmap01 tensor b (braiding_op c a) $o
(cate_fun' (tensor (tensor b a) c)
   (tensor b (tensor a c)) 
   (associator_op b a c) $o
 fmap10 tensor (braiding_op b a) c) $==
cate_fun' (tensor (tensor b c) a)
  (tensor b (tensor c a)) 
  (associator_op b c a) $o
((braide (tensor b c) a)^-1$ $o
 cate_fun' (tensor (tensor a b) c)
   (tensor a (tensor b c)) 
   (associator_op a b c))
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
(braide (tensor b c) a)^-1$ $==
braiding_op (tensor b c) a
    2: {
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
(braide (tensor b c) a)^-1$ $==
braiding_op (tensor b c) a napply cate_moveR_V1.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
Id (tensor a (tensor b c)) $==
braide (tensor b c) a $o braiding_op (tensor b c) a
      symmetry.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
braide (tensor b c) a $o braiding_op (tensor b c) a $==
Id (tensor a (tensor b c))
      nrefine ((_ $@R _) $@ _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
braide (tensor b c) a $== ?Goal0
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
?Goal0 $o braiding_op (tensor b c) a $==
Id (tensor a (tensor b c))
      1: napply cate_buildequiv_fun.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
cat_symm_tensor_braiding (tensor b c) a $o
braiding_op (tensor b c) a $==
Id (tensor a (tensor b c))
      rapply braid_braid. }
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
fmap01 tensor b (braiding_op c a) $o
(cate_fun' (tensor (tensor b a) c)
   (tensor b (tensor a c)) 
   (associator_op b a c) $o
 fmap10 tensor (braiding_op b a) c) $==
cate_fun' (tensor (tensor b c) a)
  (tensor b (tensor c a)) 
  (associator_op b c a) $o
((braide (tensor b c) a)^-1$ $o
 cate_fun' (tensor (tensor a b) c)
   (tensor a (tensor b c)) 
   (associator_op a b c))
    snrefine ((_ $@R _) $@ _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
tensor b (tensor a c) $-> tensor b (tensor c a)
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
fmap01 tensor b (braiding_op c a) $== ?g
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
?g $o
(cate_fun' (tensor (tensor b a) c)
   (tensor b (tensor a c)) 
   (associator_op b a c) $o
 fmap10 tensor (braiding_op b a) c) $==
cate_fun' (tensor (tensor b c) a)
  (tensor b (tensor c a)) 
  (associator_op b c a) $o
((braide (tensor b c) a)^-1$ $o
 cate_fun' (tensor (tensor a b) c)
   (tensor a (tensor b c)) 
   (associator_op a b c))
    {
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
tensor b (tensor a c) $-> tensor b (tensor c a) refine (emap _ _)^-1$.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
tensor c a $<~> tensor a c
      rapply braide. }
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
fmap01 tensor b (braiding_op c a) $==
(emap (tensor b) (braide c a))^-1$
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
(emap (tensor b) (braide c a))^-1$ $o
(cate_fun' (tensor (tensor b a) c)
   (tensor b (tensor a c)) 
   (associator_op b a c) $o
 fmap10 tensor (braiding_op b a) c) $==
cate_fun' (tensor (tensor b c) a)
  (tensor b (tensor c a)) 
  (associator_op b c a) $o
((braide (tensor b c) a)^-1$ $o
 cate_fun' (tensor (tensor a b) c)
   (tensor a (tensor b c)) 
   (associator_op a b c))
    {
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
fmap01 tensor b (braiding_op c a) $==
(emap (tensor b) (braide c a))^-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
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
(emap (tensor b) (braide c a))^-1$ $==
fmap01 tensor b (braiding_op c a)
      refine (cate_inv_adjointify _ _ _ _ $@ fmap2 _ _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
(braide c a)^-1$ $== braiding_op c a
      napply cate_inv_adjointify. }
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
(emap (tensor b) (braide c a))^-1$ $o
(cate_fun' (tensor (tensor b a) c)
   (tensor b (tensor a c)) 
   (associator_op b a c) $o
 fmap10 tensor (braiding_op b a) c) $==
cate_fun' (tensor (tensor b c) a)
  (tensor b (tensor c a)) 
  (associator_op b c a) $o
((braide (tensor b c) a)^-1$ $o
 cate_fun' (tensor (tensor a b) c)
   (tensor a (tensor b c)) 
   (associator_op a b c))
    snrefine ((_ $@L (_ $@L _)) $@ _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
tensor (tensor a b) c $-> tensor (tensor b a) c
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
fmap10 tensor (braiding_op b a) c $== ?g
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
(emap (tensor b) (braide c a))^-1$ $o
(cate_fun' (tensor (tensor b a) c)
   (tensor b (tensor a c)) 
   (associator_op b a c) $o 
 ?g) $==
cate_fun' (tensor (tensor b c) a)
  (tensor b (tensor c a)) 
  (associator_op b c a) $o
((braide (tensor b c) a)^-1$ $o
 cate_fun' (tensor (tensor a b) c)
   (tensor a (tensor b c)) 
   (associator_op a b c))
    {
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
tensor (tensor a b) c $-> tensor (tensor b a) c refine (emap (flip tensor c) _)^-1$.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
tensor b a $<~> tensor a b
      rapply braide. }
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
fmap10 tensor (braiding_op b a) c $==
(emap (flip tensor c) (braide b a))^-1$
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
(emap (tensor b) (braide c a))^-1$ $o
(cate_fun' (tensor (tensor b a) c)
   (tensor b (tensor a c)) 
   (associator_op b a c) $o
 (emap (flip tensor c) (braide b a))^-1$) $==
cate_fun' (tensor (tensor b c) a)
  (tensor b (tensor c a)) 
  (associator_op b c a) $o
((braide (tensor b c) a)^-1$ $o
 cate_fun' (tensor (tensor a b) c)
   (tensor a (tensor b c)) 
   (associator_op a b c))
    {
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
fmap10 tensor (braiding_op b a) c $==
(emap (flip tensor c) (braide b a))^-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
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
(emap (flip tensor c) (braide b a))^-1$ $==
fmap10 tensor (braiding_op b a) c
      refine (cate_inv_adjointify _ _ _ _ $@ fmap2 _ _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
(braide b a)^-1$ $== braiding_op b a
      napply cate_inv_adjointify. }
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
(emap (tensor b) (braide c a))^-1$ $o
(cate_fun' (tensor (tensor b a) c)
   (tensor b (tensor a c)) 
   (associator_op b a c) $o
 (emap (flip tensor c) (braide b a))^-1$) $==
cate_fun' (tensor (tensor b c) a)
  (tensor b (tensor c a)) 
  (associator_op b c a) $o
((braide (tensor b c) a)^-1$ $o
 cate_fun' (tensor (tensor a b) c)
   (tensor a (tensor b c)) 
   (associator_op a b c))
    refine ((_ $@L _)^$ $@ _^$ $@ cate_inv2 _ $@ _ $@ (_ $@L _)).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
?Goal $==
cate_fun' (tensor (tensor b a) c)
  (tensor b (tensor a c)) 
  (associator_op b a c) $o
(emap (flip tensor c) (braide b a))^-1$
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
?Goal2^-1$ $->
(emap (tensor b) (braide c a))^-1$ $o ?Goal
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
?Goal2 $== ?Goal3
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
?Goal3^-1$ $==
cate_fun' (tensor (tensor b c) a)
  (tensor b (tensor c a)) 
  (associator_op b c a) $o 
?Goal6
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
?Goal6 $==
(braide (tensor b c) a)^-1$ $o
cate_fun' (tensor (tensor a b) c)
  (tensor a (tensor b c)) 
  (associator_op a b c)
    1,2,4,5: rapply cate_inv_compose'.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
emap (flip tensor c) (braide b a) $oE
cat_tensor_associator (b, a, c) $oE
emap (tensor b) (braide c a) $==
cat_tensor_associator (a, b, c) $oE
braide (tensor b c) a $oE
cat_tensor_associator (b, c, a)
    refine (_ $@ (_ $@@ _) $@ _ $@ (_ $@R _)^$ $@ _^$).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
emap (flip tensor c) (braide b a) $oE
cat_tensor_associator (b, a, c) $oE
emap (tensor b) (braide c a) $== 
?Goal3 $o ?Goal1
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
?Goal1 $== ?Goal2
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
?Goal3 $== ?Goal4
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
?Goal4 $o ?Goal2 $== ?Goal10 $o ?Goal12
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
?Goal9 $== ?Goal10
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
cat_tensor_associator (a, b, c) $oE
braide (tensor b c) a $oE
cat_tensor_associator (b, c, a) $-> 
?Goal9 $o ?Goal12
    1-3,5-6: rapply cate_buildequiv_fun.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
emap (flip tensor c) (braide b a) $o
cat_tensor_associator (b, a, c) $o
fmap (tensor b) (braide c a) $==
cat_tensor_associator (a, b, c) $o
braide (tensor b c) a $o
cat_tensor_associator (b, c, a)
    refine ((fmap02 _ _ _ $@@ ((_ $@ fmap20 _ _ _) $@R _)) $@ cat_symm_tensor_hexagon a b c $@ ((_ $@L _^$) $@R _)).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
braide c a $== cat_symm_tensor_braiding c a
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
emap (flip tensor c) (braide b a) $==
fmap10 tensor ?Goal1 c
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
?Goal1 $== cat_symm_tensor_braiding b a
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsSymmetricMonoidal A tensor unit
a, b, c: A
braide (tensor b c) a $->
cat_symm_tensor_braiding (tensor b c) a
    1-4: napply cate_buildequiv_fun.
Defined.

Definition issymmetricmonoidal_op' {A : Type} (tensor : A -> A -> A) (unit : A)
  `{HasEquivs A} `{H' : !IsSymmetricMonoidal A^op tensor unit}
  : IsSymmetricMonoidal A tensor unit
  := issymmetricmonoidal_op (A:=A^op) tensor unit.

(** ** Further Coherence Conditions *)
(** In Mac Lane's original axiomatisation of a monoidal category, 3 extra coherence conditions were given in addition to the pentagon and triangle identities. It was later shown by Kelly that these axioms are redundant and follow from the rest. We reproduce these arguments here. *)

(** The left unitor of a tensor can be decomposed as an associator and a functorial action of the tensor on a left unitor. *)
Definition left_unitor_associator {A} (tensor : A -> A -> A) (unit : A)
  `{IsMonoidal A tensor unit} (x y : A)
  : (left_unitor (tensor x y) : _ $-> _)
    $== fmap10 tensor (left_unitor x) y $o associator unit x y.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
(cat_tensor_left_unitor (tensor x y)
 :
 tensor unit (tensor x y) $-> tensor x y) $==
fmap10 tensor (cat_tensor_left_unitor x) y $o
cat_tensor_associator unit x y
Proof.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
(cat_tensor_left_unitor (tensor x y)
 :
 tensor unit (tensor x y) $-> tensor x y) $==
fmap10 tensor (cat_tensor_left_unitor x) y $o
cat_tensor_associator unit x y
  refine ((cate_moveR_eV _ _ _ (isnat_natequiv left_unitor _))^$
    $@ ((_ $@L _) $@R _) $@ cate_moveR_eV _ _ _ (isnat_natequiv left_unitor _)).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
fmap (tensor unit)
  (cate_fun' (tensor unit (tensor x y)) 
     (tensor x y)
     (cat_tensor_left_unitor (tensor x y))) $==
fmap (tensor unit)
  (fmap10 tensor (cat_tensor_left_unitor x) y $o
   cat_tensor_associator unit x y)
  refine (_ $@ (fmap01_comp _ _ _ _)^$).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
fmap (tensor unit)
  (cate_fun' (tensor unit (tensor x y)) 
     (tensor x y)
     (cat_tensor_left_unitor (tensor x y))) $==
fmap01 tensor unit
  (fmap10 tensor (cat_tensor_left_unitor x) y) $o
fmap01 tensor unit (cat_tensor_associator unit x y)
  refine (_ $@ (cate_moveR_Ve _ _ _ (associator_nat_m _  _ _)^$ $@R _)).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
fmap (tensor unit)
  (cate_fun' (tensor unit (tensor x y)) 
     (tensor x y)
     (cat_tensor_left_unitor (tensor x y))) $==
(cat_tensor_associator unit x y)^-1$ $o
(fmap10 tensor
   (fmap01 tensor unit (cat_tensor_left_unitor x)) y $o
 cat_tensor_associator unit (tensor unit x) y) $o
fmap01 tensor unit (cat_tensor_associator unit x y)
  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
H1: IsMonoidal A tensor unit
x, y: A
fmap (tensor unit)
  (cate_fun' (tensor unit (tensor x y)) 
     (tensor x y)
     (cat_tensor_left_unitor (tensor x y))) $==
(cat_tensor_associator unit x y)^-1$ $o
(fmap10 tensor
   (fmap01 tensor unit (cat_tensor_left_unitor x)) y $o
 cat_tensor_associator unit (tensor unit x) y $o
 fmap01 tensor unit (cat_tensor_associator unit x y))
  change (fmap (tensor ?x) ?f) with (fmap01 tensor x f).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
fmap01 tensor unit
  (cate_fun' (tensor unit (tensor x y)) 
     (tensor x y)
     (cat_tensor_left_unitor (tensor x y))) $==
(cat_tensor_associator unit x y)^-1$ $o
(fmap10 tensor
   (fmap01 tensor unit (cat_tensor_left_unitor x)) y $o
 cat_tensor_associator unit (tensor unit x) y $o
 fmap01 tensor unit (cat_tensor_associator unit x y))
  change (cate_fun' _ _ (cat_tensor_left_unitor ?x))
    with (cate_fun (cat_tensor_left_unitor x)).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
fmap01 tensor unit
  (cat_tensor_left_unitor (tensor x y)) $==
(cat_tensor_associator unit x y)^-1$ $o
(fmap10 tensor
   (fmap01 tensor unit (cat_tensor_left_unitor x)) y $o
 cat_tensor_associator unit (tensor unit x) y $o
 fmap01 tensor unit (cat_tensor_associator unit x y))
  apply 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
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator unit x y $o
fmap01 tensor unit
  (cat_tensor_left_unitor (tensor x y)) $==
fmap10 tensor
  (fmap01 tensor unit (cat_tensor_left_unitor x)) y $o
cat_tensor_associator unit (tensor unit x) y $o
fmap01 tensor unit (cat_tensor_associator unit x y)
  refine ((_ $@L triangle_identity _ _ _ _ _ _) $@ _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator unit x y $o
(fmap10 tensor (cat_tensor_right_unitor unit)
   (tensor x y) $o
 cat_tensor_associator unit unit (tensor x y)) $==
fmap10 tensor
  (fmap01 tensor unit (cat_tensor_left_unitor x)) y $o
cat_tensor_associator unit (tensor unit x) y $o
fmap01 tensor unit (cat_tensor_associator unit x y)
  nrefine (cat_assoc_opp _ _ _ $@ _ $@ 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
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator unit x y $o
fmap10 tensor (cat_tensor_right_unitor unit)
  (tensor x y) $o
cat_tensor_associator unit unit (tensor x y) $==
fmap10 tensor
  (fmap01 tensor unit (cat_tensor_left_unitor x)) y $o
(cat_tensor_associator unit (tensor unit x) y $o
 fmap01 tensor unit (cat_tensor_associator unit x y))
  refine (_ $@ ((fmap20 _ (triangle_identity _ _ _ _ _ _) _
    $@ fmap10_comp _ _ _ _)^$ $@R _)).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator unit x y $o
fmap10 tensor (cat_tensor_right_unitor unit)
  (tensor x y) $o
cat_tensor_associator unit unit (tensor x y) $==
fmap10 tensor
  (fmap10 tensor (cat_tensor_right_unitor unit) x) y $o
fmap10 tensor (cat_tensor_associator unit unit x) y $o
(cat_tensor_associator unit (tensor unit x) y $o
 fmap01 tensor unit (cat_tensor_associator unit x y))
  refine (_ $@ 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
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator unit x y $o
fmap10 tensor (cat_tensor_right_unitor unit)
  (tensor x y) $o
cat_tensor_associator unit unit (tensor x y) $==
fmap10 tensor
  (fmap10 tensor (cat_tensor_right_unitor unit) x) y $o
(fmap10 tensor (cat_tensor_associator unit unit x) y $o
 (cat_tensor_associator unit (tensor unit x) y $o
  fmap01 tensor unit (cat_tensor_associator unit x y)))
  refine (_ $@ (_ $@L (pentagon_identity _ _ _ _ _ _ $@ 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
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator unit x y $o
fmap10 tensor (cat_tensor_right_unitor unit)
  (tensor x y) $o
cat_tensor_associator unit unit (tensor x y) $==
fmap10 tensor
  (fmap10 tensor (cat_tensor_right_unitor unit) x) y $o
(cat_tensor_associator (tensor unit unit) x y $o
 cat_tensor_associator unit unit (tensor x y))
  refine ((_ $@R _) $@ 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
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator unit x y $o
fmap10 tensor (cat_tensor_right_unitor unit)
  (tensor x y) $==
fmap10 tensor
  (fmap10 tensor (cat_tensor_right_unitor unit) x) y $o
cat_tensor_associator (tensor unit unit) x y
  exact (associator_nat_l _ _ _).
Defined.

(** The right unitor of a tensor can be decomposed as an inverted associator and a functorial action of the tensor on a right unitor. *)
Definition right_unitor_associator {A} (tensor : A -> A -> A) (unit : A)
  `{IsMonoidal A tensor unit} (x y : A)
  : (fmap01 tensor x (right_unitor y) : _ $-> _)
    $== right_unitor (tensor x y) $o associator x y unit.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
(fmap01 tensor x (cat_tensor_right_unitor y)
 :
 tensor x (flip tensor unit y) $-> tensor x y) $==
cat_tensor_right_unitor (tensor x y) $o
cat_tensor_associator x y unit
Proof.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
(fmap01 tensor x (cat_tensor_right_unitor y)
 :
 tensor x (flip tensor unit y) $-> tensor x y) $==
cat_tensor_right_unitor (tensor x y) $o
cat_tensor_associator x y unit
  refine ((cate_moveR_eV _ _ _ (isnat_natequiv right_unitor _))^$
    $@ ((_ $@L _) $@R _) $@ cate_moveR_eV _ _ _ (isnat_natequiv right_unitor _)).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
fmap (flip tensor unit)
  (fmap (tensor x) (cat_tensor_right_unitor y)) $==
fmap (flip tensor unit)
  (cat_tensor_right_unitor (tensor x y) $o
   cat_tensor_associator x y unit)
  refine (_ $@ (fmap10_comp tensor _ _ _)^$).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
fmap (flip tensor unit)
  (fmap (tensor x) (cat_tensor_right_unitor y)) $==
fmap10 tensor (cat_tensor_right_unitor (tensor x y))
  unit $o
fmap10 tensor (cat_tensor_associator x y unit) unit
  refine ((cate_moveR_eV _ _ _ (associator_nat_m _ _ _))^$ $@ _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator x y unit $o
fmap01 tensor x
  (fmap10 tensor (cat_tensor_right_unitor y) unit) $o
(cat_tensor_associator x (flip tensor unit y) unit)^-1$ $==
fmap10 tensor (cat_tensor_right_unitor (tensor x y))
  unit $o
fmap10 tensor (cat_tensor_associator x y unit) unit
  refine (_ $@ (cate_moveR_eV _ _ _ (triangle_identity _ _ _ _ _ _) $@R _)).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator x y unit $o
fmap01 tensor x
  (fmap10 tensor (cat_tensor_right_unitor y) unit) $o
(cat_tensor_associator x (flip tensor unit y) unit)^-1$ $==
fmap01 tensor (tensor x y)
  (cat_tensor_left_unitor unit) $o
(cat_tensor_associator (tensor x y) unit unit)^-1$ $o
fmap10 tensor (cat_tensor_associator x y unit) unit
  apply 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
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator x y unit $o
fmap01 tensor x
  (fmap10 tensor (cat_tensor_right_unitor y) unit) $==
fmap01 tensor (tensor x y)
  (cat_tensor_left_unitor unit) $o
(cat_tensor_associator (tensor x y) unit unit)^-1$ $o
fmap10 tensor (cat_tensor_associator x y unit) unit $o
cat_tensor_associator x (flip tensor unit y) unit
  refine ((_ $@L
    (fmap02 _ _ (cate_moveR_eV _ _ _ (triangle_identity _ _ _ _ _ _))^$
    $@ fmap01_comp _ _ _ _)) $@ _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator x y unit $o
(fmap01 tensor x
   (fmap01 tensor y (cat_tensor_left_unitor unit)) $o
 fmap01 tensor x
   (cat_tensor_associator y unit unit)^-1$) $==
fmap01 tensor (tensor x y)
  (cat_tensor_left_unitor unit) $o
(cat_tensor_associator (tensor x y) unit unit)^-1$ $o
fmap10 tensor (cat_tensor_associator x y unit) unit $o
cat_tensor_associator x (flip tensor unit y) unit
  refine (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
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator x y unit $o
fmap01 tensor x
  (fmap01 tensor y (cat_tensor_left_unitor unit)) $o
fmap01 tensor x
  (cat_tensor_associator y unit unit)^-1$ $==
fmap01 tensor (tensor x y)
  (cat_tensor_left_unitor unit) $o
(cat_tensor_associator (tensor x y) unit unit)^-1$ $o
fmap10 tensor (cat_tensor_associator x y unit) unit $o
cat_tensor_associator x (flip tensor unit y) unit
  nrefine ((associator_nat_r _ _ _ $@R _) $@ 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
H1: IsMonoidal A tensor unit
x, y: A
fmap01 tensor (tensor x y)
  (cat_tensor_left_unitor unit) $o
(cat_tensor_associator x y (tensor unit unit) $o
 fmap01 tensor x
   (cat_tensor_associator y unit unit)^-1$) $==
fmap01 tensor (tensor x y)
  (cat_tensor_left_unitor unit) $o
(cat_tensor_associator (tensor x y) unit unit)^-1$ $o
fmap10 tensor (cat_tensor_associator x y unit) unit $o
cat_tensor_associator x (flip tensor unit y) unit
  do 2 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
H1: IsMonoidal A tensor unit
x, y: A
fmap01 tensor (tensor x y)
  (cat_tensor_left_unitor unit) $o
(cat_tensor_associator x y (tensor unit unit) $o
 fmap01 tensor x
   (cat_tensor_associator y unit unit)^-1$) $==
fmap01 tensor (tensor x y)
  (cat_tensor_left_unitor unit) $o
((cat_tensor_associator (tensor x y) unit unit)^-1$ $o
 (fmap10 tensor (cat_tensor_associator x y unit) unit $o
  cat_tensor_associator x (flip tensor unit y) unit))
  refine (_ $@L _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator x y (tensor unit unit) $o
fmap01 tensor x
  (cat_tensor_associator y unit unit)^-1$ $==
(cat_tensor_associator (tensor x y) unit unit)^-1$ $o
(fmap10 tensor (cat_tensor_associator x y unit) unit $o
 cat_tensor_associator x (flip tensor unit y) unit)
  refine ((_ $@L (emap_inv' _ _)^$) $@ _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator x y (tensor unit unit) $o
(emap (tensor x) (cat_tensor_associator y unit unit))^-1$ $==
(cat_tensor_associator (tensor x y) unit unit)^-1$ $o
(fmap10 tensor (cat_tensor_associator x y unit) unit $o
 cat_tensor_associator x (flip tensor unit y) unit)
  apply 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
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator x y (tensor unit unit) $==
(cat_tensor_associator (tensor x y) unit unit)^-1$ $o
(fmap10 tensor (cat_tensor_associator x y unit) unit $o
 cat_tensor_associator x (flip tensor unit y) unit) $o
emap (tensor x) (cat_tensor_associator y unit unit)
  refine (_ $@ (_ $@L cate_buildequiv_fun _)^$).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator x y (tensor unit unit) $==
(cat_tensor_associator (tensor x y) unit unit)^-1$ $o
(fmap10 tensor (cat_tensor_associator x y unit) unit $o
 cat_tensor_associator x (flip tensor unit y) unit) $o
fmap (tensor x) (cat_tensor_associator y unit unit)
  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
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator x y (tensor unit unit) $==
(cat_tensor_associator (tensor x y) unit unit)^-1$ $o
(fmap10 tensor (cat_tensor_associator x y unit) unit $o
 cat_tensor_associator x (flip tensor unit y) unit $o
 fmap (tensor x) (cat_tensor_associator y unit unit))
  apply 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
H1: IsMonoidal A tensor unit
x, y: A
cat_tensor_associator (tensor x y) unit unit $o
cat_tensor_associator x y (tensor unit unit) $==
fmap10 tensor (cat_tensor_associator x y unit) unit $o
cat_tensor_associator x (flip tensor unit y) unit $o
fmap (tensor x) (cat_tensor_associator y unit unit)
  rapply pentagon_identity.
Defined.

(** The left unitor at the unit is the right unitor at the unit. *)
Definition left_unitor_unit_right_unitor_unit {A} (tensor : A -> A -> A) (unit : A)
  `{IsMonoidal A tensor unit}
  : (left_unitor unit : tensor unit unit $-> _) $== right_unitor unit.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
(cat_tensor_left_unitor unit
 :
 tensor unit unit $-> unit) $==
cat_tensor_right_unitor unit
Proof.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
(cat_tensor_left_unitor unit
 :
 tensor unit unit $-> unit) $==
cat_tensor_right_unitor unit
  refine ((cate_moveR_eV _ _ _ (isnat_natequiv left_unitor (left_unitor unit)))^$
    $@ _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
cat_tensor_left_unitor unit $o
fmap (tensor unit) (cat_tensor_left_unitor unit) $o
(cat_tensor_left_unitor (tensor unit unit))^-1$ $==
cat_tensor_right_unitor unit
  apply 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
H1: IsMonoidal A tensor unit
cat_tensor_left_unitor unit $o
fmap (tensor unit) (cat_tensor_left_unitor unit) $==
cat_tensor_right_unitor unit $o
cat_tensor_left_unitor (tensor unit unit)
  refine (_ $@ (_ $@L left_unitor_associator _ _ _ _)^$).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
cat_tensor_left_unitor unit $o
fmap (tensor unit) (cat_tensor_left_unitor unit) $==
cat_tensor_right_unitor unit $o
(fmap10 tensor (cat_tensor_left_unitor unit) unit $o
 cat_tensor_associator unit unit unit)
  nrefine (_ $@ (_ $@R _) $@ 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
H1: IsMonoidal A tensor unit
cat_tensor_left_unitor unit $o
fmap (tensor unit) (cat_tensor_left_unitor unit) $==
?Goal0 $o cat_tensor_associator unit unit unit
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
?Goal0 $==
cat_tensor_right_unitor unit $o
fmap10 tensor (cat_tensor_left_unitor unit) unit 
  2: exact (isnat_natequiv right_unitor _)^$.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
cat_tensor_left_unitor unit $o
fmap (tensor unit) (cat_tensor_left_unitor unit) $==
fmap idmap (cat_tensor_left_unitor unit) $o
(fun a : A => cate_fun (cat_tensor_right_unitor a))
  (tensor unit unit) $o
cat_tensor_associator unit unit unit
  nrefine ((_ $@L _) $@ 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
H1: IsMonoidal A tensor unit
fmap (tensor unit) (cat_tensor_left_unitor unit) $==
cat_tensor_right_unitor (tensor unit unit) $o
cat_tensor_associator unit unit unit
  refine (triangle_identity _ _ _ _ _ _ $@ _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
fmap10 tensor (cat_tensor_right_unitor unit) unit $o
cat_tensor_associator unit unit unit $==
cat_tensor_right_unitor (tensor unit unit) $o
cat_tensor_associator unit unit unit
  nrefine (_ $@R _).
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
fmap10 tensor (cat_tensor_right_unitor unit) unit $==
cat_tensor_right_unitor (tensor unit unit)
  napply cate_monic_equiv.
A: Type
tensor: A -> A -> A
unit: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
H1: IsMonoidal A tensor unit
?Goal1 $o
fmap10 tensor (cat_tensor_right_unitor unit) unit $==
?Goal1 $o cat_tensor_right_unitor (tensor unit unit)
  exact (isnat_natequiv right_unitor (right_unitor unit)).
Defined.

(** TODO: Kelly also shows that there are redundant coherence conditions for symmetric monoidal categories also, but we leave these out for now. *)

(** ** Monoidal functors *)

(** A (lax) monoidal functor [F] between two monoidal categories [A] and [B] is a functor [F : A -> B] together with: *)
Class IsMonoidalFunctor {A B : Type}
  {tensorA : A -> A -> A} {tensorB : B -> B -> B} {IA : A} {IB : B}
  `{IsMonoidal A tensorA IA, IsMonoidal B tensorB IB}
  (F : A -> B) `{!Is0Functor F, !Is1Functor F} := {

  (** A natural transformation [fmap_tensor] from [F a ⊗ F b] to [F (a ⊗ b)]. *)
  fmap_tensor
    : NatTrans
        (uncurry (fun a b => tensorB (F a) (F b)))
        (uncurry (fun a b => F (tensorA a b)));

  (** A morphism [fmap_unit] relating the two unit objects. *)
  fmap_unit : IB $-> F (IA);

  (** Such that the following coherence conditions hold: 

  [F] preserves the [associator]s in a suitable way. *)
  fmap_tensor_assoc a b c
    : fmap F (associator a b c)
        $o fmap_tensor (a, tensorA b c)
        $o fmap01 tensorB (F a) (fmap_tensor (b, c))
      $== fmap_tensor (tensorA a b, c)
        $o fmap10 tensorB (fmap_tensor (a, b)) (F c)
        $o associator (F a) (F b) (F c);

  (** [F] preserves the [left_unitor]s in a suitable way. *)
  fmap_tensor_left_unitor a
    : trans_nattrans left_unitor (F a)
      $== fmap F (left_unitor a)
        $o fmap_tensor (IA, a)
        $o fmap10 tensorB fmap_unit (F a);

  (** [F] preserves the [right_unitors]s in a suitable way. *)
  fmap_tensor_right_unitor a
    : trans_nattrans right_unitor (F a)
      $== fmap F (right_unitor a)
        $o fmap_tensor (a, IA)
        $o fmap01 tensorB (F a) fmap_unit;
}.

Arguments fmap_tensor {A B tensorA tensorB IA IB _ _ _ _ _ _ _ _ _ _ _ _}
  F {_ _ _}.

Definition fmap_tensor_nat {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 x' y y': A} (f : x $-> x') (g : y $-> y')
  : fmap_tensor F (x', y') $o fmap11 tensorB (fmap F f) (fmap F g)
    $== fmap F (fmap11 tensorA f g) $o fmap_tensor F (x, y).
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, x', y, y': A
f: x $-> x'
g: y $-> y'
fmap_tensor F (x', y') $o
fmap11 tensorB (fmap F f) (fmap F g) $==
fmap F (fmap11 tensorA f g) $o fmap_tensor F (x, y)
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, x', y, y': A
f: x $-> x'
g: y $-> y'
fmap_tensor F (x', y') $o
fmap11 tensorB (fmap F f) (fmap F g) $==
fmap F (fmap11 tensorA f g) $o fmap_tensor F (x, y)
  destruct (fmap_tensor F) as [fmap_tensor_F nat].
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, x', y, y': A
f: x $-> x'
g: y $-> y'
fmap_tensor_F: uncurry
  (fun a b : A => tensorB (F a) (F b)) $=>
uncurry
  (fun a b : A => F (tensorA a b))
nat: Is1Natural
  (uncurry (fun a b : A => tensorB (F a) (F b)))
  (uncurry (fun a b : A => F (tensorA a b)))
  fmap_tensor_F
{|
  trans_nattrans := fmap_tensor_F;
  is1natural_nattrans := nat
|} (x', y') $o fmap11 tensorB (fmap F f) (fmap F g) $==
fmap F (fmap11 tensorA f g) $o
{|
  trans_nattrans := fmap_tensor_F;
  is1natural_nattrans := nat
|} (x, y)
  exact (nat (x, y) (x', y') (f, g)).
Defined.

Definition fmap_tensor_nat_l {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 x' y : A} (f : x $-> x')
  : fmap_tensor F (x', y) $o fmap10 tensorB (fmap F f) (F y)
    $== fmap F (fmap10 tensorA f y) $o fmap_tensor F (x, y).
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, x', y: A
f: x $-> x'
fmap_tensor F (x', y) $o
fmap10 tensorB (fmap F f) (F y) $==
fmap F (fmap10 tensorA f y) $o fmap_tensor F (x, y)
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, x', y: A
f: x $-> x'
fmap_tensor F (x', y) $o
fmap10 tensorB (fmap F f) (F y) $==
fmap F (fmap10 tensorA f y) $o fmap_tensor F (x, y)
  refine ((_ $@L (fmap12 tensorB _ (fmap_id _ _)
    $@ fmap10_is_fmap11 _ _ _)^$) $@ _).
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, x', y: A
f: x $-> x'
fmap_tensor F (x', y) $o
fmap11 tensorB (fmap F f) (fmap F (Id (snd (x, y)))) $==
fmap F (fmap10 tensorA f y) $o fmap_tensor F (x, y) 
  refine (_ $@ (fmap2 F (fmap10_is_fmap11 _ _ _) $@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, x', y: A
f: x $-> x'
fmap_tensor F (x', y) $o
fmap11 tensorB (fmap F f) (fmap F (Id (snd (x, y)))) $==
fmap F (fmap11 tensorA f (Id (snd (x', y)))) $o
fmap_tensor F (x, y)
  snapply fmap_tensor_nat.
Defined.

Definition fmap_tensor_nat_r {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 y y' : A} (g : y $-> y')
  : fmap_tensor F (x, y') $o fmap01 tensorB (F x) (fmap F g)
    $== fmap F (fmap01 tensorA x g) $o fmap_tensor F (x, y).
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, y, y': A
g: y $-> y'
fmap_tensor F (x, y') $o
fmap01 tensorB (F x) (fmap F g) $==
fmap F (fmap01 tensorA x g) $o fmap_tensor F (x, y)
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, y, y': A
g: y $-> y'
fmap_tensor F (x, y') $o
fmap01 tensorB (F x) (fmap F g) $==
fmap F (fmap01 tensorA x g) $o fmap_tensor F (x, y)
  refine ((_ $@L (fmap21 tensorB (fmap_id _ _) _
    $@ fmap01_is_fmap11 _ _ _)^$) $@ _).
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, y, y': A
g: y $-> y'
fmap_tensor F (x, y') $o
fmap11 tensorB (fmap F (Id (fst (x, y)))) (fmap F g) $==
fmap F (fmap01 tensorA x g) $o fmap_tensor F (x, y)
  refine (_ $@ (fmap2 F (fmap01_is_fmap11 _ _ _) $@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, y, y': A
g: y $-> y'
fmap_tensor F (x, y') $o
fmap11 tensorB (fmap F (Id (fst (x, y)))) (fmap F g) $==
fmap F (fmap11 tensorA (Id (fst (x, y'))) g) $o
fmap_tensor F (x, y)
  snapply fmap_tensor_nat.
Defined.