FLRP.Closure.FilterIdeal¶
Snow's filter-ideal lemma at Layer D¶
This is the FLRP.Closure.FilterIdeal module of the Agda Universal Algebra Library.
The lemma (Snow, Algebra Universalis 43 (2000)).1
If the lattice L ≤ Eq(X) is representable over a finite set X and L₀ ≤ L is
a sublattice with universe α↑ ∪ β↓ for some α, β ∈ L, then L₀ is
representable.
The manuscript's proof is four lines and entirely constructive: writing λ(L) for
the monoid of unary maps respecting every member of L, it takes θ ∈ L ∖ L₀,
picks witnesses (a , b) ∈ α ∖ θ and (u , v) ∈ θ ∖ β, and defines the
two-valued map
h(x) = a if x ∈ u/β, h(x) = b otherwise.
Then β ≤ ker h, so h respects everything below β; and (a , b) ∈ γ for
every γ ≥ α, so h respects everything above α. Hence h ∈ λ(L₀) while
h violates θ at the pair (u , v). Since λ(L) ⊆ λ(L₀), every
θ ∉ L₀ is violated by some member of λ(L₀), i.e. L₀ = Con ⟨X , λ(L₀)⟩.2
The formalization works at Layer D of the two-layer congruence discipline
(ADR-008), with decidable congruences in place of subsets of Eq(X). Rather than
manipulating the full function monoid λ(L₀), which is never needed and cannot be
enumerated, the ambient lattice is presented as the congruence lattice of an
algebra 𝑨, and the representing algebra of L₀ is the expansion 𝑩 of 𝑨
by one unary operation h(a , b , u) per triple of carrier elements: the
manuscript's two-valued map when (a , b) is an α-pair, and the identity
otherwise (so that the symbol family is total). Both halves of the manuscript
proof survive verbatim:
- each
h(a , b , u)respects every congruence in the filter-ideal union (hMap-compat, the formal reading ofh ∈ λ(L₀)), so every member of the union remains a congruence of𝑩(liftᵈ); - a decidable congruence of
𝑩outside both the filter and the ideal is impossible (h-violation): the witness extraction⊈ᵈ-witnessof FLRP.Representable supplies the pairs(a , b)and(u , v)constructively, and compatibility with the congruence's ownhoperation at(u , v)is the contradiction.
The classification snow, asserting that every decidable
congruence of 𝑩 lies in α↑ ∪ β↓, follows by deciding the two containments
(⊆ᵈ-dec).
The Assembly submodule then turns a closed finite family
presenting the union (in the sense of the engine's closure test: every congruence
of 𝑨 in the union is ≑ a listed member) into the order isomorphism
ConIsoᵈ𝑩 𝑳₀ and the Representableᵈ witness.
This lands with no postulate and no registry assumption, in contrast to the
Kurzweil–Netter duality route (dual-Representableᵈ of
FLRP.Closure.Basic).
The order-theoretic half of the lemma, asserting that α↑ ∪ β↓ is always a
sublattice, is Classical.Structures.Lattice.FilterIdeal; nothing here depends
on it, but the case analyses are the same four lines. The manuscript also derives
adjoined ordinal sums as a corollary of this lemma (α = β = 1_{L₁} × 0_{L₂}
inside L₁ × L₂); the library proves ordinal-sum closure directly in
FLRP.Closure.OrdinalSum, so the corollary is a free consistency check between
the two routes rather than new mathematics.
The setting¶
The construction is parameterized by the ambient algebra 𝑨 (over
an arbitrary finite-level signature), its carrier-finiteness witness, and the
two distinguished decidable congruences α and β.
Nothing requires α and β to be comparable, or the
ambient signature to be unary; the intended instances (coset algebras of
finite groups) are unary, but the extension construction is uniform.
module FilterIdealClosure {𝑆 : Signature 0ℓ 0ℓ} (𝑨 : Algebra {𝑆 = 𝑆} 0ℓ 0ℓ) (𝑭 : FiniteAlgebra 𝑨) (α β : DecCon 𝑨 0ℓ) where open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) renaming ( sym to ≈sym ) open FiniteAlgebra
The extended signature¶
The signature gets one extra unary symbol per triple (a , b , u) of carrier
elements, the parameters of the manuscript's h map: the α-pair (a , b) and
the β-class representative u.
-- The symbol type of the h operations: one per carrier triple. HSym : Type 0ℓ HSym = 𝕌[ 𝑨 ] × 𝕌[ 𝑨 ] × 𝕌[ 𝑨 ] -- The extended signature: the symbols of 𝑆, plus the h symbols (all unary). 𝑆⁺ : Signature 0ℓ 0ℓ 𝑆⁺ = (OperationSymbolsOf 𝑆 ⊎ HSym) , [ ArityOf 𝑆 , (λ _ → Fin 1) ]
The h maps¶
Following the house pattern of FLRP.Representable's decToFin,
the value of h is a pure function hVal of the two decision
verdicts: Is (a , b) an α-pair, and is x in the β-class of u?
This is so that the case analyses below can re-expose the decisions as explicit
arguments. When (a , b) is not an α-pair the map is the identity, which
respects everything; this is what makes the symbol family total without a
Σ-constraint on the triples.
private -- The manuscript's two-valued map, as a function of the two verdicts: -- constant a on the β-class of u, constant b off it, identity if (a , b) -- is not an α-pair. hVal : {P Q : Type 0ℓ} → 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ] → Dec P → Dec Q → 𝕌[ 𝑨 ] hVal a b x (no _) _ = x hVal a b x (yes _) (yes _) = a hVal a b x (yes _) (no _) = b -- A positive α-verdict and a positive β-verdict land on a ... hVal-const-a : {P Q : Type 0ℓ} (a b x : 𝕌[ 𝑨 ]) (dp : Dec P) (dq : Dec Q) → P → Q → hVal a b x dp dq ≡ a hVal-const-a a b x (yes _) (yes _) _ _ = _≡_.refl hVal-const-a a b x (yes _) (no ¬q) _ q = ⊥-elim (¬q q) hVal-const-a a b x (no ¬p) _ p _ = ⊥-elim (¬p p) -- ... a positive α-verdict and a negative β-verdict land on b. hVal-const-b : {P Q : Type 0ℓ} (a b x : 𝕌[ 𝑨 ]) (dp : Dec P) (dq : Dec Q) → P → ¬ Q → hVal a b x dp dq ≡ b hVal-const-b a b x (yes _) (no _) _ _ = _≡_.refl hVal-const-b a b x (yes _) (yes q) _ ¬q = ⊥-elim (¬q q) hVal-const-b a b x (no ¬p) _ p _ = ⊥-elim (¬p p) -- The h operation of the triple (a , b , u), evaluated by running the -- decision procedures of α and β. hMap : HSym → 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ] hMap (a , b , u) x = hVal a b x (proj₂ α a b) (proj₂ β u x)
The map respects the carrier's setoid equality: the α-verdict is fixed, and
≈-equal arguments receive the same β-verdict because congruences respect
≈ (ConRel-resp).
hMap-cong : (s : HSym) {x y : 𝕌[ 𝑨 ]} → x ≈ y → hMap s x ≈ hMap s y hMap-cong (a , b , u) {x} {y} x≈y = aux (α .proj₂ a b) (β .proj₂ u x) (β .proj₂ u y) where open Setoid 𝔻[ 𝑨 ] using () renaming ( refl to ≈refl ) aux : {P : Type 0ℓ} (dp : Dec P) (dx : Dec (ConRel β u x)) (dy : Dec (ConRel β u y)) → hVal a b x dp dx ≈ hVal a b y dp dy aux (no _) _ _ = x≈y aux (yes _) (yes _) (yes _) = ≈refl aux (yes _) (no _) (no _) = ≈refl aux (yes _) (yes βux) (no ¬βuy) = ⊥-elim (¬βuy (ConRel-resp β ≈refl x≈y βux)) aux (yes _) (no ¬βux) (yes βuy) = ⊥-elim (¬βux (ConRel-resp β ≈refl (≈sym x≈y) βuy))
The extended algebra¶
𝑩 interprets the old symbols exactly as 𝑨 does and
each new symbol by its hMap, on the same carrier setoid. The
congruence obligation for the old symbols is discharged through the diagonal
congruence of 𝑨 (whose compatibility field is the statement that
the operations respect ≈).
private -- The operations of 𝑨 respect ≈, read off the diagonal congruence. ≈-compat : (f : OperationSymbolsOf 𝑆) {u v : ArityOf 𝑆 f → 𝕌[ 𝑨 ]} → (∀ i → u i ≈ v i) → (f ^ 𝑨) u ≈ (f ^ 𝑨) v ≈-compat f h = lower (is-compatible (𝟘[ 𝑨 ] {0ℓ} .proj₂) f (lift ∘ h)) -- The interpretation of the extended signature. interp⁺ : (o : OperationSymbolsOf 𝑆⁺) → Op (ArityOf 𝑆⁺ o) 𝕌[ 𝑨 ] interp⁺ (inj₁ f) = f ^ 𝑨 interp⁺ (inj₂ s) = λ as → hMap s (as 0F) interp⁺-cong : (o : OperationSymbolsOf 𝑆⁺) {u v : ArityOf 𝑆⁺ o → 𝕌[ 𝑨 ]} → (∀ i → u i ≈ v i) → interp⁺ o u ≈ interp⁺ o v interp⁺-cong (inj₁ f) h = ≈-compat f h interp⁺-cong (inj₂ s) h = hMap-cong s (h 0F) -- The extension of 𝑨 by the h operations, on the same carrier setoid. 𝑩 : Algebra {𝑆 = 𝑆⁺} 0ℓ 0ℓ 𝑩 = mkAlgebra 𝔻[ 𝑨 ] interp⁺ interp⁺-cong -- Carrier finiteness is inherited: the domain setoid is unchanged. 𝑩-FiniteAlgebra : FiniteAlgebra 𝑩 𝑩-FiniteAlgebra ._≟_ = 𝑭 ._≟_ 𝑩-FiniteAlgebra .card = 𝑭 .card 𝑩-FiniteAlgebra .enum = 𝑭 .enum 𝑩-FiniteAlgebra .enum-sur = 𝑭 .enum-sur
Restriction, the filter-ideal union, and lifting¶
A decidable congruence of 𝑩 restricts to one of 𝑨
by forgetting compatibility with the h symbols; the underlying relation is unchanged.
-- Restriction along the signature inclusion: same relation, fewer operations. restrictᵈ : DecCon 𝑩 0ℓ → DecCon 𝑨 0ℓ restrictᵈ ((θ , θcon) , θ?) = ( θ , mkcon (reflexive θcon) (is-equivalence θcon) (is-compatible θcon ∘ inj₁) ) , θ?
InFilterIdeal γ is membership of a congruence in the universe
α↑ ∪ β↓ of the sublattice L₀, stated by containment.
-- γ lies in the filter above α or in the ideal below β. InFilterIdeal : DecCon 𝑨 0ℓ → Type 0ℓ InFilterIdeal γ = α ⊆ᵈ γ ⊎ γ ⊆ᵈ β
The first half of the manuscript proof: every h operation respects every
congruence in the union. In the filter case the values of h lie in {a , b}
and (a , b) is an α-pair, hence a γ-pair; in the ideal case γ ⊆ β ⊆ ker h,
so γ-related arguments receive the same value. (Together with the trivial
observation that the operations of 𝑨 respect every congruence of
𝑨, this is precisely the manuscript's ops(𝑩) ⊆ λ(L₀).)
hMap-compat : (s : HSym) (γ : DecCon 𝑨 0ℓ) → InFilterIdeal γ → {x y : 𝕌[ 𝑨 ]} → ConRel γ x y → ConRel γ (hMap s x) (hMap s y) hMap-compat (a , b , u) γ (inj₁ α⊆γ) {x} {y} γxy = aux (proj₂ α a b) (proj₂ β u x) (proj₂ β u y) where γ-refl : ∀ {z} → ConRel γ z z γ-refl = IsEquivalence.refl (is-equivalence (proj₂ (proj₁ γ))) γ-sym : ∀ {z w} → ConRel γ z w → ConRel γ w z γ-sym = IsEquivalence.sym (is-equivalence (proj₂ (proj₁ γ))) -- In the filter case the h values are α-related, hence γ-related. aux : (dp : Dec (ConRel α a b)) (dx : Dec (ConRel β u x)) (dy : Dec (ConRel β u y)) → ConRel γ (hVal a b x dp dx) (hVal a b y dp dy) aux (no _) _ _ = γxy aux (yes _) (yes _) (yes _) = γ-refl aux (yes _) (no _) (no _) = γ-refl aux (yes αab) (yes _) (no _) = α⊆γ αab aux (yes αab) (no _) (yes _) = γ-sym (α⊆γ αab) hMap-compat (a , b , u) γ (inj₂ γ⊆β) {x} {y} γxy = aux (proj₂ α a b) (proj₂ β u x) (proj₂ β u y) where γ-refl : ∀ {z} → ConRel γ z z γ-refl = IsEquivalence.refl (is-equivalence (proj₂ (proj₁ γ))) β-sym : ∀ {z w} → ConRel β z w → ConRel β w z β-sym = IsEquivalence.sym (is-equivalence (proj₂ (proj₁ β))) β-trans : ∀ {z w t} → ConRel β z w → ConRel β w t → ConRel β z t β-trans = IsEquivalence.trans (is-equivalence (proj₂ (proj₁ β))) -- In the ideal case γ ⊆ β ⊆ ker h: γ-related arguments share a β-class -- verdict, so h sends them to literally the same value. aux : (dp : Dec (ConRel α a b)) (dx : Dec (ConRel β u x)) (dy : Dec (ConRel β u y)) → ConRel γ (hVal a b x dp dx) (hVal a b y dp dy) aux (no _) _ _ = γxy aux (yes _) (yes _) (yes _) = γ-refl aux (yes _) (no _) (no _) = γ-refl aux (yes _) (yes βux) (no ¬βuy) = ⊥-elim (¬βuy (β-trans βux (γ⊆β γxy))) aux (yes _) (no ¬βux) (yes βuy) = ⊥-elim (¬βux (β-trans βuy (β-sym (γ⊆β γxy))))
Consequently every congruence of 𝑨 in the union lifts to a
congruence of 𝑩 with the same underlying relation.
-- A member of the filter-ideal union is a congruence of the extension. liftᵈ : (γ : DecCon 𝑨 0ℓ) → InFilterIdeal γ → DecCon 𝑩 0ℓ liftᵈ γ@((θ , θcon) , θ?) mem = ( θ , mkcon (reflexive θcon) (is-equivalence θcon) compat ) , θ? where compat : 𝑩 ∣≈ θ compat (inj₁ f) = is-compatible θcon f compat (inj₂ s) = λ h → hMap-compat s γ mem (h 0F)
The violation step and the classification¶
The second half of the manuscript proof. Suppose a decidable congruence of
𝑩 lies outside the filter and outside the ideal. Both
failed containments yield concrete witnesses (⊈ᵈ-witness):
an α-pair (a , b) not related by the congruence, and a related pair
(u , v) that is not a β-pair. The congruence must be compatible with its
own operation h(a , b , u), but that operation sends (u , v) to
(a , b), a contradiction.
h-violation : (d : DecCon 𝑩 0ℓ) → ¬ α ⊆ᵈ restrictᵈ d → ¬ restrictᵈ d ⊆ᵈ β → ⊥ h-violation d@((_θ_ , θcon) , _) ¬filter ¬ideal = step where wα = ⊈ᵈ-witness 𝑭 α (restrictᵈ d) ¬filter wβ = ⊈ᵈ-witness 𝑭 (restrictᵈ d) β ¬ideal a b u v : 𝕌[ 𝑨 ] a = wα .proj₁ b = wα .proj₂ .proj₁ u = wβ .proj₁ v = wβ .proj₂ .proj₁ αab : ConRel α a b αab = wα .proj₂ .proj₂ .proj₁ ¬θab : ¬ a θ b ¬θab = wα .proj₂ .proj₂ .proj₂ θuv : u θ v θuv = wβ .proj₂ .proj₂ .proj₁ ¬βuv : ¬ ConRel β u v ¬βuv = wβ .proj₂ .proj₂ .proj₂ β-refl : ConRel β u u β-refl = IsEquivalence.refl (is-equivalence (β .proj₁ .proj₂)) -- Compatibility of the congruence with its own h operation, at (u , v). θ-h : ConRel d (hMap (a , b , u) u) (hMap (a , b , u) v) θ-h = is-compatible θcon (inj₂ (a , b , u)) (λ _ → θuv) -- h sends u to a (u is in its own β-class) and v to b ((u , v) ∉ β). step : ⊥ step = ¬θab ( subst₂ (ConRel d) (hVal-const-a a b u (proj₂ α a b) (proj₂ β u u) αab β-refl) (hVal-const-b a b v (proj₂ α a b) (proj₂ β u v) αab ¬βuv) θ-h )
Snow's lemma (classification form). Deciding the two containments over the finite carrier leaves the impossible case to the violation step.
-- Every decidable congruence of the extension lies in the filter or the ideal. snow : (d : DecCon 𝑩 0ℓ) → InFilterIdeal (restrictᵈ d) snow d with ⊆ᵈ-dec 𝑭 α (restrictᵈ d) ... | yes filter = inj₁ filter ... | no ¬filter with ⊆ᵈ-dec 𝑭 (restrictᵈ d) β ... | yes ideal = inj₂ ideal ... | no ¬ideal = ⊥-elim (h-violation d ¬filter ¬ideal)
Assembly: from a closed finite family to Representableᵈ¶
The remaining inputs are exactly the Layer-D presentation data of the
sublattice L₀:
- the abstract target
𝑳, aFiniteLatticewhose carrier indexes the members ofL₀; - the concrete family
γof decidable congruences of𝑨, each in the union (γ-mem); - closedness of the family (
classify): every congruence of𝑨in the union is≑a listed member, the constructive content of the engine-side closure testInv(λ(L₀)) = L₀, supplied per application (for the coset-algebra instances it is the WP-3 bridge composed with a subgroup-interval classification); - order agreement (
γ-mono/γ-reflect): containment of family members matches the meet order of the target's tables.
Nothing here forces any of the decision procedures to run during
type-checking; the heavy decisions (⊆ᵈ-dec inside
snow) stay unevaluated because every proof below is by
containment reasoning and antisymmetry, never by normalization.
module Assembly (𝑳 : FiniteLattice) (open FiniteLattice 𝑳 renaming (Carrier to L)) (γ : L → DecCon 𝑨 0ℓ) (γ-mem : ∀ k → InFilterIdeal (γ k)) (classify : (e : DecCon 𝑨 0ℓ) → InFilterIdeal e → Σ[ k ∈ L ] proj₁ e ≑ proj₁ (γ k)) (γ-mono : ∀ k l → γ k ⊆ᵈ γ l → k ∧ l ≡ k) (γ-reflect : ∀ k l → k ∧ l ≡ k → γ k ⊆ᵈ γ l) where private 𝑳₀ = toLattice 𝑳 open Lattice-Order 𝑳₀ using ( ≤-antisym )
The two maps: classify the restriction; lift the listed member.
to₀ : DecCon 𝑩 0ℓ → L to₀ d = classify (restrictᵈ d) (snow d) .proj₁ from₀ : L → DecCon 𝑩 0ℓ from₀ k = liftᵈ (γ k) (γ-mem k)
Monotonicity in both directions, through the family's order agreement; the round trips, by the classification equalities and antisymmetry.
to₀-mono : {d e : DecCon 𝑩 0ℓ} → d ⊆ᵈ e → to₀ d ∧ to₀ e ≡ to₀ d to₀-mono {d} {e} d⊆e = γ-mono (to₀ d) (to₀ e) λ p → proj₁ (proj₂ (classify (restrictᵈ e) (snow e))) (d⊆e (proj₂ (proj₂ (classify (restrictᵈ d) (snow d))) p)) from₀-mono : {k l : L} → k ∧ l ≡ k → from₀ k ⊆ᵈ from₀ l from₀-mono {k} {l} = γ-reflect k l to₀∘from₀ : (k : L) → to₀ (from₀ k) ≡ k to₀∘from₀ k = ≤-antisym (γ-mono (to₀ (from₀ k)) k (classify (restrictᵈ (from₀ k)) (snow (from₀ k)) .proj₂ .proj₂)) (γ-mono k (to₀ (from₀ k)) (classify (restrictᵈ (from₀ k)) (snow (from₀ k)) .proj₂ .proj₁ )) from₀∘to₀ : (d : DecCon 𝑩 0ℓ) → from₀ (to₀ d) ≑ᵈ d from₀∘to₀ d = classify (restrictᵈ d) (snow d) .proj₂ .proj₂ , classify (restrictᵈ d) (snow d) .proj₂ .proj₁
The order isomorphism, and the representability witness once the extended signature's finiteness data are supplied.
filterIdeal-ConIsoᵈ : ConIsoᵈ 𝑩 𝑳₀ filterIdeal-ConIsoᵈ = record { to = to₀ ; from = from₀ ; to-mono = to₀-mono ; from-mono = from₀-mono ; to∘from = to₀∘from₀ ; from∘to = from₀∘to₀ } -- Snow's filter-ideal lemma, packaged: the sublattice α↑ ∪ β↓ is -- decidably representable, witnessed by the extended algebra. filterIdeal-Representableᵈ : FiniteSignature 𝑆⁺ → Representableᵈ 𝑳₀ filterIdeal-Representableᵈ fs = record { sigᵈ = 𝑆⁺ ; algᵈ = 𝑩 ; finiteᵈ = 𝑩-FiniteAlgebra ; finsigᵈ = fs ; con-isoᵈ = filterIdeal-ConIsoᵈ }
Finiteness of the extended signature¶
The extension adds n³ unary symbols to a finite finitary signature, so it is
finite finitary whenever the carrier has an ≡-surjective enumeration (per the
caveat of Classical.Signatures.Finite, the raw carrier, the setoid
enumeration of a FiniteAlgebra does not suffice). The enumeration
of the symbol sum and of the triples is assembled from the standard
Fin splitting and pairing combinators.
private -- ≡-surjective enumeration of a pair type from ones of the components. pairEnum : {A B : Type 0ℓ} {m n : ℕ} → (Fin m → A) → (Fin n → B) → Fin (m * n) → A × B pairEnum {m = m} {n = n} eA eB k = eA (remQuot {m} n k .proj₁) , eB (remQuot {m} n k .proj₂) pairEnum-sur : {A B : Type 0ℓ} {m n : ℕ} (eA : Fin m → A) (eB : Fin n → B) → (∀ a → ∃[ i ] eA i ≡ a) → (∀ b → ∃[ j ] eB j ≡ b) → (p : A × B) → ∃[ k ] pairEnum eA eB k ≡ p pairEnum-sur {n = n} eA eB eA-sur eB-sur (a , b) with eA-sur a | eB-sur b ... | i , ea | j , eb = combine i j , trans (cong (λ q → eA (proj₁ q) , eB (proj₂ q)) (remQuot-combine i j)) (cong₂ _,_ ea eb) -- ≡-surjective enumeration of a sum type from ones of the summands. sumEnum : {A B : Type 0ℓ} {m n : ℕ} → (Fin m → A) → (Fin n → B) → Fin (m + n) → A ⊎ B sumEnum {m = m} eA eB k = ⊎-map eA eB (splitAt m k) sumEnum-sur : {A B : Type 0ℓ} {m n : ℕ} (eA : Fin m → A) (eB : Fin n → B) → (∀ a → ∃[ i ] eA i ≡ a) → (∀ b → ∃[ j ] eB j ≡ b) → (s : A ⊎ B) → ∃[ k ] sumEnum eA eB k ≡ s sumEnum-sur {m = m} {n = n} eA eB eA-sur eB-sur (inj₁ a) with eA-sur a ... | i , ea = (i ↑ˡ n) , trans (cong (⊎-map eA eB) (splitAt-↑ˡ m i n)) (cong inj₁ ea) sumEnum-sur {m = m} {n = n} eA eB eA-sur eB-sur (inj₂ b) with eB-sur b ... | j , eb = (m ↑ʳ j) , trans (cong (⊎-map eA eB) (splitAt-↑ʳ m n j)) (cong inj₂ eb) open FiniteSignature -- The extended signature is finite finitary, given an ≡-surjective carrier -- enumeration. 𝑆⁺-FiniteSignature : FiniteSignature 𝑆 → (n : ℕ) (e : Fin n → 𝕌[ 𝑨 ]) (e-sur : ∀ x → ∃[ i ] e i ≡ x) → FiniteSignature 𝑆⁺ 𝑆⁺-FiniteSignature 𝑺 n e e-sur .opCard = 𝑺 .opCard + n * (n * n) 𝑆⁺-FiniteSignature 𝑺 n e e-sur .opEnum = sumEnum (𝑺 .opEnum) (pairEnum e (pairEnum e e)) 𝑆⁺-FiniteSignature 𝑺 n e e-sur .opEnum-sur = sumEnum-sur (𝑺 .opEnum) (pairEnum e (pairEnum e e)) (𝑺 .opEnum-sur) (pairEnum-sur e (pairEnum e e) e-sur (pairEnum-sur e e e-sur e-sur)) 𝑆⁺-FiniteSignature 𝑺 n e e-sur .finitary (inj₁ f) = 𝑺 .finitary f 𝑆⁺-FiniteSignature 𝑺 n e e-sur .finitary (inj₂ _) = 1 , ↔-id _