f.hs

deriving instance Functor Proof
type YESP = Yoneda (Compose (Either String) Proof)

applyPropRule :: Path -> (Proof (PropCalc a) 
              -> Either String (Proof (PropCalc a)))
              -> Proof (PropCalc a)
              -> Either String (Proof (PropCalc a))
applyPropRule xs f (Proof x) = getCompose
                             . lowerYoneda
                             $ go xs (f . liftYoneda . Compose) x
                             
  where
  go :: Path
     -> (Proof (PropCalc a) -> YESP (PropCalc a))
     -> PropCalc a
     -> YESP (PropCal a)
  go (_:xs) f (Not x)         = go xs f x <&> Not
  go (GoLeft:xs) f (And x y)  = go xs f x <&> (`And` y)
  go (GoLeft:xs) f (Or x y)   = go xs f x <&> (`Or` y)
  go (GoLeft:xs) f (Imp x y)  = go xs f x <&> (`Imp` y)
  go (GoRight:xs) f (And x y) = go xs f x <&> (x `And`)
  go (GoRight:xs) f (Or x y)  = go xs f x <&> (x `Or`)
  go (GoRight:xs) f (Imp x y) = go xs f x <&> (x `Imp`)
  go _ f x = f (Proof x)