/caterwaul/Field/PartiallyOrdered/extractField

Copy path to clipboard

Source

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

let vObject = Type

let object = Type

let cat =
../../Category/Monoidal/Cartesian/extractMonoidal
kCat
vObject
object
../../Category/Set/monoidal/cartesian

in λ(m : object) →
λ(field : ./Type m) →
{ additive =
../../Group/PartiallyOrderedCommutative/extractCommutativeGroup
m
field.additive
, multiplicative = field.multiplicative.{ unit, inverse, product }
}
: ../Type object cat m