let Cat = ../../Cat/semigroupal

let Set = ../rig

let vObject = Type

let v =
      ../../Monoidal/Cartesian/extractMonoidal
        Cat
        Type
        vObject
        ../monoidal/cartesian

let Either = Set.additive.product

let Tuple = Set.multiplicative.product

let categoryInstance =
      { unit = λ(a : Type) → λ(x : a) → x
      , product =
          λ(a : { _1 : Type, _2 : Type }) →
          λ(p : ∀(r : Type) → (∀(z : Type) → (z → a._2) → (a._1 → z) → r) → r) →
            p
              (a._1 → a._2)
              ( λ(z : Type) →
                λ(f : z → a._2) →
                λ(g : a._1 → z) →
                λ(x : a._1) →
                  f (g x)
              )
      , hom.map
        =
          λ(a : { _1 : Type, _2 : Type }) →
          λ(b : { _1 : Type, _2 : Type }) →
          λ(f : { _1 : b._1 → a._1, _2 : a._2 → b._2 }) →
          λ(fn : a._1 → a._2) →
          λ(x : b._1) →
            f._2 (fn (f._1 x))
      }

in      { distributivity =
            λ(a : Type) →
            λ(b : Type) →
            λ(c : Type) →
              { to =
                  λ(p : { _1 : a, _2 : Either { _1 = b, _2 = c } }) →
                    let E =
                          Either
                            { _1 = { _1 : a, _2 : b }, _2 = { _1 : a, _2 : c } }

                    in  merge
                          { Left = λ(x : b) → E.Left { _1 = p._1, _2 = x }
                          , Right = λ(x : c) → E.Right { _1 = p._1, _2 = x }
                          }
                          p._2
              , from =
                  λ ( e
                    : Either
                        { _1 = { _1 : a, _2 : b }, _2 = { _1 : a, _2 : c } }
                    ) →
                    let E = Either { _1 = b, _2 = c }

                    in  merge
                          { Left =
                              λ(p : { _1 : a, _2 : b }) →
                                { _1 = p._1, _2 = E.Left p._2 }
                          , Right =
                              λ(p : { _1 : a, _2 : c }) →
                                { _1 = p._1, _2 = E.Right p._2 }
                          }
                          e
              }
        , leftAnnihilation =
            λ(a : Type) →
              { to = λ(p : { _1 : <>, _2 : a }) → p._1
              , from = λ(v : <>) → merge {=} v : { _1 : <>, _2 : a }
              }
        , rightAnnihilation =
            λ(a : Type) →
              { to = λ(p : { _1 : a, _2 : <> }) → p._2
              , from = λ(v : <>) → merge {=} v : { _1 : a, _2 : <> }
              }
        , additive =
              { associativity =
                  λ(a : Type) →
                  λ(b : Type) →
                  λ(c : Type) →
                    { to =
                        λ ( e
                          : Either { _1 = Either { _1 = a, _2 = b }, _2 = c }
                          ) →
                          let EI = Either { _1 = b, _2 = c }

                          let EO = Either { _1 = a, _2 = EI }

                          in  merge
                                { Left =
                                    λ(x : Either { _1 = a, _2 = b }) →
                                      merge
                                        { Left = λ(y : a) → EO.Left y
                                        , Right =
                                            λ(y : b) → EO.Right (EI.Left y)
                                        }
                                        x
                                , Right = λ(x : c) → EO.Right (EI.Right x)
                                }
                                e
                    , from =
                        λ ( e
                          : Either { _1 = a, _2 = Either { _1 = b, _2 = c } }
                          ) →
                          let EI = Either { _1 = a, _2 = b }

                          let EO = Either { _1 = EI, _2 = c }

                          in  merge
                                { Left = λ(x : a) → EO.Left (EI.Left x)
                                , Right =
                                    λ(x : Either { _1 = b, _2 = c }) →
                                      merge
                                        { Left = λ(y : b) → EO.Left (EI.Right y)
                                        , Right = λ(y : c) → EO.Right y
                                        }
                                        x
                                }
                                e
                    }
              , leftIdentity =
                  λ(a : Type) →
                    { to =
                        λ(e : Either { _1 = <>, _2 = a }) →
                          merge
                            { Left = λ(v : <>) → merge {=} v : a
                            , Right = λ(x : a) → x
                            }
                            e
                    , from = (Either { _1 = <>, _2 = a }).Right
                    }
              , rightIdentity =
                  λ(a : Type) →
                    { to =
                        λ(e : Either { _1 = a, _2 = <> }) →
                          merge
                            { Left = λ(x : a) → x
                            , Right = λ(v : <>) → merge {=} v : a
                            }
                            e
                    , from = (Either { _1 = a, _2 = <> }).Left
                    }
              , tensor.map
                =
                  λ(a : { _1 : Type, _2 : Type }) →
                  λ(b : { _1 : Type, _2 : Type }) →
                  λ(f : { _1 : a._1 → b._1, _2 : a._2 → b._2 }) →
                  λ(e : Either a) →
                    let E = Either b

                    in  merge
                          { Left = λ(x : a._1) → E.Left (f._1 x)
                          , Right = λ(x : a._2) → E.Right (f._2 x)
                          }
                          e
              }
            ∧ categoryInstance
        , multiplicative =
              { associativity =
                  λ(a : Type) →
                  λ(b : Type) →
                  λ(c : Type) →
                    { to =
                        λ(p : { _1 : { _1 : a, _2 : b }, _2 : c }) →
                          { _1 = p._1._1, _2 = { _1 = p._1._2, _2 = p._2 } }
                    , from =
                        λ(p : { _1 : a, _2 : { _1 : b, _2 : c } }) →
                          { _1 = { _1 = p._1, _2 = p._2._1 }, _2 = p._2._2 }
                    }
              , leftIdentity =
                  λ(a : Type) →
                    { to = λ(p : { _1 : {}, _2 : a }) → p._2
                    , from = λ(x : a) → { _1 = {=}, _2 = x }
                    }
              , rightIdentity =
                  λ(a : Type) →
                    { to = λ(p : { _1 : a, _2 : {} }) → p._1
                    , from = λ(x : a) → { _1 = x, _2 = {=} }
                    }
              , tensor.map
                =
                  λ(a : { _1 : Type, _2 : Type }) →
                  λ(b : { _1 : Type, _2 : Type }) →
                  λ(f : { _1 : a._1 → b._1, _2 : a._2 → b._2 }) →
                  λ(t : Tuple a) →
                    { _1 = f._1 t._1, _2 = f._2 t._2 }
              }
            ∧ categoryInstance
        }
      ∧ categoryInstance
    : ../../Rig/Type Type v Set