Rebase.Data.Profunctor.Strong

first' ≡ dimap swap swap . second'
lmap fst ≡ rmap fst . first'
lmap (second' f) . first' ≡ rmap (second' f) . first'
first' . first' ≡ dimap assoc unassoc . first' where
  assoc ((a,b),c) = (a,(b,c))
  unassoc (a,(b,c)) = ((a,b),c)

second' ≡ dimap swap swap . first'
lmap snd ≡ rmap snd . second'
lmap (first' f) . second' ≡ rmap (first' f) . second'
second' . second' ≡ dimap unassoc assoc . second' where
  assoc ((a,b),c) = (a,(b,c))
  unassoc (a,(b,c)) = ((a,b),c)

unfirst ≡ unsecond . dimap swap swap
lmap (,()) ≡ unfirst . rmap (,())
unfirst . lmap (second f) ≡ unfirst . rmap (second f)
unfirst . unfirst = unfirst . dimap assoc unassoc where
  assoc ((a,b),c) = (a,(b,c))
  unassoc (a,(b,c)) = ((a,b),c)

unsecond ≡ unfirst . dimap swap swap
lmap ((),) ≡ unsecond . rmap ((),)
unsecond . lmap (first f) ≡ unsecond . rmap (first f)
unsecond . unsecond = unsecond . dimap unassoc assoc where
  assoc ((a,b),c) = (a,(b,c))
  unassoc (a,(b,c)) = ((a,b),c)