/caterwaul/Field/PartiallyOrdered/extractField
Copy path to clipboardSource
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