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

let vObject = Type

in  λ(object : Kind) →
    λ(v : ../Kind kCat Type vObject) →
    λ(cat : ../Kind kCat vObject object) →
        { braid :
            ∀(x : object) →
            ∀(y : object) →
              cat.arrow
                { _1 = cat.product { _1 = x, _2 = y }
                , _2 = cat.product { _1 = y, _2 = x }
                }
        }
      ⩓ ../Type object v cat