CoAndProductAdjunction.hs

module Adjunctions where

data Coproduct n x
  where
  First :: x -> Coproduct 'Z x
  Next :: Either (Coproduct n x) x -> Coproduct ('S n) x

fold :: Coproduct n x -> x
fold (First x) = x
fold (Next (Right x)) = x
fold (Next (Left x)) = fold x

inj :: SNat n -> x -> Coproduct n x
inj SZ = First
inj (SS n) = Next . Left . inj n

data Product' n x
  where
  Only :: x -> Product' 'Z x
  And :: x -> (Product' n x) -> Product' ('S n) x

head' :: Product' ('S n) x -> x
head' (And x _) = x

tail' :: Product' ('S n) x -> Product' n x
tail' (And _ xs) = xs

afwd :: SNat n -> (Coproduct n y -> x) -> (y -> Product' n x)
afwd SZ f y = Only $ f $ First y
afwd (SS n) f y = And (f $ inj (SS n) y) rec
  where
  rec = afwd n (f . Next . Left) y

abwd :: SNat n -> (y -> Product' n x) -> (Coproduct n y -> x)
abwd SZ f (First y) = case (f y) of (Only x) -> x
abwd (SS n) f (Next (Right y)) = head' $ f y
abwd (SS n) f (Next (Left r)) = abwd n (tail' . f) r