0 | module Data.Coproduct

  2 | import public Data.Ops

  3 | import Proofs.Extensionality

  5 | %default total

  8 | public export

  9 | data (+) : Type -> Type -> Type where

 10 |   ||| Left choice

 11 |   (<+) : a -> a + b

 12 |   ||| Right choice

 13 |   (+>) : b -> a + b

 16 | public export

 17 | choice : (a -> c) -> (b -> c) -> a + b -> c

 18 | choice f g (<+ x) = f x

 19 | choice f g (+> x) = g x

 21 | public export

 22 | dia : a + a -> a

 23 | dia (<+ x) = x

 24 | dia (+> x) = x

 29 | Bifunctor (+) where

 30 |   bimap f g (<+ x) = <+ (f x)

 31 |   bimap f g (+> x) = +> (g x)

 35 | public export

 36 | 0 bifunctorId' : {0 a, b : Type} ->

 37 |                  (x : a + b) ->

 38 |                 Prelude.Interfaces.bimap {f = (+)} (Prelude.id {a}) (Prelude.id {a=b}) x

 39 |                 === x

 40 | bifunctorId' (<+ x) = Refl

 41 | bifunctorId' (+> x) = Refl

 43 | public export 0

 44 | bimapCompose : (x : a + b) ->

 45 |                Prelude.Interfaces.bimap {f = (+)} (g . f) (k . l) x

 46 |            === Prelude.Interfaces.bimap {f = (+)} g k (Prelude.Interfaces.bimap f l x)

 47 | bimapCompose (<+ x) = Refl

 48 | bimapCompose (+> x) = Refl

 50 | public export

 51 | bimapChoice : {0 a, b, a', b' : Type} ->

 52 |               {0 f : a -> Type} -> {0 g : b -> Type} ->

 53 |               {0 f' : a' -> Type} -> {0 g' : b' -> Type} ->

 54 |               (fwd1 : a -> a') ->

 55 |               (bwd1 : (x : a) -> f' (fwd1 x) -> f x) ->

 56 |               (fwd2 : b -> b') ->

 57 |               (bwd2 : (x : b) -> g' (fwd2 x) -> g x) ->

 58 |               (x : a + b) ->

 59 |               choice f' g' (bimap fwd1 fwd2 x) ->

 60 |               choice f g x

 61 | bimapChoice fwd1 bwd1 fwd2 bwd2 (<+ x) y = bwd1 x y

 62 | bimapChoice fwd1 bwd1 fwd2 bwd2 (+> x) y = bwd2 x y

 65 | bimapChoiceId : {0 a, b : Type} -> {0 f : a -> Type} -> {0 g : b -> Type} ->

 66 |                 (x : a + b) ->

 67 |                 (y : choice f g (bimap Basics.id Basics.id x)) ->

 68 |                 bimapChoice {f' = f, g' = g} Basics.id (\_ => Basics.id) Basics.id (\_ => Basics.id) x y

 69 |                 === replace {p = choice f g} (bifunctorId' x) y

 70 | bimapChoiceId (<+ x) y = Refl

 71 | bimapChoiceId (+> x) y = Refl

 74 | bimapChoiceComp : forall a1, a2, a3, b1, b2, b3.

 75 |    {0 f1 : a1 -> Type} -> {0 g1 : b1 -> Type} ->

 76 |    {0 f2 : a2 -> Type} -> {0 g2 : b2 -> Type} ->

 77 |    {0 f3 : a3 -> Type} -> {0 g3 : b3 -> Type} ->

 78 |    (fwda12 : a1 -> a2) ->

 79 |    (bwda12 : (x : a1) -> f2 (fwda12 x) -> f1 x) ->

 80 |    (fwdb12 : b1 -> b2) ->

 81 |    (bwdb12 : (x : b1) -> g2 (fwdb12 x) -> g1 x) ->

 82 |    (fwda23 : a2 -> a3) ->

 83 |    (bwda23 : (x : a2) -> f3 (fwda23 x) -> f2 x) ->

 84 |    (fwdb23 : b2 -> b3) ->

 85 |    (bwdb23 : (x : b2) -> g3 (fwdb23 x) -> g2 x) ->

 86 |    (vx : a1 + b1) ->

 87 |    (vy : Coproduct.choice f3 g3 (bimap (\x => fwda23 (fwda12 x)) (\x => fwdb23 (fwdb12 x)) vx)) ->

 88 |    bimapChoice {f' = f3, g' = g3}

 89 |        (\x => fwda23 (fwda12 x))

 90 |        (\z, x => bwda12 z (bwda23 (fwda12 z) x))

 91 |        (\x => fwdb23 (fwdb12 x))

 92 |        (\z, x => bwdb12 z (bwdb23 (fwdb12 z) x))

 93 |        vx vy

 94 |        === let

 95 |            ppp : choice f3 g3 (bimap fwda23 fwdb23 (bimap fwda12 fwdb12 vx))

 96 |            ppp = (replace {p = choice f3 g3} (bimapCompose vx) vy)

 97 |            choice1 : choice f2 g2 (bimap fwda12 fwdb12 vx)

 98 |            choice1 = bimapChoice {f = f2, f' = f3, g = g2, g' = g3} fwda23 bwda23 fwdb23 bwdb23 (bimap fwda12 fwdb12 vx) ppp

 99 |            choice2 : choice f1 g1 vx

100 |            choice2 = bimapChoice {f = f1, f' = f2, g = g1, g' = g2} fwda12 bwda12 fwdb12 bwdb12 vx choice1

101 |          in choice2

102 | bimapChoiceComp fwda12 bwda12 fwdb12 bwdb12 fwda23 bwda23 fwdb23 bwdb23 (<+ x) vy = Refl

103 | bimapChoiceComp fwda12 bwda12 fwdb12 bwdb12 fwda23 bwda23 fwdb23 bwdb23 (+> x) vy = Refl