{-|
A true †-category has a contravariant endofunctor on C that reverses the
morphisms. I’m not sure how to implement that, so this structure simply uses
pairs of morphisms as the morphism.
-}
let kCat = ../Cat/semigroupal

let vObject = Type

in  λ(object : Kind) →
    λ(cat : ../Kind kCat vObject object) →
        { constraint = cat.constraint
        , arrow = ../../Isomorphism/Type object cat
        }
      : ../Kind kCat vObject object