/caterwaul/Category/Cartesian/extractCategory

Copy path to clipboard

FIXME: Should be able to do cartesian.{ arrow, product }, but Dhall doesn’t like that for some reason.

Source

{-|

**FIXME**: Should be able to do `cartesian.{ arrow, product }`, but Dhall
doesn’t like that for some reason.
-}
λ(cat : ../Monoidal/Sort) →
λ(vObject : Kind) →
λ(object : Kind) →
λ(cartesian : ./Kind cat vObject object) →
{ constraint = cartesian.constraint, arrow = cartesian.arrow }
: ../Kind cat vObject object