Skip to content

Instantly share code, notes, and snippets.

@Icelandjack

Icelandjack/Applicative_failures.md Secret

Last active April 23, 2024 14:38
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Icelandjack/a95ec7413b0c7be60e70dd4b063d87ff to your computer and use it in GitHub Desktop.
Save Icelandjack/a95ec7413b0c7be60e70dd4b063d87ff to your computer and use it in GitHub Desktop.
Download ZIP
Ways of failing to be Applicative
Raw
Applicative_failures.md

I'm gathering some failures of the Applicative laws. One failure is enough to disqualify something from being Applicative but I got curious whether I could find all combinations of laws that fail.

data LR a = L | R

This was an interesting case. As others have noted this is the Const Bool, I initially started exploring this to understand Applicative sums mediated by Applicative morphisms.

Here is the result for Const ABC.

When we define a pure = const L it makes it the unit. This pins down how it interacts with <*>.

  L <*> b = b
  a <*> L = a

This fully determines three equations of <*>:

instance Applicative LR where
  pure = const L
  
  L <*> L = L
  L <*> R = R
  R <*> L = R
  R <*> R = ...

But the last equation can return R, or L:

  R <*> R = R
-- or
  R <*> R = L

The second one initially surprised me because I was thinking about LR as an Applicative not as a Monoidal Xor Bool with a phantom type.

I had been under the impression that all Applicative sums preserved the direction, if both operands were the same: L <*> L = L and R <*> R = R.

instance (Applicative l, Apply r) => Applicative (Sum l r) where
  pure a = InL . pure l
  InL fs <*> InL as = InL (fs <*> @l as)
  InR fs <*> InR as = InR (fs <*> @r as)
  ..

where mismatched sums L <*> R, or R <*> L were sent away from the identity case (pure) using an 'Applicative (homo)morphism', a function that preserves the Applicative structure.

  InL fs <*> InR as = InR (app fs <*> as)
  InR fs <*> InL as = InR (fs <*> app as)

As pointed out by Miyazato:

When the "Monoid of constructors" of an applicative is actually a Group, I think every Applicative morphisms here must be isomorphism (i.e. invertible.)

Here is how the rest of them fail

L L L L: Id
L L L R: Id
L L R L:    Comp      Inter
L L R R:              Inter
L R L L: Id Comp      Inter
L R L R: Id           Inter
L R R L:
L R R R:
R L L L: Id Comp Homo
R L L R: Id      Homo
R L R L: Id Comp Homo Inter
R L R R: Id Comp Homo Inter
R R L L: Id Comp Homo Inter
R R L R: Id Comp Homo Inter
R R R L: Id Comp Homo
R R R R: Id      Homo
Raw
failing_to_be_applicative.md

These are datatypes and their instances, by error subset:

fails: Identity Law

pure _ = L; L L L L: Id
pure _ = R; R R R R: Id

pure _ = L; L L L R: Id
pure _ = R; L R R R: Id
data V2 a = V2 a a

instance Applicative V2 where
  pure a = V2 a a
  V2 f g <*> V2 a b = V2 (f a) (f a)
or
  V2 f g <*> V2 a b = V2 (g b) (g b)
data V3 a = V3 a a a

instance Applicative V3 where
  pure a = V3 a a a
  V3 f g h <*> V3 a b c = V3 (f a) (f a) (f a)
instance Applicative Maybe where
  pure _ = Nothing
  _ <*> _ = Nothing
data Opt a = None String | Some a
  deriving stock (Eq, Show, Functor)
instance Applicative Opt where
  pure :: a -> Opt a
  pure = Some

  Some f <*> Some a = Some (f a)
  None str <*> Some a = None ""
  Some f <*> None str' = None ""
  None str <*> None str' = None (str <> str')
newtype L a = L [a]

instance Applicative L where
  pure a = L []
  L fs <*> L as = L (fs <*> as)

fails: Identity, Composition

data V2 a = V2 a a
  deriving stock (Eq, Show, Functor)

instance Applicative V2 where
  pure a = V2 a a
  V2 f g <*> V2 a b = V2 (g b) (f a)
data Opt a = None String | Some a
  deriving stock (Eq, Show, Functor)

instance Applicative Opt where
  pure = Some
  Some f <*> Some a = Some (f a)
  None str <*> Some a = None ""
  Some f <*> None str' = None ""
  None str <*> None str' = None (str <> str')
newtype L a = L [a]

instance Applicative L where
  pure a = L []
or
  pure a = L [a]
  L fs <*> L as = L (reverse (fs <*> as))
newtype Inf a = Inf [a]
  deriving newtype (Eq, Show, Arbitrary, Functor)

instance Applicative Inf where
  pure a = Inf [a]

  Inf (f:g:gs) <*> Inf (a:b:bs) = Inf (g b:f a:(gs <*> bs))
  Inf fs <*> Inf as = Inf (zipWith id fs as)

fails: Identity, Composition, Interchange

pure _ = L, L R L L: Id, Comp, Inter, Comm
pure _ = R, R R L R: Id, Comp, Inter, Comm
data V2 a = V2 a a

instance Applicative F where
  pure a = F a a
  F f g <*> F a b = F (f b) (f a)
or
  F f g <*> F a b = F (f b) (f b)
or
  F f g <*> F a b = F (f b) (g a)
or
  F f g <*> F a b = F (g a) (f a)
or
  F f g <*> F a b = F (g a) (g a)
or
  F f g <*> F a b = F (g b) (f b)
or
  F f g <*> F a b = F (g b) (g a)
data V3 a = V3 a a a

instance Applicative F where
  pure a = F a a a
  F f g h <*> F a b c = F (f a) (f a) (f b)
data Opt a = None String | Some a
  deriving stock (Eq, Show, Functor)

instance Applicative Opt where
  pure = Some
  Some f <*> Some a = Some (f a)

fails: Identity, Composition, Homomorphism

pure _ = L; R L L L: Id, Comp, Homo
pure _ = R; R R R L: Id, Comp, Homo

pure _ = L; R R R L: Id, Comp, Homo
pure _ = R; R L L L: Id, Comp, Homo
```haskell

```haskell
data Strs a = Strs String String
  deriving stock (Eq, Show, Functor)

instance Applicative Strs where
  pure _ = Strs "" ""
  Strs s s' <*> Strs s1 s1' = Strs "okokok" (s <> s1)

fails: Identity, Composition, Homomorphism, Interchange

pure _ = L; R L R L: Id, Comp, Homo, Inter, Comm
pure _ = R; R L R L: Id, Comp, Homo, Inter, Comm

pure _ = L; R L R R: Id, Comp, Homo, Inter, Comm
pure _ = R; L L R L: Id, Comp, Homo, Inter, Comm

pure _ = L; R R L L: Id, Comp, Homo, Inter, Comm
pure _ = R; R R L L: Id, Comp, Homo, Inter, Comm

pure _ = L; R R L R: Id, Comp, Homo, Inter, Comm
pure _ = R; L R L L: Id, Comp, Homo, Inter, Comm
newtype L a = L [a]

instance Applicative L where
  pure a = L []
or
  pure a = L [a]
  L fs <*> L as = L (reverse (fs <*> as))

fails: Identity, Homomorphism

pure _ = L; R L L R: Id, Homo
pure _ = R; L R R L: Id, Homo

pure _ = L; R R R R: Id, Homo
pure _ = R; L L L L: Id, Homo
data F a = F String
  deriving stock (Eq, Show, Functor)

instance Applicative F where
  pure _ = F ""
  F str <*> F str' = F "OK"
instance Applicative Maybe where
  pure = Just
  _ <*> _ = Nothing
data Strs a = Strs String String
  deriving stock (Eq, Show, Functor)

instance Applicative Strs where
  pure _ = Strs "" ""
  Strs s s' <*> Strs s1 s1' = Strs (s <> s1) "okokok"

fails: Identity, Homomorphism, Interchange

data F a = F String a a

instance Applicative F where
  pure a = F "ok" a a
  F str f g <*> F str' a b = F (str <> str') (f a) (g b)
newtype L a = L [a]

instance Applicative L where
  pure a = L [a,a]
or
  pure a = L [a,a,a]
  L fs <*> L as = L (fs <*> as)

fails: Identity, Interchange

pure _ = L, L R L R: Id, Inter, Comm
pure _ = R, L R L R: Id, Inter, Comm
data F a = L String a a
  deriving stock (Eq, Show, Functor)

instance Applicative F where
  pure a = L "" a a
  L str f g <*> L str' a b = L str (f a) (g b)
data F a = L String
  deriving stock (Eq, Show, Functor)

instance Applicative F where
  pure _ = L "", or L "OOHH"
  L str <*> L str' = L str
data V2 a = V2 a a

instance Applicative V2 where
  pure a = V2 a a
  V2 f g <*> V2 a b = V2 (f a) (g a)
or
  V2 f g <*> V2 a b = V2 (f b) (g b)
data V3 a = V3 a a a

