Parametrised modules, instantiated and renaming imports, postfix operators — group theory in textbook notation

[Russoul]

Parametrised modules for the perfect surface: a file may open, after its imports, with a module header — a telescope every def in the file abstracts over — plus the import forms and operator machinery that make the corpus's group theory read like the textbook. The governing discipline is unchanged: every sugar is declared, not inferred — recovery is a checkable rule, the round trip stays α-strict, and nothing moves the trust boundary (defs are Π/λ-closed over the header before they reach Σ and the kernel, so entries are byte-identical to their fully-spelled selves — the groupTheory migration is Σ-α-identical by construction, and the kernel is untouched).

What the corpus reads like now

module {G : 𝕌} (g : El (IsGroup G))

infixl 7 ·
postfix 9 ⁻¹

def · : El G → El G → El G ≔ g .π₁ .π₁
def gAssoc : (x y z : El G) → x · y · z ≡ x · (y · z)
def gInvUniq : {x y : El G} → (x · y ≡ e) → x ⁻¹ ≡ y
def gOpInv : (x y : El G) → (x · y) ⁻¹ ≡ y ⁻¹ · x ⁻¹

and in the two-group modules, per-side notation via renaming instantiated imports:

import (groupTheory g) (· as ·ᴳ, e as eG, ⁻¹ as ⁻¹ᴳ, …)
import (groupTheory h) (· as ·ᴴ, e as eH, ⁻¹ as ⁻¹ᴴ, …)

def homInv : (p : El Hom) (x : El G) → homAp p (x ⁻¹ᴳ) ≡ homAp p x ⁻¹ᴴ
def cosetSplice : {x y z : El G} → x · y ⁻¹ · (y · z ⁻¹) ≡ x · z ⁻¹

The pieces

• Module headers. module {G : 𝕌} (g : El (IsGroup G)) after the imports. Defs elaborate at the parameter context and are Π/λ-closed (skeletons in step) before Σ; sibling references auto-apply the prefix through pre-seeded spine slots — solutions given, not holes — so written arguments, {t} overrides, blanks, and every recovery tier flow past them unchanged. Plain importers see the full telescope with the header's plicity: existing call sites spell exactly what they always spelled.

• Instantiated imports. import (groupTheory g) (·, e, ⁻¹, …) applies a parameterized module at arguments elaborated once, at the importer's own parameter context, through the spine solve itself — written arguments cover the explicit parameters, implicit ones are recovered from their types — then weakened to each use site.

• Renaming imports. o as x on any open installs the importer's surface name for the Σ-def (one visibility-table entry). This is what lets the defs' real names be the notation — def ·, def ⁻¹, def e — while plain importers, who must spell the group argument positionally (a slot infix syntax lacks), keep their prefix spellings byte-for-byte via import groupTheory (· as gop, e as ge, ⁻¹ as ginv, …). A renamed open deliberately leaves its fixity behind; a renamed operator declares its own.

• Double instantiation. The pre-application table keys on the importer's local name, so one module instantiates twice per file with renaming as the disambiguator — groupTheory at g and at h above. A second un-renamed open of the same name is refused, not shadowed. (Type-directed resolution across instantiations — one · for both groups — is deliberately deferred; the overload machinery extends to it naturally, but argument-less names like e stay ambiguous at inference positions.)

• Postfix operators. A third fixity class, postfix 9 ⁻¹, parsed at the projection tier — f x ⁻¹ is (f x) ⁻¹, exactly the .π₁ convention, chaining as x ⁻¹ ⁻¹ — excluded from infix climb and atom positions; the mention form (⁻¹) passes it as a function.

• f {} suppresses the parameter prefix too. The no-insert form already meant "the bare def over its full telescope"; extending that to the header prefix is how a module references its own defs at other instances — Hom {} _ (qIsGroup _ _ s nn) _ h, the hom out of the quotient, blanks recovered as ever.

The corpus conversion

groupTheory (19 defs at (G, g)), subgroup ((G, g); N deliberately stays per-def — the module quantifies over subgroups, several defs never mention N, and its position/plicity varies), quotGroup ((G, g, N), instantiating both predecessors, plus a plain renamed groupTheory import for the quotient-group accessor lemmas — one module imported both ways), groupHom ((G, g, H, h)), and groupIso ((G, g, H, h, p) — "fix a homomorphism", all 41 defs of the kernel/image/first-isomorphism development). The qProj family split out of groupHom (its second group is the quotient, not a parameter): structure lemmas into quotGroup, the projection hom into a new qProj.nova. Where a header fixed one plicity over defs that varied it, external sites on the flipped side spell a blank solved from the proof argument's type (cosetRefl _ s); everything else outside the converted files is textually untouched.

Verification throughout: kernel Σ α-identical across the migration, corpus byte-canonical under check-distill, 162 golden tests (new: parameterized elaboration, single and double instantiation, distill round trip of headers and instantiated imports, notation), 95/95 module elaborations in both store modes, ~10s full corpus elaboration (unchanged).

Recorded limits

One header fixes one plicity per parameter; instantiation arguments resolve at elaboration (the header they mention comes later in the file than the import line); data/clausal items inside parameterized modules are refused for now; qualified operator references in term position (grp.∙ x y) don't parse — renamed or unqualified access covers current use. All in the spec's Status section, with the conversion recipes.