Yes, there is a connection. Which makes it all the more strange: Either does correspond as you say which means it has the same properties as the connective. In the correspondence the functor arrow is implication and a pair of functions ‘a -> b’ and ‘b -> a’ is logical equivalence. Using these we can trivially demonstrate the equivalence of Either to the associativity laws using an isomorphism.

That’s what makes his talk strange. He talks about types as sets and seems to expect Either to correspond to set union? If he understood type theory then he’d understand that we use isomorphism and not equality.

You can express type equality in set theory and that is useful and makes sense.

But it doesn’t make sense in his argument.

Malarky? Come on. Doesn’t have associativity? Weird.