instance Applicative V3 where
  pure a = V3 a a a
  V3 f g h <*> V3 a b c = V3 (f a) (f a) (f c)

fails: Composition, Interchange

pure _ = L, L L R L: Comp, Inter, Comm
pure _ = R, R L R R: Comp, Inter, Comm
data V2 a = V2 a a

instance Applicative V2 where
  pure a = V2 a a
  V2 f g <*> V2 a b = V2 (g a) (f b)
data Opt a = None String | Some a
  deriving stock (Eq, Show, Functor)

instance Applicative Opt where
  pure :: a -> Opt a
  pure = Some

  Some f <*> Some a = Some (f a)
  None str <*> Some a = None ""
  Some f <*> None str' = None str'
  None str <*> None str' = None (str <> str')

fails: Interchange

pure _ = L, L L R R: Inter, Comm
pure _ = R, L L R R: Inter, Comm
data F a = L String
  deriving stock (Eq, Show, Functor)

instance Applicative F where
  pure _ = L "" -- or L "OOOH"
  L str <*> L str' = L str'
data V2 a = V2 a a
  deriving stock (Eq, Show, Functor)

instance Applicative V2 where
  pure a = V2 a a
  V2 f g <*> V2 a b = V2 (f a) (f b)
or
  V2 f g <*> V2 a b = V2 (g a) (g b)
data Inf a = Inf String a deriving stock (Eq, Show, Generic, Functor)

instance Arbitrary a => Arbitrary (Inf a) where
  arbitrary = Inf <$> arbitrary <*> arbitrary

instance Applicative Inf where
  pure = Inf mempty
  Inf str f <*> Inf str' a = Inf str' (f a)
``
Raw
V3.md

data V3 a = V3 a a a

Another simple type.

The pure function is uniquely determined

instance Applicative V3 where
  pure a = V3 a a a

  V3 f g a <*> V3 a b c = ..

But there are multiple valid permutations of the right-hand side. Only one gives a correct Applicative definition,

  1: 
 17:    Comp Inter WeakCommutativity
  9: Id 
 17: Id Comp
