ga_first f = Code <[ \(x,y) -> ((~~(unCode f) x),y) ]>
ga_second f = Code <[ \(x,y) -> (x ,(~~(unCode f) y)) ]>
ga_cancell = Code <[ \(_,x) -> x ]>
ga_first f = Code <[ \(x,y) -> ((~~(unCode f) x),y) ]>
ga_second f = Code <[ \(x,y) -> (x ,(~~(unCode f) y)) ]>
ga_cancell = Code <[ \(_,x) -> x ]>
-- Note that we trust the user's pair of functions actually are
-- mutually inverse; confirming this in the type system would
-- require very powerful dependent types (such as Coq's). However,
-- Note that we trust the user's pair of functions actually are
-- mutually inverse; confirming this in the type system would
-- require very powerful dependent types (such as Coq's). However,
biga_inv :: g x y -> g y x
-- For any GArrow instance, its mutually inverse pairs form a BiGArrow
biga_inv :: g x y -> g y x
-- For any GArrow instance, its mutually inverse pairs form a BiGArrow
id = GArrowInversePair { forward = id , backward = id }
f . g = GArrowInversePair { forward = (forward f) . (forward g) , backward = (backward g) . (backward f) }
id = GArrowInversePair { forward = id , backward = id }
f . g = GArrowInversePair { forward = (forward f) . (forward g) , backward = (backward g) . (backward f) }
ga_first f = GArrowInversePair { forward = ga_first (forward f), backward = ga_first (backward f) }
ga_second f = GArrowInversePair { forward = ga_second (forward f), backward = ga_second (backward f) }
ga_cancell = GArrowInversePair { forward = ga_cancell , backward = ga_uncancell }
ga_first f = GArrowInversePair { forward = ga_first (forward f), backward = ga_first (backward f) }
ga_second f = GArrowInversePair { forward = ga_second (forward f), backward = ga_second (backward f) }
ga_cancell = GArrowInversePair { forward = ga_cancell , backward = ga_uncancell }
ga_uncancelr = GArrowInversePair { forward = ga_uncancelr , backward = ga_cancelr }
ga_assoc = GArrowInversePair { forward = ga_assoc , backward = ga_unassoc }
ga_unassoc = GArrowInversePair { forward = ga_unassoc , backward = ga_assoc }
ga_uncancelr = GArrowInversePair { forward = ga_uncancelr , backward = ga_cancelr }
ga_assoc = GArrowInversePair { forward = ga_assoc , backward = ga_unassoc }
ga_unassoc = GArrowInversePair { forward = ga_unassoc , backward = ga_assoc }
-- but notice that we can't (in general) get
-- instance GArrowDrop g => GArrowDrop (GArrowInversePair g) where ...
-- but notice that we can't (in general) get
-- instance GArrowDrop g => GArrowDrop (GArrowInversePair g) where ...