let kCat = ../Cat/semigroupal

let vObject = Type

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

in  λ(object : Kind) →
    λ(cat : ../Kind kCat vObject object) →
    λ(category : ../Type object v cat) →
      let op = ../Op/Kind vObject object cat

      let opCategory = ../Op/category object cat category

      let Dagger = ./Kind object cat

      in    { unit =
                λ(a : object) →
                  { to = category.unit a, from = opCategory.unit a }
            , product =
                λ(a : { _1 : object, _2 : object }) →
                λ ( p
                  : ∀(r : Type) →
                    ( ∀(z : object) →
                      Dagger.arrow { _1 = z, _2 = a._2 } →
                      Dagger.arrow { _1 = a._1, _2 = z } →
                        r
                    ) →
                      r
                  ) →
                  { to =
                      category.product
                        a
                        ( λ(r : Type) →
                          λ ( arrowsOut
                            : ∀(z : object) →
                              cat.arrow { _1 = z, _2 = a._2 } →
                              cat.arrow { _1 = a._1, _2 = z } →
                                r
                            ) →
                            p
                              r
                              ( λ(z : object) →
                                λ(f : Dagger.arrow { _1 = z, _2 = a._2 }) →
                                λ(g : Dagger.arrow { _1 = a._1, _2 = z }) →
                                  arrowsOut z f.to g.to
                              )
                        )
                  , from =
                      opCategory.product
                        a
                        ( λ(r : Type) →
                          λ ( arrowsOut
                            : ∀(z : object) →
                              op.arrow { _1 = z, _2 = a._2 } →
                              op.arrow { _1 = a._1, _2 = z } →
                                r
                            ) →
                            p
                              r
                              ( λ(z : object) →
                                λ(f : Dagger.arrow { _1 = z, _2 = a._2 }) →
                                λ(g : Dagger.arrow { _1 = a._1, _2 = z }) →
                                  arrowsOut z f.from g.from
                              )
                        )
                  }
            , hom.map
              =
                λ(a : { _1 : object, _2 : object }) →
                λ(b : { _1 : object, _2 : object }) →
                λ ( fn
                  : { _1 : Dagger.arrow { _1 = b._1, _2 = a._1 }
                    , _2 : Dagger.arrow { _1 = a._2, _2 = b._2 }
                    }
                  ) →
                λ(f : Dagger.arrow a) →
                  { to =
                      category.hom.map a b { _1 = fn._1.to, _2 = fn._2.to } f.to
                  , from =
                      opCategory.hom.map
                        a
                        b
                        { _1 = fn._1.from, _2 = fn._2.from }
                        f.from
                  }
            }
          : ../Type object v Dagger