637: Id Comp Inter WeakCommutativity
 39: Id      Inter WeakCommutativity
  9:         Inter WeakCommutativity
 = V3 (f a) (f a) (f a): Id
 = V3 (f a) (f a) (f b): Id Comp Inter WeakCommutativity
 = V3 (f a) (f a) (f c): Id      Inter WeakCommutativity
 = V3 (f a) (f a) (g a): Id Comp Inter WeakCommutativity
 = V3 (f a) (f a) (g b): Id Comp
 = V3 (f a) (f a) (g c): Id Comp Inter WeakCommutativity
 = V3 (f a) (f a) (h a): Id      Inter WeakCommutativity
 = V3 (f a) (f a) (h b): Id Comp Inter WeakCommutativity
 = V3 (f a) (f a) (h c): Id
 = V3 (f a) (f b) (f a): Id      Inter WeakCommutativity
 = V3 (f a) (f b) (f b): Id      Inter WeakCommutativity
 = V3 (f a) (f b) (f c):         Inter WeakCommutativity
 = V3 (f a) (f b) (g a): Id Comp Inter WeakCommutativity
 = V3 (f a) (f b) (g b): Id Comp Inter WeakCommutativity
 = V3 (f a) (f b) (g c):    Comp Inter WeakCommutativity
 = V3 (f a) (f b) (h a): Id      Inter WeakCommutativity
 = V3 (f a) (f b) (h b): Id Comp Inter WeakCommutativity
 = V3 (f a) (f b) (h c):         Inter WeakCommutativity
 = V3 (f a) (f c) (f a): Id Comp Inter WeakCommutativity
 = V3 (f a) (f c) (f b): Id Comp Inter WeakCommutativity
 = V3 (f a) (f c) (f c): Id      Inter WeakCommutativity
 = V3 (f a) (f c) (g a): Id Comp Inter WeakCommutativity
 = V3 (f a) (f c) (g b): Id Comp Inter WeakCommutativity
 = V3 (f a) (f c) (g c): Id Comp Inter WeakCommutativity
 = V3 (f a) (f c) (h a): Id Comp Inter WeakCommutativity
 = V3 (f a) (f c) (h b): Id Comp Inter WeakCommutativity
 = V3 (f a) (f c) (h c): Id Comp Inter WeakCommutativity
 = V3 (f a) (g a) (f a): Id      Inter WeakCommutativity
 = V3 (f a) (g a) (f b): Id Comp Inter WeakCommutativity
 = V3 (f a) (g a) (f c): Id      Inter WeakCommutativity
 = V3 (f a) (g a) (g a): Id      Inter WeakCommutativity
 = V3 (f a) (g a) (g b): Id Comp Inter WeakCommutativity
 = V3 (f a) (g a) (g c): Id Comp Inter WeakCommutativity
 = V3 (f a) (g a) (h a): Id      Inter WeakCommutativity
 = V3 (f a) (g a) (h b): Id Comp Inter WeakCommutativity
 = V3 (f a) (g a) (h c): Id      Inter WeakCommutativity
 = V3 (f a) (g b) (f a): Id
 = V3 (f a) (g b) (f b): Id Comp Inter WeakCommutativity
 = V3 (f a) (g b) (f c):         Inter WeakCommutativity
 = V3 (f a) (g b) (g a): Id Comp Inter WeakCommutativity
 = V3 (f a) (g b) (g b): Id
 = V3 (f a) (g b) (g c):         Inter WeakCommutativity
 = V3 (f a) (g b) (h a): Id      Inter WeakCommutativity
 = V3 (f a) (g b) (h b): Id      Inter WeakCommutativity
 = V3 (f a) (g b) (h c):
 = V3 (f a) (g c) (f a): Id Comp Inter WeakCommutativity
 = V3 (f a) (g c) (f b): Id Comp Inter WeakCommutativity
 = V3 (f a) (g c) (f c): Id Comp Inter WeakCommutativity
 = V3 (f a) (g c) (g a): Id Comp Inter WeakCommutativity
 = V3 (f a) (g c) (g b): Id Comp Inter WeakCommutativity
 = V3 (f a) (g c) (g c): Id Comp Inter WeakCommutativity
 = V3 (f a) (g c) (h a): Id Comp Inter WeakCommutativity
 = V3 (f a) (g c) (h b): Id Comp Inter WeakCommutativity
 = V3 (f a) (g c) (h c): Id      Inter WeakCommutativity
 = V3 (f a) (h a) (f a): Id Comp Inter WeakCommutativity
 = V3 (f a) (h a) (f b): Id Comp Inter WeakCommutativity
 = V3 (f a) (h a) (f c): Id Comp Inter WeakCommutativity
 = V3 (f a) (h a) (g a): Id Comp Inter WeakCommutativity
 = V3 (f a) (h a) (g b): Id Comp Inter WeakCommutativity
 = V3 (f a) (h a) (g c): Id Comp Inter WeakCommutativity
 = V3 (f a) (h a) (h a): Id      Inter WeakCommutativity
 = V3 (f a) (h a) (h b): Id Comp Inter WeakCommutativity
 = V3 (f a) (h a) (h c): Id Comp Inter WeakCommutativity
 = V3 (f a) (h b) (f a): Id Comp Inter WeakCommutativity
 = V3 (f a) (h b) (f b): Id Comp Inter WeakCommutativity
 = V3 (f a) (h b) (f c):    Comp Inter WeakCommutativity
 = V3 (f a) (h b) (g a): Id Comp Inter WeakCommutativity
 = V3 (f a) (h b) (g b): Id Comp Inter WeakCommutativity
 = V3 (f a) (h b) (g c):    Comp Inter WeakCommutativity
 = V3 (f a) (h b) (h a): Id Comp Inter WeakCommutativity
 = V3 (f a) (h b) (h b): Id Comp Inter WeakCommutativity
 = V3 (f a) (h b) (h c):         Inter WeakCommutativity
 = V3 (f a) (h c) (f a): Id Comp
 = V3 (f a) (h c) (f b): Id Comp Inter WeakCommutativity
 = V3 (f a) (h c) (f c): Id Comp Inter WeakCommutativity
 = V3 (f a) (h c) (g a): Id Comp Inter WeakCommutativity
 = V3 (f a) (h c) (g b): Id Comp
 = V3 (f a) (h c) (g c): Id Comp Inter WeakCommutativity
 = V3 (f a) (h c) (h a): Id Comp Inter WeakCommutativity
 = V3 (f a) (h c) (h b): Id Comp Inter WeakCommutativity
 = V3 (f a) (h c) (h c): Id
 = V3 (f b) (f a) (f a): Id Comp Inter WeakCommutativity
 = V3 (f b) (f a) (f b): Id Comp Inter WeakCommutativity
 = V3 (f b) (f a) (f c): Id Comp Inter WeakCommutativity
 = V3 (f b) (f a) (g a): Id Comp Inter WeakCommutativity
 = V3 (f b) (f a) (g b): Id Comp Inter WeakCommutativity
 = V3 (f b) (f a) (g c): Id Comp Inter WeakCommutativity
 = V3 (f b) (f a) (h a): Id Comp Inter WeakCommutativity
 = V3 (f b) (f a) (h b): Id Comp Inter WeakCommutativity
 = V3 (f b) (f a) (h c): Id Comp Inter WeakCommutativity
 = V3 (f b) (f b) (f a): Id Comp Inter WeakCommutativity
 = V3 (f b) (f b) (f b): Id Comp Inter WeakCommutativity
 = V3 (f b) (f b) (f c): Id Comp Inter WeakCommutativity
 = V3 (f b) (f b) (g a): Id Comp Inter WeakCommutativity
 = V3 (f b) (f b) (g b): Id Comp Inter WeakCommutativity
 = V3 (f b) (f b) (g c): Id Comp Inter WeakCommutativity
 = V3 (f b) (f b) (h a): Id Comp Inter WeakCommutativity
 = V3 (f b) (f b) (h b): Id Comp Inter WeakCommutativity
 = V3 (f b) (f b) (h c): Id Comp Inter WeakCommutativity
 = V3 (f b) (f c) (f a): Id Comp Inter WeakCommutativity
 = V3 (f b) (f c) (f b): Id Comp Inter WeakCommutativity
 = V3 (f b) (f c) (f c): Id Comp Inter WeakCommutativity
 = V3 (f b) (f c) (g a): Id Comp Inter WeakCommutativity
 = V3 (f b) (f c) (g b): Id Comp Inter WeakCommutativity
 = V3 (f b) (f c) (g c): Id Comp Inter WeakCommutativity
 = V3 (f b) (f c) (h a): Id Comp Inter WeakCommutativity
 = V3 (f b) (f c) (h b): Id Comp Inter WeakCommutativity
 = V3 (f b) (f c) (h c): Id Comp Inter WeakCommutativity
 = V3 (f b) (g a) (f a): Id Comp Inter WeakCommutativity
 = V3 (f b) (g a) (f b): Id Comp Inter WeakCommutativity
 = V3 (f b) (g a) (f c): Id Comp Inter WeakCommutativity
 = V3 (f b) (g a) (g a): Id Comp Inter WeakCommutativity
 = V3 (f b) (g a) (g b): Id Comp Inter WeakCommutativity
 = V3 (f b) (g a) (g c): Id Comp Inter WeakCommutativity
 = V3 (f b) (g a) (h a): Id Comp Inter WeakCommutativity
 = V3 (f b) (g a) (h b): Id Comp Inter WeakCommutativity
 = V3 (f b) (g a) (h c): Id Comp Inter WeakCommutativity
 = V3 (f b) (g b) (f a): Id Comp Inter WeakCommutativity
 = V3 (f b) (g b) (f b): Id      Inter WeakCommutativity
 = V3 (f b) (g b) (f c): Id Comp Inter WeakCommutativity
 = V3 (f b) (g b) (g a): Id Comp Inter WeakCommutativity
 = V3 (f b) (g b) (g b): Id      Inter WeakCommutativity
 = V3 (f b) (g b) (g c): Id      Inter WeakCommutativity
 = V3 (f b) (g b) (h a): Id Comp Inter WeakCommutativity
 = V3 (f b) (g b) (h b): Id      Inter WeakCommutativity
 = V3 (f b) (g b) (h c): Id      Inter WeakCommutativity
 = V3 (f b) (g c) (f a): Id Comp Inter WeakCommutativity
 = V3 (f b) (g c) (f b): Id Comp Inter WeakCommutativity
 = V3 (f b) (g c) (f c): Id Comp Inter WeakCommutativity
 = V3 (f b) (g c) (g a): Id Comp Inter WeakCommutativity
 = V3 (f b) (g c) (g b): Id Comp Inter WeakCommutativity
 = V3 (f b) (g c) (g c): Id Comp Inter WeakCommutativity
 = V3 (f b) (g c) (h a): Id Comp Inter WeakCommutativity
 = V3 (f b) (g c) (h b): Id Comp Inter WeakCommutativity
 = V3 (f b) (g c) (h c): Id Comp Inter WeakCommutativity
 = V3 (f b) (h a) (f a): Id Comp Inter WeakCommutativity
 = V3 (f b) (h a) (f b): Id Comp Inter WeakCommutativity
 = V3 (f b) (h a) (f c): Id Comp Inter WeakCommutativity
 = V3 (f b) (h a) (g a): Id Comp Inter WeakCommutativity
 = V3 (f b) (h a) (g b): Id Comp Inter WeakCommutativity
 = V3 (f b) (h a) (g c): Id Comp Inter WeakCommutativity
 = V3 (f b) (h a) (h a): Id Comp Inter WeakCommutativity
 = V3 (f b) (h a) (h b): Id Comp Inter WeakCommutativity
 = V3 (f b) (h a) (h c): Id Comp Inter WeakCommutativity
 = V3 (f b) (h b) (f a): Id Comp Inter WeakCommutativity
 = V3 (f b) (h b) (f b): Id Comp Inter WeakCommutativity
 = V3 (f b) (h b) (f c): Id Comp Inter WeakCommutativity
 = V3 (f b) (h b) (g a): Id Comp Inter WeakCommutativity
 = V3 (f b) (h b) (g b): Id Comp Inter WeakCommutativity
 = V3 (f b) (h b) (g c): Id Comp Inter WeakCommutativity
 = V3 (f b) (h b) (h a): Id Comp Inter WeakCommutativity
 = V3 (f b) (h b) (h b): Id Comp Inter WeakCommutativity
 = V3 (f b) (h b) (h c): Id Comp Inter WeakCommutativity
 = V3 (f b) (h c) (f a): Id Comp Inter WeakCommutativity
 = V3 (f b) (h c) (f b): Id Comp Inter WeakCommutativity
 = V3 (f b) (h c) (f c): Id Comp Inter WeakCommutativity
 = V3 (f b) (h c) (g a): Id Comp Inter WeakCommutativity
 = V3 (f b) (h c) (g b): Id Comp Inter WeakCommutativity
 = V3 (f b) (h c) (g c): Id Comp Inter WeakCommutativity
 = V3 (f b) (h c) (h a): Id Comp Inter WeakCommutativity
 = V3 (f b) (h c) (h b): Id Comp Inter WeakCommutativity
 = V3 (f b) (h c) (h c): Id Comp Inter WeakCommutativity
 = V3 (f c) (f a) (f a): Id Comp Inter WeakCommutativity
 = V3 (f c) (f a) (f b): Id Comp Inter WeakCommutativity
 = V3 (f c) (f a) (f c): Id Comp Inter WeakCommutativity
 = V3 (f c) (f a) (g a): Id Comp Inter WeakCommutativity
 = V3 (f c) (f a) (g b): Id Comp Inter WeakCommutativity
 = V3 (f c) (f a) (g c): Id Comp Inter WeakCommutativity
 = V3 (f c) (f a) (h a): Id Comp Inter WeakCommutativity
 = V3 (f c) (f a) (h b): Id Comp Inter WeakCommutativity
 = V3 (f c) (f a) (h c): Id Comp Inter WeakCommutativity
 = V3 (f c) (f b) (f a): Id Comp Inter WeakCommutativity
 = V3 (f c) (f b) (f b): Id Comp Inter WeakCommutativity
 = V3 (f c) (f b) (f c): Id Comp Inter WeakCommutativity
 = V3 (f c) (f b) (g a): Id Comp Inter WeakCommutativity
 = V3 (f c) (f b) (g b): Id Comp Inter WeakCommutativity
 = V3 (f c) (f b) (g c): Id Comp Inter WeakCommutativity
 = V3 (f c) (f b) (h a): Id Comp Inter WeakCommutativity
 = V3 (f c) (f b) (h b): Id Comp Inter WeakCommutativity
 = V3 (f c) (f b) (h c): Id Comp Inter WeakCommutativity
 = V3 (f c) (f c) (f a): Id Comp Inter WeakCommutativity
 = V3 (f c) (f c) (f b): Id Comp Inter WeakCommutativity
 = V3 (f c) (f c) (f c): Id Comp Inter WeakCommutativity
 = V3 (f c) (f c) (g a): Id Comp Inter WeakCommutativity
 = V3 (f c) (f c) (g b): Id Comp Inter WeakCommutativity
 = V3 (f c) (f c) (g c): Id Comp Inter WeakCommutativity
 = V3 (f c) (f c) (h a): Id Comp Inter WeakCommutativity
 = V3 (f c) (f c) (h b): Id Comp Inter WeakCommutativity
 = V3 (f c) (f c) (h c): Id      Inter WeakCommutativity
 = V3 (f c) (g a) (f a): Id Comp Inter WeakCommutativity
 = V3 (f c) (g a) (f b): Id Comp Inter WeakCommutativity
 = V3 (f c) (g a) (f c): Id Comp Inter WeakCommutativity
 = V3 (f c) (g a) (g a): Id Comp Inter WeakCommutativity
 = V3 (f c) (g a) (g b): Id Comp Inter WeakCommutativity
 = V3 (f c) (g a) (g c): Id Comp Inter WeakCommutativity
 = V3 (f c) (g a) (h a): Id Comp Inter WeakCommutativity
 = V3 (f c) (g a) (h b): Id Comp Inter WeakCommutativity
 = V3 (f c) (g a) (h c): Id Comp Inter WeakCommutativity
 = V3 (f c) (g b) (f a): Id Comp Inter WeakCommutativity
 = V3 (f c) (g b) (f b): Id Comp Inter WeakCommutativity
 = V3 (f c) (g b) (f c): Id Comp Inter WeakCommutativity
 = V3 (f c) (g b) (g a): Id Comp Inter WeakCommutativity
 = V3 (f c) (g b) (g b): Id Comp Inter WeakCommutativity
 = V3 (f c) (g b) (g c): Id Comp Inter WeakCommutativity
 = V3 (f c) (g b) (h a): Id Comp Inter WeakCommutativity
 = V3 (f c) (g b) (h b): Id Comp Inter WeakCommutativity
 = V3 (f c) (g b) (h c): Id      Inter WeakCommutativity
 = V3 (f c) (g c) (f a): Id Comp Inter WeakCommutativity
 = V3 (f c) (g c) (f b): Id Comp Inter WeakCommutativity
 = V3 (f c) (g c) (f c): Id Comp Inter WeakCommutativity
 = V3 (f c) (g c) (g a): Id Comp Inter WeakCommutativity
 = V3 (f c) (g c) (g b): Id Comp Inter WeakCommutativity
 = V3 (f c) (g c) (g c): Id Comp Inter WeakCommutativity
 = V3 (f c) (g c) (h a): Id Comp Inter WeakCommutativity
 = V3 (f c) (g c) (h b): Id Comp Inter WeakCommutativity
 = V3 (f c) (g c) (h c): Id      Inter WeakCommutativity
 = V3 (f c) (h a) (f a): Id Comp Inter WeakCommutativity
 = V3 (f c) (h a) (f b): Id Comp Inter WeakCommutativity
 = V3 (f c) (h a) (f c): Id Comp Inter WeakCommutativity
 = V3 (f c) (h a) (g a): Id Comp Inter WeakCommutativity
 = V3 (f c) (h a) (g b): Id Comp Inter WeakCommutativity
 = V3 (f c) (h a) (g c): Id Comp Inter WeakCommutativity
 = V3 (f c) (h a) (h a): Id Comp Inter WeakCommutativity
 = V3 (f c) (h a) (h b): Id Comp Inter WeakCommutativity
 = V3 (f c) (h a) (h c): Id Comp Inter WeakCommutativity
 = V3 (f c) (h b) (f a): Id Comp Inter WeakCommutativity
 = V3 (f c) (h b) (f b): Id Comp Inter WeakCommutativity
 = V3 (f c) (h b) (f c): Id Comp Inter WeakCommutativity
 = V3 (f c) (h b) (g a): Id Comp Inter WeakCommutativity
 = V3 (f c) (h b) (g b): Id Comp Inter WeakCommutativity
 = V3 (f c) (h b) (g c): Id Comp Inter WeakCommutativity
 = V3 (f c) (h b) (h a): Id Comp Inter WeakCommutativity
 = V3 (f c) (h b) (h b): Id Comp Inter WeakCommutativity
 = V3 (f c) (h b) (h c): Id      Inter WeakCommutativity
 = V3 (f c) (h c) (f a): Id Comp Inter WeakCommutativity
 = V3 (f c) (h c) (f b): Id Comp Inter WeakCommutativity
 = V3 (f c) (h c) (f c): Id Comp Inter WeakCommutativity
 = V3 (f c) (h c) (g a): Id Comp Inter WeakCommutativity
 = V3 (f c) (h c) (g b): Id Comp Inter WeakCommutativity
 = V3 (f c) (h c) (g c): Id Comp Inter WeakCommutativity
 = V3 (f c) (h c) (h a): Id Comp Inter WeakCommutativity
 = V3 (f c) (h c) (h b): Id Comp Inter WeakCommutativity
 = V3 (f c) (h c) (h c): Id      Inter WeakCommutativity
 = V3 (g a) (f a) (f a): Id Comp Inter WeakCommutativity
 = V3 (g a) (f a) (f b): Id Comp Inter WeakCommutativity
 = V3 (g a) (f a) (f c): Id Comp Inter WeakCommutativity
 = V3 (g a) (f a) (g a): Id Comp Inter WeakCommutativity
 = V3 (g a) (f a) (g b): Id Comp Inter WeakCommutativity
 = V3 (g a) (f a) (g c): Id Comp Inter WeakCommutativity
 = V3 (g a) (f a) (h a): Id Comp Inter WeakCommutativity
 = V3 (g a) (f a) (h b): Id Comp Inter WeakCommutativity
 = V3 (g a) (f a) (h c): Id Comp Inter WeakCommutativity
 = V3 (g a) (f b) (f a): Id Comp Inter WeakCommutativity
 = V3 (g a) (f b) (f b): Id Comp Inter WeakCommutativity
 = V3 (g a) (f b) (f c):    Comp Inter WeakCommutativity
 = V3 (g a) (f b) (g a): Id Comp Inter WeakCommutativity
 = V3 (g a) (f b) (g b): Id Comp Inter WeakCommutativity
 = V3 (g a) (f b) (g c):    Comp Inter WeakCommutativity
 = V3 (g a) (f b) (h a): Id Comp Inter WeakCommutativity
 = V3 (g a) (f b) (h b): Id Comp Inter WeakCommutativity
 = V3 (g a) (f b) (h c):    Comp Inter WeakCommutativity
 = V3 (g a) (f c) (f a): Id Comp Inter WeakCommutativity
 = V3 (g a) (f c) (f b): Id Comp Inter WeakCommutativity
 = V3 (g a) (f c) (f c): Id Comp Inter WeakCommutativity
 = V3 (g a) (f c) (g a): Id Comp Inter WeakCommutativity
 = V3 (g a) (f c) (g b): Id Comp Inter WeakCommutativity
 = V3 (g a) (f c) (g c): Id Comp Inter WeakCommutativity
 = V3 (g a) (f c) (h a): Id Comp Inter WeakCommutativity
 = V3 (g a) (f c) (h b): Id Comp Inter WeakCommutativity
 = V3 (g a) (f c) (h c): Id Comp Inter WeakCommutativity
 = V3 (g a) (g a) (f a): Id Comp Inter WeakCommutativity
 = V3 (g a) (g a) (f b): Id Comp Inter WeakCommutativity
 = V3 (g a) (g a) (f c): Id Comp Inter WeakCommutativity
 = V3 (g a) (g a) (g a): Id Comp Inter WeakCommutativity
 = V3 (g a) (g a) (g b): Id Comp Inter WeakCommutativity
 = V3 (g a) (g a) (g c): Id Comp Inter WeakCommutativity
 = V3 (g a) (g a) (h a): Id Comp Inter WeakCommutativity
 = V3 (g a) (g a) (h b): Id Comp Inter WeakCommutativity
 = V3 (g a) (g a) (h c): Id Comp Inter WeakCommutativity
 = V3 (g a) (g b) (f a): Id Comp Inter WeakCommutativity
 = V3 (g a) (g b) (f b): Id Comp Inter WeakCommutativity
 = V3 (g a) (g b) (f c):    Comp Inter WeakCommutativity
 = V3 (g a) (g b) (g a): Id      Inter WeakCommutativity
 = V3 (g a) (g b) (g b): Id      Inter WeakCommutativity
 = V3 (g a) (g b) (g c):         Inter WeakCommutativity
 = V3 (g a) (g b) (h a): Id Comp Inter WeakCommutativity
 = V3 (g a) (g b) (h b): Id      Inter WeakCommutativity
 = V3 (g a) (g b) (h c):         Inter WeakCommutativity
 = V3 (g a) (g c) (f a): Id Comp Inter WeakCommutativity
 = V3 (g a) (g c) (f b): Id Comp Inter WeakCommutativity
 = V3 (g a) (g c) (f c): Id Comp Inter WeakCommutativity
 = V3 (g a) (g c) (g a): Id Comp Inter WeakCommutativity
 = V3 (g a) (g c) (g b): Id Comp Inter WeakCommutativity
 = V3 (g a) (g c) (g c): Id Comp Inter WeakCommutativity
 = V3 (g a) (g c) (h a): Id Comp Inter WeakCommutativity
 = V3 (g a) (g c) (h b): Id Comp Inter WeakCommutativity
 = V3 (g a) (g c) (h c): Id Comp Inter WeakCommutativity
 = V3 (g a) (h a) (f a): Id Comp Inter WeakCommutativity
 = V3 (g a) (h a) (f b): Id Comp Inter WeakCommutativity
 = V3 (g a) (h a) (f c): Id Comp Inter WeakCommutativity
 = V3 (g a) (h a) (g a): Id Comp Inter WeakCommutativity
 = V3 (g a) (h a) (g b): Id Comp Inter WeakCommutativity
 = V3 (g a) (h a) (g c): Id Comp Inter WeakCommutativity
 = V3 (g a) (h a) (h a): Id Comp Inter WeakCommutativity
 = V3 (g a) (h a) (h b): Id Comp Inter WeakCommutativity
 = V3 (g a) (h a) (h c): Id Comp Inter WeakCommutativity
 = V3 (g a) (h b) (f a): Id Comp Inter WeakCommutativity
 = V3 (g a) (h b) (f b): Id Comp Inter WeakCommutativity
 = V3 (g a) (h b) (f c):    Comp Inter WeakCommutativity
 = V3 (g a) (h b) (g a): Id Comp Inter WeakCommutativity
 = V3 (g a) (h b) (g b): Id Comp Inter WeakCommutativity
 = V3 (g a) (h b) (g c):    Comp Inter WeakCommutativity
 = V3 (g a) (h b) (h a): Id Comp Inter WeakCommutativity
 = V3 (g a) (h b) (h b): Id Comp Inter WeakCommutativity
 = V3 (g a) (h b) (h c):    Comp Inter WeakCommutativity
 = V3 (g a) (h c) (f a): Id Comp Inter WeakCommutativity
 = V3 (g a) (h c) (f b): Id Comp Inter WeakCommutativity
 = V3 (g a) (h c) (f c): Id Comp Inter WeakCommutativity
 = V3 (g a) (h c) (g a): Id Comp Inter WeakCommutativity
 = V3 (g a) (h c) (g b): Id Comp Inter WeakCommutativity
 = V3 (g a) (h c) (g c): Id Comp Inter WeakCommutativity
 = V3 (g a) (h c) (h a): Id Comp Inter WeakCommutativity
 = V3 (g a) (h c) (h b): Id Comp Inter WeakCommutativity
 = V3 (g a) (h c) (h c): Id Comp Inter WeakCommutativity
 = V3 (g b) (f a) (f a): Id Comp
 = V3 (g b) (f a) (f b): Id Comp Inter WeakCommutativity
 = V3 (g b) (f a) (f c): Id Comp Inter WeakCommutativity
 = V3 (g b) (f a) (g a): Id Comp Inter WeakCommutativity
 = V3 (g b) (f a) (g b): Id Comp
 = V3 (g b) (f a) (g c): Id Comp Inter WeakCommutativity
 = V3 (g b) (f a) (h a): Id Comp Inter WeakCommutativity
 = V3 (g b) (f a) (h b): Id Comp Inter WeakCommutativity
 = V3 (g b) (f a) (h c): Id Comp
 = V3 (g b) (f b) (f a): Id Comp Inter WeakCommutativity
 = V3 (g b) (f b) (f b): Id Comp Inter WeakCommutativity
 = V3 (g b) (f b) (f c): Id Comp Inter WeakCommutativity
 = V3 (g b) (f b) (g a): Id Comp Inter WeakCommutativity
 = V3 (g b) (f b) (g b): Id Comp Inter WeakCommutativity
 = V3 (g b) (f b) (g c): Id Comp Inter WeakCommutativity
 = V3 (g b) (f b) (h a): Id Comp Inter WeakCommutativity
 = V3 (g b) (f b) (h b): Id Comp Inter WeakCommutativity
 = V3 (g b) (f b) (h c): Id Comp Inter WeakCommutativity
 = V3 (g b) (f c) (f a): Id Comp Inter WeakCommutativity
 = V3 (g b) (f c) (f b): Id Comp Inter WeakCommutativity
 = V3 (g b) (f c) (f c): Id Comp Inter WeakCommutativity
 = V3 (g b) (f c) (g a): Id Comp Inter WeakCommutativity
 = V3 (g b) (f c) (g b): Id Comp Inter WeakCommutativity
 = V3 (g b) (f c) (g c): Id Comp Inter WeakCommutativity
 = V3 (g b) (f c) (h a): Id Comp Inter WeakCommutativity
 = V3 (g b) (f c) (h b): Id Comp Inter WeakCommutativity
 = V3 (g b) (f c) (h c): Id Comp Inter WeakCommutativity
 = V3 (g b) (g a) (f a): Id Comp Inter WeakCommutativity
 = V3 (g b) (g a) (f b): Id Comp Inter WeakCommutativity
 = V3 (g b) (g a) (f c): Id Comp Inter WeakCommutativity
 = V3 (g b) (g a) (g a): Id Comp Inter WeakCommutativity
 = V3 (g b) (g a) (g b): Id Comp Inter WeakCommutativity
 = V3 (g b) (g a) (g c): Id Comp Inter WeakCommutativity
 = V3 (g b) (g a) (h a): Id Comp Inter WeakCommutativity
 = V3 (g b) (g a) (h b): Id Comp Inter WeakCommutativity
 = V3 (g b) (g a) (h c): Id Comp Inter WeakCommutativity
 = V3 (g b) (g b) (f a): Id Comp
 = V3 (g b) (g b) (f b): Id Comp Inter WeakCommutativity
 = V3 (g b) (g b) (f c): Id Comp Inter WeakCommutativity
 = V3 (g b) (g b) (g a): Id Comp Inter WeakCommutativity
 = V3 (g b) (g b) (g b): Id
 = V3 (g b) (g b) (g c): Id      Inter WeakCommutativity
 = V3 (g b) (g b) (h a): Id Comp Inter WeakCommutativity
 = V3 (g b) (g b) (h b): Id      Inter WeakCommutativity
 = V3 (g b) (g b) (h c): Id
 = V3 (g b) (g c) (f a): Id Comp Inter WeakCommutativity
 = V3 (g b) (g c) (f b): Id Comp Inter WeakCommutativity
 = V3 (g b) (g c) (f c): Id Comp Inter WeakCommutativity
 = V3 (g b) (g c) (g a): Id Comp Inter WeakCommutativity
 = V3 (g b) (g c) (g b): Id Comp Inter WeakCommutativity
 = V3 (g b) (g c) (g c): Id Comp Inter WeakCommutativity
 = V3 (g b) (g c) (h a): Id Comp Inter WeakCommutativity
 = V3 (g b) (g c) (h b): Id Comp Inter WeakCommutativity
 = V3 (g b) (g c) (h c): Id Comp Inter WeakCommutativity
 = V3 (g b) (h a) (f a): Id Comp Inter WeakCommutativity
 = V3 (g b) (h a) (f b): Id Comp Inter WeakCommutativity
 = V3 (g b) (h a) (f c): Id Comp Inter WeakCommutativity
 = V3 (g b) (h a) (g a): Id Comp Inter WeakCommutativity
 = V3 (g b) (h a) (g b): Id Comp Inter WeakCommutativity
 = V3 (g b) (h a) (g c): Id Comp Inter WeakCommutativity
 = V3 (g b) (h a) (h a): Id Comp Inter WeakCommutativity
 = V3 (g b) (h a) (h b): Id Comp Inter WeakCommutativity
 = V3 (g b) (h a) (h c): Id Comp Inter WeakCommutativity
 = V3 (g b) (h b) (f a): Id Comp Inter WeakCommutativity
 = V3 (g b) (h b) (f b): Id Comp Inter WeakCommutativity
 = V3 (g b) (h b) (f c): Id Comp Inter WeakCommutativity
 = V3 (g b) (h b) (g a): Id Comp Inter WeakCommutativity
 = V3 (g b) (h b) (g b): Id Comp Inter WeakCommutativity
 = V3 (g b) (h b) (g c): Id Comp Inter WeakCommutativity
 = V3 (g b) (h b) (h a): Id Comp Inter WeakCommutativity
 = V3 (g b) (h b) (h b): Id Comp Inter WeakCommutativity
 = V3 (g b) (h b) (h c): Id Comp Inter WeakCommutativity
 = V3 (g b) (h c) (f a): Id Comp
 = V3 (g b) (h c) (f b): Id Comp Inter WeakCommutativity
 = V3 (g b) (h c) (f c): Id Comp Inter WeakCommutativity
 = V3 (g b) (h c) (g a): Id Comp Inter WeakCommutativity
 = V3 (g b) (h c) (g b): Id Comp
 = V3 (g b) (h c) (g c): Id Comp Inter WeakCommutativity
 = V3 (g b) (h c) (h a): Id Comp Inter WeakCommutativity
 = V3 (g b) (h c) (h b): Id Comp Inter WeakCommutativity
 = V3 (g b) (h c) (h c): Id Comp
 = V3 (g c) (f a) (f a): Id Comp Inter WeakCommutativity
 = V3 (g c) (f a) (f b): Id Comp Inter WeakCommutativity
 = V3 (g c) (f a) (f c): Id Comp Inter WeakCommutativity
 = V3 (g c) (f a) (g a): Id Comp Inter WeakCommutativity
 = V3 (g c) (f a) (g b): Id Comp Inter WeakCommutativity
 = V3 (g c) (f a) (g c): Id Comp Inter WeakCommutativity
 = V3 (g c) (f a) (h a): Id Comp Inter WeakCommutativity
 = V3 (g c) (f a) (h b): Id Comp Inter WeakCommutativity
 = V3 (g c) (f a) (h c): Id Comp Inter WeakCommutativity
 = V3 (g c) (f b) (f a): Id Comp Inter WeakCommutativity
 = V3 (g c) (f b) (f b): Id Comp Inter WeakCommutativity
 = V3 (g c) (f b) (f c): Id Comp Inter WeakCommutativity
 = V3 (g c) (f b) (g a): Id Comp Inter WeakCommutativity
 = V3 (g c) (f b) (g b): Id Comp Inter WeakCommutativity
 = V3 (g c) (f b) (g c): Id Comp Inter WeakCommutativity
 = V3 (g c) (f b) (h a): Id Comp Inter WeakCommutativity
 = V3 (g c) (f b) (h b): Id Comp Inter WeakCommutativity
 = V3 (g c) (f b) (h c): Id Comp Inter WeakCommutativity
 = V3 (g c) (f c) (f a): Id Comp Inter WeakCommutativity
 = V3 (g c) (f c) (f b): Id Comp Inter WeakCommutativity
 = V3 (g c) (f c) (f c): Id Comp Inter WeakCommutativity
 = V3 (g c) (f c) (g a): Id Comp Inter WeakCommutativity
 = V3 (g c) (f c) (g b): Id Comp Inter WeakCommutativity
 = V3 (g c) (f c) (g c): Id Comp Inter WeakCommutativity
 = V3 (g c) (f c) (h a): Id Comp Inter WeakCommutativity
 = V3 (g c) (f c) (h b): Id Comp Inter WeakCommutativity
 = V3 (g c) (f c) (h c): Id Comp Inter WeakCommutativity
 = V3 (g c) (g a) (f a): Id Comp Inter WeakCommutativity
 = V3 (g c) (g a) (f b): Id Comp Inter WeakCommutativity
 = V3 (g c) (g a) (f c): Id Comp Inter WeakCommutativity
 = V3 (g c) (g a) (g a): Id Comp Inter WeakCommutativity
 = V3 (g c) (g a) (g b): Id Comp Inter WeakCommutativity
 = V3 (g c) (g a) (g c): Id Comp Inter WeakCommutativity
 = V3 (g c) (g a) (h a): Id Comp Inter WeakCommutativity
 = V3 (g c) (g a) (h b): Id Comp Inter WeakCommutativity
 = V3 (g c) (g a) (h c): Id Comp Inter WeakCommutativity
 = V3 (g c) (g b) (f a): Id Comp Inter WeakCommutativity
 = V3 (g c) (g b) (f b): Id Comp Inter WeakCommutativity
 = V3 (g c) (g b) (f c): Id Comp Inter WeakCommutativity
 = V3 (g c) (g b) (g a): Id Comp Inter WeakCommutativity
 = V3 (g c) (g b) (g b): Id Comp Inter WeakCommutativity
 = V3 (g c) (g b) (g c): Id      Inter WeakCommutativity
 = V3 (g c) (g b) (h a): Id Comp Inter WeakCommutativity
 = V3 (g c) (g b) (h b): Id Comp Inter WeakCommutativity
 = V3 (g c) (g b) (h c): Id Comp Inter WeakCommutativity
 = V3 (g c) (g c) (f a): Id Comp Inter WeakCommutativity
 = V3 (g c) (g c) (f b): Id Comp Inter WeakCommutativity
 = V3 (g c) (g c) (f c): Id Comp Inter WeakCommutativity
 = V3 (g c) (g c) (g a): Id Comp Inter WeakCommutativity
 = V3 (g c) (g c) (g b): Id Comp Inter WeakCommutativity
 = V3 (g c) (g c) (g c): Id Comp Inter WeakCommutativity
 = V3 (g c) (g c) (h a): Id Comp Inter WeakCommutativity
 = V3 (g c) (g c) (h b): Id Comp Inter WeakCommutativity
 = V3 (g c) (g c) (h c): Id      Inter WeakCommutativity
 = V3 (g c) (h a) (f a): Id Comp Inter WeakCommutativity
 = V3 (g c) (h a) (f b): Id Comp Inter WeakCommutativity
 = V3 (g c) (h a) (f c): Id Comp Inter WeakCommutativity
 = V3 (g c) (h a) (g a): Id Comp Inter WeakCommutativity
 = V3 (g c) (h a) (g b): Id Comp Inter WeakCommutativity
 = V3 (g c) (h a) (g c): Id Comp Inter WeakCommutativity
 = V3 (g c) (h a) (h a): Id Comp Inter WeakCommutativity
 = V3 (g c) (h a) (h b): Id Comp Inter WeakCommutativity
 = V3 (g c) (h a) (h c): Id Comp Inter WeakCommutativity
 = V3 (g c) (h b) (f a): Id Comp Inter WeakCommutativity
 = V3 (g c) (h b) (f b): Id Comp Inter WeakCommutativity
 = V3 (g c) (h b) (f c): Id Comp Inter WeakCommutativity
 = V3 (g c) (h b) (g a): Id Comp Inter WeakCommutativity
 = V3 (g c) (h b) (g b): Id Comp Inter WeakCommutativity
 = V3 (g c) (h b) (g c): Id Comp Inter WeakCommutativity
 = V3 (g c) (h b) (h a): Id Comp Inter WeakCommutativity
 = V3 (g c) (h b) (h b): Id Comp Inter WeakCommutativity
 = V3 (g c) (h b) (h c): Id Comp Inter WeakCommutativity
 = V3 (g c) (h c) (f a): Id Comp Inter WeakCommutativity
 = V3 (g c) (h c) (f b): Id Comp Inter WeakCommutativity
 = V3 (g c) (h c) (f c): Id Comp Inter WeakCommutativity
 = V3 (g c) (h c) (g a): Id Comp Inter WeakCommutativity
 = V3 (g c) (h c) (g b): Id Comp Inter WeakCommutativity
 = V3 (g c) (h c) (g c): Id Comp Inter WeakCommutativity
 = V3 (g c) (h c) (h a): Id Comp Inter WeakCommutativity
 = V3 (g c) (h c) (h b): Id Comp Inter WeakCommutativity
 = V3 (g c) (h c) (h c): Id Comp Inter WeakCommutativity
 = V3 (h a) (f a) (f a): Id Comp Inter WeakCommutativity
 = V3 (h a) (f a) (f b): Id Comp Inter WeakCommutativity
 = V3 (h a) (f a) (f c): Id Comp Inter WeakCommutativity
 = V3 (h a) (f a) (g a): Id Comp Inter WeakCommutativity
 = V3 (h a) (f a) (g b): Id Comp Inter WeakCommutativity
 = V3 (h a) (f a) (g c): Id Comp Inter WeakCommutativity
 = V3 (h a) (f a) (h a): Id Comp Inter WeakCommutativity
 = V3 (h a) (f a) (h b): Id Comp Inter WeakCommutativity
 = V3 (h a) (f a) (h c): Id Comp Inter WeakCommutativity
 = V3 (h a) (f b) (f a): Id Comp Inter WeakCommutativity
 = V3 (h a) (f b) (f b): Id Comp Inter WeakCommutativity
 = V3 (h a) (f b) (f c):    Comp Inter WeakCommutativity
 = V3 (h a) (f b) (g a): Id Comp Inter WeakCommutativity
 = V3 (h a) (f b) (g b): Id Comp Inter WeakCommutativity
 = V3 (h a) (f b) (g c):    Comp Inter WeakCommutativity
 = V3 (h a) (f b) (h a): Id Comp Inter WeakCommutativity
 = V3 (h a) (f b) (h b): Id Comp Inter WeakCommutativity
 = V3 (h a) (f b) (h c):    Comp Inter WeakCommutativity
 = V3 (h a) (f c) (f a): Id Comp Inter WeakCommutativity
 = V3 (h a) (f c) (f b): Id Comp Inter WeakCommutativity
 = V3 (h a) (f c) (f c): Id Comp Inter WeakCommutativity
 = V3 (h a) (f c) (g a): Id Comp Inter WeakCommutativity
 = V3 (h a) (f c) (g b): Id Comp Inter WeakCommutativity
 = V3 (h a) (f c) (g c): Id Comp Inter WeakCommutativity
 = V3 (h a) (f c) (h a): Id Comp Inter WeakCommutativity
 = V3 (h a) (f c) (h b): Id Comp Inter WeakCommutativity
 = V3 (h a) (f c) (h c): Id Comp Inter WeakCommutativity
 = V3 (h a) (g a) (f a): Id Comp Inter WeakCommutativity
 = V3 (h a) (g a) (f b): Id Comp Inter WeakCommutativity
 = V3 (h a) (g a) (f c): Id Comp Inter WeakCommutativity
 = V3 (h a) (g a) (g a): Id Comp Inter WeakCommutativity
 = V3 (h a) (g a) (g b): Id Comp Inter WeakCommutativity
 = V3 (h a) (g a) (g c): Id Comp Inter WeakCommutativity
 = V3 (h a) (g a) (h a): Id Comp Inter WeakCommutativity
 = V3 (h a) (g a) (h b): Id Comp Inter WeakCommutativity
 = V3 (h a) (g a) (h c): Id Comp Inter WeakCommutativity
 = V3 (h a) (g b) (f a): Id Comp Inter WeakCommutativity
 = V3 (h a) (g b) (f b): Id Comp Inter WeakCommutativity
 = V3 (h a) (g b) (f c):    Comp Inter WeakCommutativity
 = V3 (h a) (g b) (g a): Id Comp Inter WeakCommutativity
 = V3 (h a) (g b) (g b): Id Comp Inter WeakCommutativity
 = V3 (h a) (g b) (g c):    Comp Inter WeakCommutativity
 = V3 (h a) (g b) (h a): Id Comp Inter WeakCommutativity
 = V3 (h a) (g b) (h b): Id Comp Inter WeakCommutativity
 = V3 (h a) (g b) (h c):         Inter WeakCommutativity
 = V3 (h a) (g c) (f a): Id Comp Inter WeakCommutativity
 = V3 (h a) (g c) (f b): Id Comp Inter WeakCommutativity
 = V3 (h a) (g c) (f c): Id Comp Inter WeakCommutativity
 = V3 (h a) (g c) (g a): Id Comp Inter WeakCommutativity
 = V3 (h a) (g c) (g b): Id Comp Inter WeakCommutativity
 = V3 (h a) (g c) (g c): Id Comp Inter WeakCommutativity
 = V3 (h a) (g c) (h a): Id Comp Inter WeakCommutativity
 = V3 (h a) (g c) (h b): Id Comp Inter WeakCommutativity
 = V3 (h a) (g c) (h c): Id      Inter WeakCommutativity
 = V3 (h a) (h a) (f a): Id Comp Inter WeakCommutativity
 = V3 (h a) (h a) (f b): Id Comp Inter WeakCommutativity
 = V3 (h a) (h a) (f c): Id Comp Inter WeakCommutativity
 = V3 (h a) (h a) (g a): Id Comp Inter WeakCommutativity
 = V3 (h a) (h a) (g b): Id Comp Inter WeakCommutativity
 = V3 (h a) (h a) (g c): Id Comp Inter WeakCommutativity
 = V3 (h a) (h a) (h a): Id Comp Inter WeakCommutativity
 = V3 (h a) (h a) (h b): Id Comp Inter WeakCommutativity
 = V3 (h a) (h a) (h c): Id      Inter WeakCommutativity
 = V3 (h a) (h b) (f a): Id Comp Inter WeakCommutativity
 = V3 (h a) (h b) (f b): Id Comp Inter WeakCommutativity
 = V3 (h a) (h b) (f c):    Comp Inter WeakCommutativity
 = V3 (h a) (h b) (g a): Id Comp Inter WeakCommutativity
 = V3 (h a) (h b) (g b): Id Comp Inter WeakCommutativity
 = V3 (h a) (h b) (g c):    Comp Inter WeakCommutativity
 = V3 (h a) (h b) (h a): Id Comp Inter WeakCommutativity
 = V3 (h a) (h b) (h b): Id Comp Inter WeakCommutativity
 = V3 (h a) (h b) (h c):         Inter WeakCommutativity
 = V3 (h a) (h c) (f a): Id Comp Inter WeakCommutativity
 = V3 (h a) (h c) (f b): Id Comp Inter WeakCommutativity
 = V3 (h a) (h c) (f c): Id Comp Inter WeakCommutativity
 = V3 (h a) (h c) (g a): Id Comp Inter WeakCommutativity
 = V3 (h a) (h c) (g b): Id Comp Inter WeakCommutativity
 = V3 (h a) (h c) (g c): Id Comp Inter WeakCommutativity
 = V3 (h a) (h c) (h a): Id Comp Inter WeakCommutativity
 = V3 (h a) (h c) (h b): Id Comp Inter WeakCommutativity
 = V3 (h a) (h c) (h c): Id      Inter WeakCommutativity
 = V3 (h b) (f a) (f a): Id Comp Inter WeakCommutativity
 = V3 (h b) (f a) (f b): Id Comp Inter WeakCommutativity
 = V3 (h b) (f a) (f c): Id Comp Inter WeakCommutativity
 = V3 (h b) (f a) (g a): Id Comp Inter WeakCommutativity
 = V3 (h b) (f a) (g b): Id Comp Inter WeakCommutativity
 = V3 (h b) (f a) (g c): Id Comp Inter WeakCommutativity
 = V3 (h b) (f a) (h a): Id Comp Inter WeakCommutativity
 = V3 (h b) (f a) (h b): Id Comp Inter WeakCommutativity
 = V3 (h b) (f a) (h c): Id Comp Inter WeakCommutativity
 = V3 (h b) (f b) (f a): Id Comp Inter WeakCommutativity
 = V3 (h b) (f b) (f b): Id Comp Inter WeakCommutativity
 = V3 (h b) (f b) (f c): Id Comp Inter WeakCommutativity
 = V3 (h b) (f b) (g a): Id Comp Inter WeakCommutativity
 = V3 (h b) (f b) (g b): Id Comp Inter WeakCommutativity
 = V3 (h b) (f b) (g c): Id Comp Inter WeakCommutativity
 = V3 (h b) (f b) (h a): Id Comp Inter WeakCommutativity
 = V3 (h b) (f b) (h b): Id Comp Inter WeakCommutativity
 = V3 (h b) (f b) (h c): Id Comp Inter WeakCommutativity
 = V3 (h b) (f c) (f a): Id Comp Inter WeakCommutativity
 = V3 (h b) (f c) (f b): Id Comp Inter WeakCommutativity
 = V3 (h b) (f c) (f c): Id Comp Inter WeakCommutativity
 = V3 (h b) (f c) (g a): Id Comp Inter WeakCommutativity
 = V3 (h b) (f c) (g b): Id Comp Inter WeakCommutativity
 = V3 (h b) (f c) (g c): Id Comp Inter WeakCommutativity
 = V3 (h b) (f c) (h a): Id Comp Inter WeakCommutativity
 = V3 (h b) (f c) (h b): Id Comp Inter WeakCommutativity
 = V3 (h b) (f c) (h c): Id Comp Inter WeakCommutativity
 = V3 (h b) (g a) (f a): Id Comp Inter WeakCommutativity
 = V3 (h b) (g a) (f b): Id Comp Inter WeakCommutativity
 = V3 (h b) (g a) (f c): Id Comp Inter WeakCommutativity
 = V3 (h b) (g a) (g a): Id Comp Inter WeakCommutativity
 = V3 (h b) (g a) (g b): Id Comp Inter WeakCommutativity
 = V3 (h b) (g a) (g c): Id Comp Inter WeakCommutativity
 = V3 (h b) (g a) (h a): Id Comp Inter WeakCommutativity
 = V3 (h b) (g a) (h b): Id Comp Inter WeakCommutativity
 = V3 (h b) (g a) (h c): Id Comp Inter WeakCommutativity
 = V3 (h b) (g b) (f a): Id Comp Inter WeakCommutativity
 = V3 (h b) (g b) (f b): Id Comp Inter WeakCommutativity
 = V3 (h b) (g b) (f c): Id Comp Inter WeakCommutativity
 = V3 (h b) (g b) (g a): Id Comp Inter WeakCommutativity
 = V3 (h b) (g b) (g b): Id Comp Inter WeakCommutativity
 = V3 (h b) (g b) (g c): Id Comp Inter WeakCommutativity
 = V3 (h b) (g b) (h a): Id Comp Inter WeakCommutativity
 = V3 (h b) (g b) (h b): Id      Inter WeakCommutativity
 = V3 (h b) (g b) (h c): Id Comp Inter WeakCommutativity
 = V3 (h b) (g c) (f a): Id Comp Inter WeakCommutativity
 = V3 (h b) (g c) (f b): Id Comp Inter WeakCommutativity
 = V3 (h b) (g c) (f c): Id Comp Inter WeakCommutativity
 = V3 (h b) (g c) (g a): Id Comp Inter WeakCommutativity
 = V3 (h b) (g c) (g b): Id Comp Inter WeakCommutativity
 = V3 (h b) (g c) (g c): Id Comp Inter WeakCommutativity
 = V3 (h b) (g c) (h a): Id Comp Inter WeakCommutativity
 = V3 (h b) (g c) (h b): Id Comp Inter WeakCommutativity
 = V3 (h b) (g c) (h c): Id Comp Inter WeakCommutativity
 = V3 (h b) (h a) (f a): Id Comp Inter WeakCommutativity
 = V3 (h b) (h a) (f b): Id Comp Inter WeakCommutativity
 = V3 (h b) (h a) (f c): Id Comp Inter WeakCommutativity
 = V3 (h b) (h a) (g a): Id Comp Inter WeakCommutativity
 = V3 (h b) (h a) (g b): Id Comp Inter WeakCommutativity
 = V3 (h b) (h a) (g c): Id Comp Inter WeakCommutativity
 = V3 (h b) (h a) (h a): Id Comp Inter WeakCommutativity
 = V3 (h b) (h a) (h b): Id Comp Inter WeakCommutativity
 = V3 (h b) (h a) (h c): Id Comp Inter WeakCommutativity
 = V3 (h b) (h b) (f a): Id Comp Inter WeakCommutativity
 = V3 (h b) (h b) (f b): Id Comp Inter WeakCommutativity
 = V3 (h b) (h b) (f c): Id Comp Inter WeakCommutativity
 = V3 (h b) (h b) (g a): Id Comp Inter WeakCommutativity
 = V3 (h b) (h b) (g b): Id Comp Inter WeakCommutativity
 = V3 (h b) (h b) (g c): Id Comp Inter WeakCommutativity
 = V3 (h b) (h b) (h a): Id Comp Inter WeakCommutativity
 = V3 (h b) (h b) (h b): Id Comp Inter WeakCommutativity
 = V3 (h b) (h b) (h c): Id      Inter WeakCommutativity
 = V3 (h b) (h c) (f a): Id Comp Inter WeakCommutativity
 = V3 (h b) (h c) (f b): Id Comp Inter WeakCommutativity
 = V3 (h b) (h c) (f c): Id Comp Inter WeakCommutativity
 = V3 (h b) (h c) (g a): Id Comp Inter WeakCommutativity
 = V3 (h b) (h c) (g b): Id Comp Inter WeakCommutativity
 = V3 (h b) (h c) (g c): Id Comp Inter WeakCommutativity
 = V3 (h b) (h c) (h a): Id Comp Inter WeakCommutativity
 = V3 (h b) (h c) (h b): Id Comp Inter WeakCommutativity
 = V3 (h b) (h c) (h c): Id Comp Inter WeakCommutativity
 = V3 (h c) (f a) (f a): Id Comp
 = V3 (h c) (f a) (f b): Id Comp Inter WeakCommutativity
 = V3 (h c) (f a) (f c): Id Comp Inter WeakCommutativity
 = V3 (h c) (f a) (g a): Id Comp Inter WeakCommutativity
 = V3 (h c) (f a) (g b): Id Comp
 = V3 (h c) (f a) (g c): Id Comp Inter WeakCommutativity
 = V3 (h c) (f a) (h a): Id Comp Inter WeakCommutativity
 = V3 (h c) (f a) (h b): Id Comp Inter WeakCommutativity
 = V3 (h c) (f a) (h c): Id Comp
 = V3 (h c) (f b) (f a): Id Comp Inter WeakCommutativity
 = V3 (h c) (f b) (f b): Id Comp Inter WeakCommutativity
 = V3 (h c) (f b) (f c): Id Comp Inter WeakCommutativity
 = V3 (h c) (f b) (g a): Id Comp Inter WeakCommutativity
 = V3 (h c) (f b) (g b): Id Comp Inter WeakCommutativity
 = V3 (h c) (f b) (g c): Id Comp Inter WeakCommutativity
 = V3 (h c) (f b) (h a): Id Comp Inter WeakCommutativity
 = V3 (h c) (f b) (h b): Id Comp Inter WeakCommutativity
 = V3 (h c) (f b) (h c): Id Comp Inter WeakCommutativity
 = V3 (h c) (f c) (f a): Id Comp Inter WeakCommutativity
 = V3 (h c) (f c) (f b): Id Comp Inter WeakCommutativity
 = V3 (h c) (f c) (f c): Id Comp Inter WeakCommutativity
 = V3 (h c) (f c) (g a): Id Comp Inter WeakCommutativity
 = V3 (h c) (f c) (g b): Id Comp Inter WeakCommutativity
 = V3 (h c) (f c) (g c): Id Comp Inter WeakCommutativity
 = V3 (h c) (f c) (h a): Id Comp Inter WeakCommutativity
 = V3 (h c) (f c) (h b): Id Comp Inter WeakCommutativity
 = V3 (h c) (f c) (h c): Id Comp Inter WeakCommutativity
 = V3 (h c) (g a) (f a): Id Comp Inter WeakCommutativity
 = V3 (h c) (g a) (f b): Id Comp Inter WeakCommutativity
 = V3 (h c) (g a) (f c): Id Comp Inter WeakCommutativity
 = V3 (h c) (g a) (g a): Id Comp Inter WeakCommutativity
 = V3 (h c) (g a) (g b): Id Comp Inter WeakCommutativity
 = V3 (h c) (g a) (g c): Id Comp Inter WeakCommutativity
 = V3 (h c) (g a) (h a): Id Comp Inter WeakCommutativity
 = V3 (h c) (g a) (h b): Id Comp Inter WeakCommutativity
 = V3 (h c) (g a) (h c): Id Comp Inter WeakCommutativity
 = V3 (h c) (g b) (f a): Id Comp
 = V3 (h c) (g b) (f b): Id Comp Inter WeakCommutativity
 = V3 (h c) (g b) (f c): Id Comp Inter WeakCommutativity
 = V3 (h c) (g b) (g a): Id Comp Inter WeakCommutativity
 = V3 (h c) (g b) (g b): Id Comp
 = V3 (h c) (g b) (g c): Id Comp Inter WeakCommutativity
 = V3 (h c) (g b) (h a): Id Comp Inter WeakCommutativity
 = V3 (h c) (g b) (h b): Id Comp Inter WeakCommutativity
 = V3 (h c) (g b) (h c): Id
 = V3 (h c) (g c) (f a): Id Comp Inter WeakCommutativity
 = V3 (h c) (g c) (f b): Id Comp Inter WeakCommutativity
 = V3 (h c) (g c) (f c): Id Comp Inter WeakCommutativity
 = V3 (h c) (g c) (g a): Id Comp Inter WeakCommutativity
 = V3 (h c) (g c) (g b): Id Comp Inter WeakCommutativity
 = V3 (h c) (g c) (g c): Id Comp Inter WeakCommutativity
 = V3 (h c) (g c) (h a): Id Comp Inter WeakCommutativity
 = V3 (h c) (g c) (h b): Id Comp Inter WeakCommutativity
 = V3 (h c) (g c) (h c): Id      Inter WeakCommutativity
 = V3 (h c) (h a) (f a): Id Comp Inter WeakCommutativity
 = V3 (h c) (h a) (f b): Id Comp Inter WeakCommutativity
 = V3 (h c) (h a) (f c): Id Comp Inter WeakCommutativity
 = V3 (h c) (h a) (g a): Id Comp Inter WeakCommutativity
 = V3 (h c) (h a) (g b): Id Comp Inter WeakCommutativity
 = V3 (h c) (h a) (g c): Id Comp Inter WeakCommutativity
 = V3 (h c) (h a) (h a): Id Comp Inter WeakCommutativity
 = V3 (h c) (h a) (h b): Id Comp Inter WeakCommutativity
 = V3 (h c) (h a) (h c): Id Comp Inter WeakCommutativity
 = V3 (h c) (h b) (f a): Id Comp Inter WeakCommutativity
 = V3 (h c) (h b) (f b): Id Comp Inter WeakCommutativity
 = V3 (h c) (h b) (f c): Id Comp Inter WeakCommutativity
 = V3 (h c) (h b) (g a): Id Comp Inter WeakCommutativity
 = V3 (h c) (h b) (g b): Id Comp Inter WeakCommutativity
 = V3 (h c) (h b) (g c): Id Comp Inter WeakCommutativity
 = V3 (h c) (h b) (h a): Id Comp Inter WeakCommutativity
 = V3 (h c) (h b) (h b): Id Comp Inter WeakCommutativity
 = V3 (h c) (h b) (h c): Id      Inter WeakCommutativity
 = V3 (h c) (h c) (f a): Id Comp
 = V3 (h c) (h c) (f b): Id Comp Inter WeakCommutativity
 = V3 (h c) (h c) (f c): Id Comp Inter WeakCommutativity
 = V3 (h c) (h c) (g a): Id Comp Inter WeakCommutativity
 = V3 (h c) (h c) (g b): Id Comp
 = V3 (h c) (h c) (g c): Id Comp Inter WeakCommutativity
 = V3 (h c) (h c) (h a): Id Comp Inter WeakCommutativity
 = V3 (h c) (h c) (h b): Id Comp Inter WeakCommutativity
 = V3 (h c) (h c) (h c): Id
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment