Algebra.field

-- Field structure on a small carrier: an additive group and a
-- multiplicative monoid (both codes, so both layer directly),
-- commutativity of each, distributivity, and the two components the
-- Ω-world could not put in a code — stated with Id they can be:
--   * nontriviality is a FUNCTION Id F one zero → 𝟘 — an Id-refutation
--     is data, and stays inside 𝕌, where an Ω-valued ¬ (one ≡ zero)
--     could not go (Core.prop.absurd shows a a ⊥-proof can still be
--     turned into a 𝟘, but only by reflecting an equation, not as a
--     code);
--   * inverses are an UNSQUASHED Σ-code — "here is the inverse", not
--     "one exists" — available to any nonzero x, with nonzero-ness
--     itself an Id-refutation.

import Core.id (Id)
import Algebra.monoid (IsMonoid)
import Algebra.group (IsGroup)

IsField : 𝕌 → 𝕌 using (Algebra.group.IsGroup.unfold, Algebra.monoid.IsMonoid.unfold)
IsField =
  λF. (g : IsGroup F)
    (mm : IsMonoid F)
    × let add = g .π₁ .π₁
          zero = g .π₁ .π₂ .π₁
          mul = mm .π₁
          one = mm .π₂ .π₁
          ((x y : F) → Id _ (add x y) (add y x))
            × ((x y : F) → Id _ (mul x y) (mul y x))
              × ((x y z : F) → Id _ (mul x (add y z)) (add (mul x y) (mul x z)))
                × ((x y z : F) → Id _ (mul (add y z) x) (add (mul y x) (mul z x)))
                  × ((p : Id _ one zero) → 𝟘)
                    × ((x : F) (k : (p : Id _ x zero) → 𝟘) → (y : F) × Id _ (mul x y) one)