F(g ∘ f) = F(g) ∘ F(f)
is the same as ∀fa, (F(g ∘ f))(fa) = (F(g) ∘ F(f))(fa)
(equality of functions is equality of images for all arguments, this is extensionality in HoTT 1 2 3).
The latter is translated as
def covariantComposition[A, B, C](fa: F[A], f: A => B, g: B => C): IsEq[F[C]] =
fa.map(f).map(g) <-> fa.map(f.andThen(g))
(actually, fa.map(f.andThen(g)) <-> fa.map(f).map(g)
).
If you'd like to have "point-free" F(g ∘ f) = F(g) ∘ F(f)
you could write _.map(f.andThen(g)) <-> _.map(f).map(g)
or _.map(f.andThen(g)) <-> (_.map(f)).andThen(_.map(g))
(this is fmap (g . f) = fmap g . fmap f
in Haskell, or more precisely, in some "meta-Haskell").
The 2nd code snippet in your question
def covariantComposition[A, B, C](fa: F[A], f: A => B, g: B => C): IsEq[F[C]] =
fa.map(f).andThen(fa.map(g)) <-> fa.map(f.andThen(g))
is incorrect. fa.map(f).andThen...
doesn't make sense as it was mentioned in comments. You seem to confuse F
and F[A]
.
In category theory, in general categories, f: A -> B
can be just arrows, not necessarily functions (e.g. related pairs in a pre-order if a category is this pre-order), so (F(g ∘ f))(fa)
can make no sense. But the category of types in Scala (or Haskell) is a category where objects are types and morphisms are functions.