Demo¶

A proof assistant is a program that checks proofs. It cannot be talked into accepting one: it type-checks the text it is given and answers with an exit code. Here the proof assistant is Agda, the writer is a language model, and Agda's answer is the only judge of what the model wrote.

agda-mcp is a server that lets the model ask Agda questions while it works, the way a person does in an editor: what is the type of this expression, what does this module export, does this file check. This page shows the server doing that, with nothing invented. The clocks are measured from archived sessions, the sessions are replayed from their transcripts, and every figure comes from a file beside this page that names the run it was read from.

Three clocks¶

What the server changes is the price of a question, not the price of a verdict. A question about a file the server already holds is answered from the loaded file, in milliseconds. A verdict, whether the file type-checks, is a fresh run of Agda every time, on the server and off it, and costs seconds. In a real development the same verdict from a shell takes longer still: the third bar is one module's check in the field, and the whole-library check a development finally gates on runs from tens of seconds to minutes. The bars start together, and each stops when its measured time is up.

A question about a file the server already holds3 ms
The median of 165 questions the interaction lane answered about a file it already held (p90 22 ms, longest 93 ms); the same questions when the file had to be loaded first took 4.8 s at the median. Measured on arm-surface-mcp-1 and arm-surface-mcp-2 and arm-surface-both-1 and arm-verdict-mcp-1 and arm-verdict-mcp-2, Sonnet 5 on the server of 2026-09-26.
A verdict: check_file, a fresh batch run of Agda2.0 s
The median of 283 calls of check_file on the same runs (p90 5.5 s, longest 7.9 s), each a run of agda over the file, answered from its exit code.
The same verdict from a shell, in a real development10 s
Not from the runs above: the archive holds no shell timings. This is the median of the single-module agda checks a shell ran in an agda-algebras session, as agda-native-air issue 83 recorded them and ADR 0002 § 2 quotes them; the whole-library check those sessions gate on runs 20 s to 10 min (ADR 0002 § 12).

One scale: a bar’s length is its time, and the bars start together. Every figure is in numbers.json beside this page, with the run ids and the field it was read from.

Three sessions, one lemma¶

The lemma is about algebras: if one algebra sits inside a second as a subalgebra, and the second is isomorphic to a third, then the first sits inside the third. The library it comes from already proves it. The statement was put to the model with that proof removed and a hole in its place, and the model was free to read the library. The same model met it three times, with the server, with a shell that had Agda on it, and with both. Each tab replays what the model typed and what it was told back, in the order it happened. A call types the way the model typed it; the answer under it appears whole, because the tool answered in one response, and it is here in full behind a control that says how long it is. The verdict at the end of each session is the archive's judge's, not this page's.

instrument	turns	questions to Agda	corpus searches	library reads	edits	verdicts	each verdict, in order
server only	12	5	2	1	1	1	accepted
shell only	15	0	0	9	2	2	refused, accepted
server and shell	14	0	0	8	2	2	refused, accepted

Counted from each session’s steps: a question is a lane-answered tool (type_of, exports_of, definition_of, get_goal); a search is a corpus tool; a library read is a shell command the archive’s audit classed as one, or a read of a file outside the work directory; a verdict is check_file or agda run in the shell, accepted or refused as the tool answered.

Three sessions on one lemma settle nothing about a sweep, and the score below says how the sweep went. What they show is the shape of the difference. With the server alone, the model asked Agda what things were before it wrote, what a module exports and what type a name has, and its one verdict was accepted. With a shell, alone or beside the server, it read the library through grep, wrote from what it found, and had its first verdict refused for a name out of scope, which is the kind of question the first session had asked. Fewer trials, and a first proof that holds, are the early signs worth watching, and there is a reason to want them beyond the score: as the theorems get harder, a proof found by trial and error is likely to be longer and harder for a person to read than it needs to be, and elegance is worth something to the people who read proofs. Whether questions keep standing in for trials where nothing on disk can be looked up is what the harder tier is for.

≤-trans-≅′, server only

Server only. The corpus is searched, definition_of pays for loading the file, and the questions after it are answered on the loaded file in milliseconds. Then one edit, and one verdict, which is a fresh run of Agda.

model: Sonnet 5 (claude-sonnet-5)
instrument: server only
run: arm162-mcp-1 2026-09-21
server: the server of 2026-09-21 (fourteen tools, the libraries' sources readable on every arm)
client: 2.1.261 (Claude Code)
turns: 12
tool calls: 11 Read ×2, search_by_name ×1, search_by_type ×1, definition_of ×1, exports_of ×2, type_of ×2, Edit ×1, check_file ×1
wall clock: 48 s (indicative: subjects ran three at a time)
cost, list price: USD 0.39

the statement, as the obligation states it, with the proof removed

{𝓞 𝓥 α ρᵃ β ρᵇ γ ρᶜ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ} →  𝑨 ≤ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≤ 𝑪

the session, 12 turns and 11 tool calls

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

files

Read(file_path: <work>/Subalgebras-sub-trans-iso.agda)

answered

1 -- Subalgebras-sub-trans-iso.agda

the whole answer, as the model saw it (963 characters of text)

1   -- Subalgebras-sub-trans-iso.agda
2   --
3   -- File: data/benchmarks/agda-algebras-v0/obligations/Subalgebras-sub-trans-iso.agda
4   --
5   -- Benchmark obligation: algebras-subalgebras-sub-trans-iso
6   -- Difficulty: non-obvious
7   -- Source: Setoid.Subalgebras.Properties (agda-algebras)
8   -- Import stratum: wholesale
9   -- Strategy: pairing
10  --
11  module Subalgebras-sub-trans-iso where
12  
13  open import AgdaDojang.Debug
14  
15  open import Agda.Primitive   using ( Level )
16  open import Data.Product     using ( _,_ ; proj₁ ; proj₂ )
17  
18  open import Overture              using ( Signature )
19  open import Setoid.Algebras       using ( Algebra )
20  open import Setoid.Functions
21  open import Setoid.Homomorphisms
22  open import Setoid.Subalgebras
23  
24  ≤-trans-≅′ : {𝓞 𝓥 α ρᵃ β ρᵇ γ ρᶜ : Level} {𝑆 : Signature 𝓞 𝓥}
25               {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ}
26    →  𝑨 ≤ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≤ 𝑪
27  ≤-trans-≅′ p B≅C = {!!}
28

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

agda-mcp

search_by_name(pattern: ≤-trans-≅)

answered

results: 1

the whole answer, as the model saw it (507 characters of JSON)

[{"defKind":"function","hasBody":true,"module":"Setoid.Subalgebras.Properties","prettyQname":"Setoid.Subalgebras.Properties.≤-trans-≅","type":"{𝑆.𝓞 𝑆.𝓥 : Agda.Primitive.Level}\n{𝑆 : Overture.Signatures.Signature 𝑆.𝓞 𝑆.𝓥}\n{α ρᵃ β ρᵇ γ ρᶜ : Agda.Primitive.Level}\n{𝑨 : Setoid.Algebras.Basic.Algebra α ρᵃ}\n{𝑩 : Setoid.Algebras.Basic.Algebra β ρᵇ}\n{𝑪 : Setoid.Algebras.Basic.Algebra γ ρᶜ} →\n𝑨 Setoid.Subalgebras.Basic._.≤ 𝑩 →\n𝑩 Setoid.Homomorphisms.Isomorphisms._.≅ 𝑪 →\n𝑨 Setoid.Subalgebras.Basic._.≤ 𝑪"}]

agda-mcp

search_by_type(pattern: ≤, limit: 30)

answered

results: 30

the whole answer, as the model saw it (18,762 characters of JSON)

[{"defKind":"function","hasBody":true,"module":"Classical.Properties.Lattice.FiniteOrder","prettyQname":"Classical.Properties.Lattice.FiniteOrder._≤?_","type":"{n : Agda.Builtin.Nat.Nat}\n(_∧_\n : Data.Fin.Base.Fin n → Data.Fin.Base.Fin n → Data.Fin.Base.Fin n)\n(a b : Data.Fin.Base.Fin n) →\nRelation.Nullary.Decidable.Core.Dec\n((_∧_ Classical.Properties.Lattice.FiniteOrder.≤ a) b)"},{"defKind":"function","hasBody":true,"module":"Classical.Properties.Lattice.Lattice-Order","prettyQname":"Classical.Properties.Lattice.Lattice-Order.∧-greatest","type":"{α ρ : Agda.Primitive.Level}\n(𝑳 : Classical.Structures.Lattice.Basic.Lattice α ρ)\n{x y z\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳))} →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ z) x →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ z) y →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ z)\n((𝑳 Classical.Structures.Lattice.Basic.Lattice-Op.∧ x) y)"},{"defKind":"function","hasBody":true,"module":"Classical.Properties.Lattice.Lattice-Order","prettyQname":"Classical.Properties.Lattice.Lattice-Order.∧-lowerʳ","type":"{α ρ : Agda.Primitive.Level}\n(𝑳 : Classical.Structures.Lattice.Basic.Lattice α ρ)\n{x y\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Structures.Lattice.Basic.Lattice-Op.𝑨 𝑳))} →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤\n (𝑳 Classical.Structures.Lattice.Basic.Lattice-Op.∧ x) y)\ny"},{"defKind":"function","hasBody":true,"module":"Classical.Properties.Lattice.Lattice-Order","prettyQname":"Classical.Properties.Lattice.Lattice-Order.∧-lowerˡ","type":"{α ρ : Agda.Primitive.Level}\n(𝑳 : Classical.Structures.Lattice.Basic.Lattice α ρ)\n{x y\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Structures.Lattice.Basic.Lattice-Op.𝑨 𝑳))} →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤\n (𝑳 Classical.Structures.Lattice.Basic.Lattice-Op.∧ x) y)\nx"},{"defKind":"function","hasBody":true,"module":"Classical.Properties.Lattice.Lattice-Order","prettyQname":"Classical.Properties.Lattice.Lattice-Order.∨-least","type":"{α ρ : Agda.Primitive.Level}\n(𝑳 : Classical.Structures.Lattice.Basic.Lattice α ρ)\n{x y z\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳))} →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ x) z →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ y) z →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤\n (𝑳 Classical.Structures.Lattice.Basic.Lattice-Op.∨ x) y)\nz"},{"defKind":"function","hasBody":true,"module":"Classical.Properties.Lattice.Lattice-Order","prettyQname":"Classical.Properties.Lattice.Lattice-Order.∨-upperʳ","type":"{α ρ : Agda.Primitive.Level}\n(𝑳 : Classical.Structures.Lattice.Basic.Lattice α ρ)\n{x\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Structures.Lattice.Basic.Lattice-Op.𝑨 𝑳))}\n{y\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳))} →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ y)\n((𝑳 Classical.Structures.Lattice.Basic.Lattice-Op.∨ x) y)"},{"defKind":"function","hasBody":true,"module":"Classical.Properties.Lattice.Lattice-Order","prettyQname":"Classical.Properties.Lattice.Lattice-Order.∨-upperˡ","type":"{α ρ : Agda.Primitive.Level}\n(𝑳 : Classical.Structures.Lattice.Basic.Lattice α ρ)\n{x\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳))}\n{y\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Structures.Lattice.Basic.Lattice-Op.𝑨 𝑳))} →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ x)\n((𝑳 Classical.Structures.Lattice.Basic.Lattice-Op.∨ x) y)"},{"defKind":"function","hasBody":true,"module":"Classical.Properties.Lattice.Lattice-Order","prettyQname":"Classical.Properties.Lattice.Lattice-Order.≤-antisym","type":"{α ρ : Agda.Primitive.Level}\n(𝑳 : Classical.Structures.Lattice.Basic.Lattice α ρ)\n{x y\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳))} →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ x) y →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ y) x →\n(Setoid.Algebras.Basic.𝔻[\n Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳 ]\n Relation.Binary.Bundles.Setoid.≈ x)\ny"},{"defKind":"function","hasBody":true,"module":"Classical.Properties.Lattice.Lattice-Order","prettyQname":"Classical.Properties.Lattice.Lattice-Order.≤-from-∨","type":"{α ρ : Agda.Primitive.Level}\n(𝑳 : Classical.Structures.Lattice.Basic.Lattice α ρ)\n{x y\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Structures.Lattice.Basic.Lattice-Op.𝑨 𝑳))} →\n(Setoid.Algebras.Basic.𝔻[\n Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳 ]\n Relation.Binary.Bundles.Setoid.≈\n (𝑳 Classical.Structures.Lattice.Basic.Lattice-Op.∨ x) y)\ny →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ x) y"},{"defKind":"function","hasBody":true,"module":"Classical.Properties.Lattice.Lattice-Order","prettyQname":"Classical.Properties.Lattice.Lattice-Order.≤-refl","type":"{α ρ : Agda.Primitive.Level}\n(𝑳 : Classical.Structures.Lattice.Basic.Lattice α ρ)\n{x\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳))} →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ x) x"},{"defKind":"function","hasBody":true,"module":"Classical.Properties.Lattice.Lattice-Order","prettyQname":"Classical.Properties.Lattice.Lattice-Order.≤-reflexive","type":"{α ρ : Agda.Primitive.Level}\n(𝑳 : Classical.Structures.Lattice.Basic.Lattice α ρ)\n{x y\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳))} →\n(Setoid.Algebras.Basic.𝔻[\n Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳 ]\n Relation.Binary.Bundles.Setoid.≈ x)\ny →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ x) y"},{"defKind":"function","hasBody":true,"module":"Classical.Properties.Lattice.Lattice-Order","prettyQname":"Classical.Properties.Lattice.Lattice-Order.≤-respʳ-≈","type":"{α ρ : Agda.Primitive.Level}\n(𝑳 : Classical.Structures.Lattice.Basic.Lattice α ρ)\n{x y y'\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳))} →\n(Setoid.Algebras.Basic.𝔻[\n Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳 ]\n Relation.Binary.Bundles.Setoid.≈ y)\ny' →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ x) y →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ x) y'"},{"defKind":"function","hasBody":true,"module":"Classical.Properties.Lattice.Lattice-Order","prettyQname":"Classical.Properties.Lattice.Lattice-Order.≤-respˡ-≈","type":"{α ρ : Agda.Primitive.Level}\n(𝑳 : Classical.Structures.Lattice.Basic.Lattice α ρ)\n{x x' y\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳))} →\n(Setoid.Algebras.Basic.𝔻[\n Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳 ]\n Relation.Binary.Bundles.Setoid.≈ x)\nx' →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ x) y →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ x') y"},{"defKind":"function","hasBody":true,"module":"Classical.Properties.Lattice.Lattice-Order","prettyQname":"Classical.Properties.Lattice.Lattice-Order.≤-trans","type":"{α ρ : Agda.Primitive.Level}\n(𝑳 : Classical.Structures.Lattice.Basic.Lattice α ρ)\n{x y z\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳))} →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ x) y →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ y) z →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ x) z"},{"defKind":"function","hasBody":true,"module":"Classical.Properties.Lattice.Lattice-Order","prettyQname":"Classical.Properties.Lattice.Lattice-Order.≤-via-∨","type":"{α ρ : Agda.Primitive.Level}\n(𝑳 : Classical.Structures.Lattice.Basic.Lattice α ρ)\n{x y\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Setoid.Algebras.Basic.Algebra.Domain\n    (Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳))} →\n(𝑳 Classical.Properties.Lattice.Lattice-Order.≤ x) y →\n(Setoid.Algebras.Basic.𝔻[\n Classical.Properties.Lattice.Lattice-Order.𝑨 𝑳 ]\n Relation.Binary.Bundles.Setoid.≈\n (𝑳 Classical.Structures.Lattice.Basic.Lattice-Op.∨ x) y)\ny"},{"defKind":"function","hasBody":true,"module":"Classical.Structures.Group.Congruences.GroupCongruences","prettyQname":"Classical.Structures.Group.Congruences.GroupCongruences.congruenceOf-mono","type":"{α ρ : Agda.Primitive.Level}\n(𝒢 : Classical.Structures.Group.Basic.Group α ρ)\n{ℓ : Agda.Primitive.Level}\n(𝑴 𝑵\n : Classical.Structures.Group.Congruences.GroupCongruences.NormalSubgroup\n   𝒢 ℓ) →\n(𝒢 Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ 𝑴)\n𝑵 →\nClassical.Structures.Group.Congruences.GroupCongruences.congruenceOf\n𝒢 𝑴\nSetoid.Congruences.Lattice._.⊆\nClassical.Structures.Group.Congruences.GroupCongruences.congruenceOf\n𝒢 𝑵"},{"defKind":"function","hasBody":true,"module":"Classical.Structures.Group.Congruences.GroupCongruences","prettyQname":"Classical.Structures.Group.Congruences.GroupCongruences.fwd","type":"{α ρ : Agda.Primitive.Level}\n(𝒢 : Classical.Structures.Group.Basic.Group α ρ)\n{ℓ : Agda.Primitive.Level}\n(𝑵\n : Classical.Structures.Group.Congruences.GroupCongruences.NormalSubgroup\n   𝒢 ℓ) →\n(𝒢 Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ\n Classical.Structures.Group.Congruences.GroupCongruences.normalOf 𝒢\n (Classical.Structures.Group.Congruences.GroupCongruences.congruenceOf\n  𝒢 𝑵))\n𝑵"},{"defKind":"function","hasBody":true,"module":"Classical.Structures.Group.Congruences.GroupCongruences","prettyQname":"Classical.Structures.Group.Congruences.GroupCongruences.normalOf-mono","type":"{α ρ : Agda.Primitive.Level}\n(𝒢 : Classical.Structures.Group.Basic.Group α ρ)\n{ℓ : Agda.Primitive.Level}\n(θ φ\n : Setoid.Congruences.Basic.Con\n   (Classical.Structures.Group.Congruences.GroupCongruences.𝑮 𝒢) ℓ) →\nθ Setoid.Congruences.Lattice._.⊆ φ →\n(𝒢 Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ\n Classical.Structures.Group.Congruences.GroupCongruences.normalOf 𝒢\n θ)\n(Classical.Structures.Group.Congruences.GroupCongruences.normalOf 𝒢\n φ)"},{"defKind":"function","hasBody":true,"module":"Classical.Structures.Group.Congruences.GroupCongruences","prettyQname":"Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ-isPartialOrder","type":"{α ρ : Agda.Primitive.Level}\n(𝒢 : Classical.Structures.Group.Basic.Group α ρ)\n{ℓ : Agda.Primitive.Level} →\nRelation.Binary.Structures.IsPartialOrder\n(Classical.Structures.Group.Congruences.GroupCongruences._≈ⁿ_ 𝒢)\n(Classical.Structures.Group.Congruences.GroupCongruences._≤ⁿ_ 𝒢)"},{"defKind":"function","hasBody":true,"module":"Classical.Structures.Group.Congruences.GroupCongruences","prettyQname":"Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ-refl","type":"{α ρ : Agda.Primitive.Level}\n(𝒢 : Classical.Structures.Group.Basic.Group α ρ)\n{ℓ : Agda.Primitive.Level}\n{𝑵\n : Classical.Structures.Group.Congruences.GroupCongruences.NormalSubgroup\n   𝒢 ℓ} →\n(𝒢 Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ 𝑵) 𝑵"},{"defKind":"function","hasBody":true,"module":"Classical.Structures.Group.Congruences.GroupCongruences","prettyQname":"Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ-trans","type":"{α ρ : Agda.Primitive.Level}\n(𝒢 : Classical.Structures.Group.Basic.Group α ρ)\n{ℓ : Agda.Primitive.Level}\n{𝑳 𝑴 𝑵\n : Classical.Structures.Group.Congruences.GroupCongruences.NormalSubgroup\n   𝒢 ℓ} →\n(𝒢 Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ 𝑳)\n𝑴 →\n(𝒢 Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ 𝑴)\n𝑵 →\n(𝒢 Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ 𝑳) 𝑵"},{"defKind":"function","hasBody":true,"module":"Classical.Structures.Group.MinimalNormalDescent.MinimalNormalDescent","prettyQname":"Classical.Structures.Group.MinimalNormalDescent.MinimalNormalDescent.∥∥-mono","type":"{α ρ : Agda.Primitive.Level}\n(𝒢 : Classical.Structures.Group.Basic.Group α ρ)\n(𝑭\n : Setoid.Algebras.Finite.FiniteAlgebra\n   (Agda.Builtin.Sigma.Σ.fst 𝒢))\n(𝑴 𝑵\n : Classical.Structures.Group.MinimalNormalDescent.MinimalNormalDescent.Normalᵈ\n   𝒢 𝑭) →\nClassical.Structures.Group.MinimalNormalDescent.MinimalNormalDescent.setᵈ\n𝒢 𝑭 𝑴\nRelation.Unary.⊆\nClassical.Structures.Group.MinimalNormalDescent.MinimalNormalDescent.setᵈ\n𝒢 𝑭 𝑵 →\nClassical.Structures.Group.MinimalNormalDescent.MinimalNormalDescent.∥\n𝒢 ∥\n𝑭 𝑴\nData.Nat.Base.≤\nClassical.Structures.Group.MinimalNormalDescent.MinimalNormalDescent.∥\n𝒢 ∥\n𝑭 𝑵"},{"defKind":"function","hasBody":true,"module":"Classical.Structures.Group.NormalClosure.NormalClosureᵈ","prettyQname":"Classical.Structures.Group.NormalClosure.NormalClosureᵈ.⟪⟫-least","type":"{α ρ : Agda.Primitive.Level}\n(𝒢 : Classical.Structures.Group.Basic.Group α ρ)\n(𝑭\n : Setoid.Algebras.Finite.FiniteAlgebra\n   (Agda.Builtin.Sigma.Σ.fst 𝒢))\n(y : Classical.Structures.Group.NormalClosure.NormalClosureᵈ.G 𝒢 𝑭)\n(𝑵\n : Classical.Structures.Group.Congruences.GroupCongruences.NormalSubgroup\n   𝒢\n   (Classical.Structures.Group.NormalClosure.NormalClosureᵈ.L 𝒢 𝑭)) →\ny Relation.Unary.∈\nClassical.Structures.Group.Congruences.GroupCongruences.set 𝒢 𝑵 →\n(𝒢 Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ\n Classical.Structures.Group.NormalClosure.NormalClosureᵈ.⟪ 𝒢 ⟫ 𝑭 y)\n𝑵"},{"defKind":"function","hasBody":true,"module":"Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice","prettyQname":"Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.Nrm-isBoundedLattice","type":"{α ρ : Agda.Primitive.Level}\n(𝒢 : Classical.Structures.Group.Basic.Group α ρ)\n(ℓ₀ : Agda.Primitive.Level) →\nRelation.Binary.Lattice.Structures.IsBoundedLattice\n(Classical.Structures.Group.Congruences.GroupCongruences._≈ⁿ_ 𝒢)\n(Classical.Structures.Group.Congruences.GroupCongruences._≤ⁿ_ 𝒢)\n(𝒢\n Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.∨ⁿ\n ℓ₀)\n(𝒢\n Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.∩ⁿ\n ℓ₀)\n(Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.𝟙ⁿ\n 𝒢 ℓ₀)\n(Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.𝟘ⁿ\n 𝒢 ℓ₀)"},{"defKind":"function","hasBody":true,"module":"Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice","prettyQname":"Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.Nrm-isLattice","type":"{α ρ : Agda.Primitive.Level}\n(𝒢 : Classical.Structures.Group.Basic.Group α ρ)\n(ℓ₀ : Agda.Primitive.Level) →\nRelation.Binary.Lattice.Structures.IsLattice\n(Classical.Structures.Group.Congruences.GroupCongruences._≈ⁿ_ 𝒢)\n(Classical.Structures.Group.Congruences.GroupCongruences._≤ⁿ_ 𝒢)\n(𝒢\n Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.∨ⁿ\n ℓ₀)\n(𝒢\n Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.∩ⁿ\n ℓ₀)"},{"defKind":"function","hasBody":true,"module":"Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice","prettyQname":"Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.least","type":"{α ρ : Agda.Primitive.Level}\n(𝒢 : Classical.Structures.Group.Basic.Group α ρ)\n(ℓ₀ : Agda.Primitive.Level)\n(𝑴 𝑵\n : Classical.Structures.Group.Congruences.GroupCongruences.NormalSubgroup\n   𝒢\n   (Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.L\n    𝒢 ℓ₀))\n(𝑷\n : Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.Nrmᴸ\n   𝒢 ℓ₀) →\n(𝒢 Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ 𝑴)\n𝑷 →\n(𝒢 Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ 𝑵)\n𝑷 →\n(𝒢 Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ\n (𝒢\n  Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.∨ⁿ\n  ℓ₀)\n 𝑴 𝑵)\n𝑷"},{"defKind":"function","hasBody":true,"module":"Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice","prettyQname":"Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.upperʳ","type":"{α ρ : Agda.Primitive.Level}\n(𝒢 : Classical.Structures.Group.Basic.Group α ρ)\n(ℓ₀ : Agda.Primitive.Level)\n(𝑴 𝑵\n : Classical.Structures.Group.Congruences.GroupCongruences.NormalSubgroup\n   𝒢\n   (Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.L\n    𝒢 ℓ₀)) →\n(𝒢 Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ 𝑵)\n((𝒢\n  Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.∨ⁿ\n  ℓ₀)\n 𝑴 𝑵)"},{"defKind":"function","hasBody":true,"module":"Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice","prettyQname":"Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.upperˡ","type":"{α ρ : Agda.Primitive.Level}\n(𝒢 : Classical.Structures.Group.Basic.Group α ρ)\n(ℓ₀ : Agda.Primitive.Level)\n(𝑴 𝑵\n : Classical.Structures.Group.Congruences.GroupCongruences.NormalSubgroup\n   𝒢\n   (Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.L\n    𝒢 ℓ₀)) →\n(𝒢 Classical.Structures.Group.Congruences.GroupCongruences.≤ⁿ 𝑴)\n((𝒢\n  Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.∨ⁿ\n  ℓ₀)\n 𝑴 𝑵)"},{"defKind":"function","hasBody":true,"module":"Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice","prettyQname":"Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.∨ⁿ-supremum","type":"{α ρ : Agda.Primitive.Level}\n(𝒢 : Classical.Structures.Group.Basic.Group α ρ)\n(ℓ₀ : Agda.Primitive.Level) →\nRelation.Binary.Lattice.Definitions.Supremum\n(Classical.Structures.Group.Congruences.GroupCongruences._≤ⁿ_ 𝒢)\n(𝒢\n Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.∨ⁿ\n ℓ₀)"},{"defKind":"function","hasBody":true,"module":"Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice","prettyQname":"Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.∩ⁿ-infimum","type":"{α ρ : Agda.Primitive.Level}\n(𝒢 : Classical.Structures.Group.Basic.Group α ρ)\n(ℓ₀ : Agda.Primitive.Level) →\nRelation.Binary.Lattice.Definitions.Infimum\n(Classical.Structures.Group.Congruences.GroupCongruences._≤ⁿ_ 𝒢)\n(𝒢\n Classical.Structures.Group.NormalSubgroupLattice.NormalSubgroupLattice.∩ⁿ\n ℓ₀)"}]

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

agda-mcp

definition_of(name: Setoid.Subalgebras.Properties.≤-trans-≅)

answered5.8 s (loading the file first)

elapsedMs: 5849definitions: 11

the whole answer, as the model saw it (5,760 characters of JSON)

{"checkedFromSource":true,"command":{"args":["--interaction-json"],"binary":"agda","cwd":"<repo>"},"definitions":[{"col":1,"endCol":8,"endLine":140,"file":"<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md","line":140,"qualified":"Setoid.Homomorphisms.Isomorphisms.≅-trans"},{"col":3,"endCol":12,"endLine":85,"file":"<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md","line":85,"qualified":"Setoid.Subalgebras.Properties._.≅-trans-≤"},{"col":3,"endCol":10,"endLine":78,"file":"<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md","line":78,"qualified":"Setoid.Subalgebras.Properties._.≤-trans"},{"col":3,"endCol":12,"endLine":81,"file":"<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md","line":81,"qualified":"Setoid.Subalgebras.Properties._.≤-trans-≅"},{"col":3,"endCol":10,"endLine":90,"file":"<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md","line":90,"qualified":"Setoid.Subalgebras.Properties._.≥-trans"},{"col":1,"endCol":8,"endLine":140,"file":"<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md","line":140,"qualified":"Setoid.Homomorphisms.Isomorphisms.≅-trans"},{"col":3,"endCol":12,"endLine":85,"file":"<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md","line":85,"qualified":"Setoid.Subalgebras.Properties._.≅-trans-≤"},{"col":3,"endCol":10,"endLine":78,"file":"<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md","line":78,"qualified":"Setoid.Subalgebras.Properties._.≤-trans"},{"col":3,"endCol":12,"endLine":81,"file":"<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md","line":81,"qualified":"Setoid.Subalgebras.Properties._.≤-trans-≅"},{"col":1,"endCol":11,"endLine":24,"file":"<work>/Subalgebras-sub-trans-iso.agda","line":24,"qualified":"Subalgebras-sub-trans-iso.≤-trans-≅′"},{"col":3,"endCol":10,"endLine":90,"file":"<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md","line":90,"qualified":"Setoid.Subalgebras.Properties._.≥-trans"}],"elapsedMs":5849,"lane":{"agdaVersion":"2.8.0","iotcm":["IOTCM \"<work>\" None Direct (Cmd_show_version)","IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_load \"<work>/Subalgebras-sub-trans-iso.agda\" [\"-i\",\"agda-dojang/agda\",\"--library-file=agda/libraries\",\"-l\",\"agda-dojang\",\"-l\",\"standard-library\",\"-l\",\"agda-algebras\",\"--safe\",\"-i\",\"<work>\"])","IOTCM \"<work>\" None Direct (Cmd_show_version)","IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_why_in_scope_toplevel \"Setoid.Subalgebras.Properties.\\8804-trans-\\8773\")","IOTCM \"<work>\" None Direct (Cmd_show_version)","IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_infer_toplevel Normalised \"Setoid.Subalgebras.Properties.\\8804-trans-\\8773\")","IOTCM \"<work>\" None Direct (Cmd_show_version)","IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_why_in_scope_toplevel \"Setoid.Homomorphisms.\\8773-trans\")","IOTCM \"<work>\" None Direct (Cmd_show_version)","IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_why_in_scope_toplevel \"Setoid.Subalgebras.\\8773-trans-\\8804\")","IOTCM \"<work>\" None Direct (Cmd_show_version)","IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_why_in_scope_toplevel \"Setoid.Subalgebras.\\8804-trans\")","IOTCM \"<work>\" None Direct (Cmd_show_version)","IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_why_in_scope_toplevel \"Setoid.Subalgebras.\\8804-trans-\\8773\")","IOTCM \"<work>\" None Direct (Cmd_show_version)","IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_why_in_scope_toplevel \"Setoid.Subalgebras.\\8805-trans\")","IOTCM \"<work>\" None Direct (Cmd_show_version)","IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_why_in_scope_toplevel \"\\8773-trans\")","IOTCM \"<work>\" None Direct (Cmd_show_version)","IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_why_in_scope_toplevel \"\\8773-trans-\\8804\")","IOTCM \"<work>\" None Direct (Cmd_show_version)","IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_why_in_scope_toplevel \"\\8804-trans\")","IOTCM \"<work>\" None Direct (Cmd_show_version)","IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_why_in_scope_toplevel \"\\8804-trans-\\8773\")","IOTCM \"<work>\" None Direct (Cmd_show_version)","IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_why_in_scope_toplevel \"\\8804-trans-\\8773\\8242\")","IOTCM \"<work>\" None Direct (Cmd_show_version)","IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_why_in_scope_toplevel \"\\8805-trans\")","IOTCM \"<work>\" None Direct (Cmd_show_version)"],"load":"first","loadElapsedMs":5806,"pid":1368034,"root":"<work>","spawned":true},"name":"Setoid.Subalgebras.Properties.≤-trans-≅","project":{"includePaths":["agda-dojang/agda","<work>"],"librariesFile":"<repo>/agda/libraries","registeredLibraries":[{"includes":["agda"],"libFile":"<repo>/agda-dojang/agda-dojang.agda-lib","name":"agda-dojang","root":"<repo>/agda-dojang"},{"includes":["src"],"libFile":"<nix>/standard-library-2.3/standard-library.agda-lib","name":"standard-library-2.3","root":"<nix>/standard-library-2.3"},{"includes":["src"],"libFile":"<nix>/agda-algebras-unstable-2026-09-07/agda-algebras.agda-lib","name":"agda-algebras","root":"<nix>/agda-algebras-unstable-2026-09-07"}],"root":"<work>","rootSource":"server-config","selectedLibraries":["agda-dojang","standard-library","agda-algebras"]},"recovered":"did-you-mean","scope":"toplevel","unlocated":[]}

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

files

Read(file_path: <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md, offset: 1, limit: 95)

answered

1 ---

the whole answer, as the model saw it (4,347 characters of text)

1   ---
2   layout: default
3   title : "Setoid.Subalgebras.Properties module (The Agda Universal Algebra Library)"
4   date : "2021-07-18"
5   author: "agda-algebras development team"
6   ---
7   
8   #### Properties of the subalgebra relation for setoid algebras
9   
10  This is the [Setoid.Subalgebras.Properties][] module of the [Agda Universal Algebra Library][].
11  
12  This module establishes the order-theoretic facts about the subalgebra relation
13  `_≤_`{.AgdaFunction} that the rest of the library relies on: that it is a
14  preorder, that isomorphism refines it in either direction, that it survives
15  universe lifting, and that it is preserved by products.
16  
17  The preorder is stated with respect to isomorphism rather than equality
18  (`≤-preorder`{.AgdaFunction}), which is the only sensible choice, since mutual
19  embeddings do not make two algebras equal.  The universe-lifting group is the
20  part used most often, for the reason recorded in [Setoid.Algebras.Basic][]:
21  Agda's universes are not cumulative, so a `≤` established at one level has to be
22  transported explicitly before it can be used at another.
23  
24  <!--
25  ```agda
26  {-# OPTIONS --cubical-compatible --exact-split --safe #-}
27  
28  module Setoid.Subalgebras.Properties where
29  
30  open import Agda.Primitive using () renaming ( Set to Type )
31  
32  -- Imports from the Agda Standard Library -------------------------------------------
33  open import Data.Product              using ( _,_ )
34  open import Function                  using ( _∘_ )  renaming ( Func to _⟶_ )
35  open import Level                     using ( Level ; _⊔_ )
36  open import Relation.Binary           using ( Setoid )
37  open import Relation.Unary            using ( Pred ; _⊆_ )
38  import Relation.Binary.Structures as RelStructs
39  
40  import Relation.Binary.Reasoning.Setoid as SetoidReasoning
41  
42  -- Imports from the Agda Universal Algebra Library ----------------------------------
43  open import Overture                  using  ( proj₁ ; proj₂ ; 𝓞 ; 𝓥 ; Signature ; 𝑆 )
44  open import Setoid.Algebras           using  ( Algebra ; Lift-Algˡ ; Lift-Algʳ
45                                               ; Lift-Alg ; ov ; ⨅ ; 𝔻[_] )
46  open import Setoid.Functions          using  ( id-is-injective ; IsInjective ; ⊙-injective )
47  open import Setoid.Homomorphisms      using  ( hom ; IsHom ; 𝒾𝒹 ; ⊙-hom ; _≅_
48                                               ; ≅toInjective ; ≅fromInjective ; mkiso
49                                               ; ≅-sym ; ≅-refl ; ≅-trans
50                                               ; Lift-≅ˡ ; Lift-≅ ; Lift-≅ʳ)
51  open import Setoid.Subalgebras.Basic  using  ( _≤_ ; _≥_ ; _≤c_ )
52  
53  private variable α ρᵃ β ρᵇ γ ρᶜ ι : Level
54  ```
55  -->
56  
57  The subalgebra relation is a *preorder*, i.e., a reflexive, transitive binary relation.
58  
59  ```agda
60  open _≅_
61  
62  ≅→≤ : {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ} → 𝑨 ≅ 𝑩 → 𝑨 ≤ 𝑩
63  ≅→≤ φ = (to φ) , ≅toInjective φ
64  
65  ≅→≥ : {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ} → 𝑨 ≅ 𝑩 → 𝑨 ≥ 𝑩
66  ≅→≥ φ = (from φ) , ≅fromInjective φ
67  
68  ≤-refl : {𝑨 𝑩 : Algebra {𝑆 = 𝑆} α ρᵃ} → 𝑨 ≅ 𝑩 → 𝑨 ≤ 𝑩
69  ≤-refl = ≅→≤
70  
71  ≥-refl : {𝑨 𝑩 : Algebra {𝑆 = 𝑆} α ρᵃ} → 𝑨 ≅ 𝑩 → 𝑨 ≥ 𝑩
72  ≥-refl = ≅→≤ ∘ ≅-sym
73  
74  ≤-reflexive : {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} → 𝑨 ≤ 𝑨
75  ≤-reflexive {𝑨 = 𝑨} = 𝒾𝒹 , id-is-injective {𝑨 = 𝔻[ 𝑨 ]}
76  
77  module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ}{𝑪 : Algebra {𝑆 = 𝑆} γ ρᶜ} where
78    ≤-trans : 𝑨 ≤ 𝑩 → 𝑩 ≤ 𝑪 → 𝑨 ≤ 𝑪
79    ≤-trans ( f , finj ) ( g , ginj ) = (⊙-hom f g) , ⊙-injective (proj₁ f) (proj₁ g) finj ginj
80  
81    ≤-trans-≅ : 𝑨 ≤ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≤ 𝑪
82    ≤-trans-≅ (h , hinj) B≅C =
83      ⊙-hom h (to B≅C) , ⊙-injective (proj₁ h) (proj₁ (to B≅C)) hinj (≅toInjective B≅C)
84  
85    ≅-trans-≤ : 𝑨 ≅ 𝑩 → 𝑩 ≤ 𝑪 → 𝑨 ≤ 𝑪
86    ≅-trans-≤ A≅B (h , hinj) =
87      ⊙-hom (to A≅B) h , ⊙-injective (proj₁ (to A≅B)) (proj₁ h) (≅toInjective A≅B) hinj
88  
89  module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ}{𝑪 : Algebra {𝑆 = 𝑆} γ ρᶜ} where
90    ≥-trans : 𝑨 ≥ 𝑩 → 𝑩 ≥ 𝑪 → 𝑨 ≥ 𝑪
91    ≥-trans A≥B B≥C = ≤-trans B≥C A≥B
92  
93  ≤→≤c→≤c : {𝑨 : Algebra {𝑆 = 𝑆} α α}{𝑩 : Algebra {𝑆 = 𝑆} α α}{𝒦 : Pred(Algebra {𝑆 = 𝑆} α α) (ov {𝑆 = 𝑆} α)}
94    → 𝑨 ≤ 𝑩 → 𝑩 ≤c 𝒦 → 𝑨 ≤c 𝒦
95  ≤→≤c→≤c A≤B sB = (proj₁ sB) , (proj₁ (proj₂ sB) , ≤-trans A≤B (proj₂ (proj₂ sB)))

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

agda-mcp

exports_of(module: Setoid.Homomorphisms)

answered56 ms (the file already loaded)

elapsedMs: 56exports: 91modules: 4

the whole answer, as the model saw it (25,119 characters of JSON)

{"checkedFromSource":false,"command":{"args":["--interaction-json"],"binary":"agda","cwd":"<repo>"},"elapsedMs":56,"exports":[{"name":"_IsHomImageOf_","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {β ρᵇ α ρᵃ : Level}\n(𝑩 : Algebra β ρᵇ) (𝑨 : Algebra α ρᵃ) →\nSet\n(𝑆.𝓞 Agda.Primitive.⊔ 𝑆.𝓥 Agda.Primitive.⊔ β Agda.Primitive.⊔ ρᵇ\n Agda.Primitive.⊔ α\n Agda.Primitive.⊔ ρᵃ)"},{"name":"_≅_","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra α ρᵃ)\n(𝑩 : Algebra β ρᵇ) →\nSet\n(𝓞 Agda.Primitive.⊔ 𝓥 Agda.Primitive.⊔ α Agda.Primitive.⊔ ρᵃ\n Agda.Primitive.⊔ β\n Agda.Primitive.⊔ ρᵇ)"},{"name":"Bijective→≅","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} (h : hom 𝑨 𝑩) →\nIsInjective (proj₁ h) → IsSurjective (proj₁ h) → 𝑨 ≅ 𝑩"},{"name":"Cg⊆ker","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥}\n{α ρᵃ β ρᵇ : Level} {ℓ = ℓ₁ : Level} {𝑨 : Algebra α ρᵃ}\n{𝑩 : Algebra β ρᵇ} (h : hom 𝑨 𝑩)\n{R : Relation.Binary.Core.Rel Setoid.Algebras.𝕌[ 𝑨 ] ℓ₁} →\nR Relation.Binary.Core.⇒ proj₁ (kercon h) →\nSetoid.Congruences.Generation.Gen R Relation.Binary.Core.⇒\nproj₁ (kercon h)"},{"name":"FirstHomTheorem","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρᵃ}\n{𝑩 : Algebra β ρᵇ} (hh : hom 𝑨 𝑩) →\nSetoid.Algebras.Σ-syntax (hom (kerquo hh) 𝑩)\n(λ .patternInTele0 →\n   ((a : Relation.Binary.Bundles.Setoid.Carrier (Algebra.Domain 𝑨)) →\n    (Setoid.Algebras.𝔻[ 𝑩 ] Relation.Binary.Bundles.Setoid.≈\n     Setoid.Homomorphisms.Noether.h hh a)\n    (Function.Bundles.Func.to (.patternInTele0 .proj₁)\n     (Function.Bundles.Func.to (πker hh .proj₁) a)))\n   Data.Product.× IsInjective (.patternInTele0 .proj₁))"},{"name":"FirstHomUnique","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρᵃ}\n{𝑩 : Algebra β ρᵇ} (hh : hom 𝑨 𝑩)\n{.patternInTele0 .patternInTele1 : hom (kerquo hh) 𝑩} →\n((a : Relation.Binary.Bundles.Setoid.Carrier (Algebra.Domain 𝑨)) →\n (Setoid.Algebras.𝔻[ 𝑩 ] Relation.Binary.Bundles.Setoid.≈\n  Setoid.Homomorphisms.Noether.h hh a)\n (Function.Bundles.Func.to (.patternInTele0 .proj₁)\n  (Function.Bundles.Func.to (πker hh .proj₁) a))) →\n((a : Relation.Binary.Bundles.Setoid.Carrier (Algebra.Domain 𝑨)) →\n (Setoid.Algebras.𝔻[ 𝑩 ] Relation.Binary.Bundles.Setoid.≈\n  Setoid.Homomorphisms.Noether.h hh a)\n (Function.Bundles.Func.to (.patternInTele1 .proj₁)\n  (Function.Bundles.Func.to (πker hh .proj₁) a))) →\n([a]\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Algebra.Domain (kerquo hh))) →\n(Setoid.Algebras.𝔻[ 𝑩 ] Relation.Binary.Bundles.Setoid.≈\n Function.Bundles.Func.to (.patternInTele0 .proj₁) [a])\n(Function.Bundles.Func.to (.patternInTele1 .proj₁) [a])"},{"name":"FromLift","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level} {r : Level} →\nhom (Setoid.Algebras.Lift-Alg 𝑨 ℓ₁ r) 𝑨"},{"name":"FromLiftʳ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level} →\nhom (Setoid.Algebras.Lift-Algʳ 𝑨 ℓ₁) 𝑨"},{"name":"FromLiftˡ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level} →\nhom (Setoid.Algebras.Lift-Algˡ 𝑨 ℓ₁) 𝑨"},{"name":"FromToLiftʳ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level}\n(a : Relation.Binary.Bundles.Setoid.Carrier (Algebra.Domain 𝑨)) →\n(Setoid.Algebras.𝔻[ 𝑨 ] Relation.Binary.Bundles.Setoid.≈ a) a"},{"name":"FromToLiftˡ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level}\n(a : Relation.Binary.Bundles.Setoid.Carrier (Algebra.Domain 𝑨)) →\n(Setoid.Algebras.𝔻[ 𝑨 ] Relation.Binary.Bundles.Setoid.≈ a) a"},{"name":"HomFactor","type":"{𝓞 𝓥 α ρᵃ β ρᵇ γ ρᶜ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρᵃ}\n{𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ} (.patternInTele0 : hom 𝑨 𝑩)\n(.patternInTele1 : hom 𝑨 𝑪) →\nOverture.kernelRel\n(Relation.Binary.Bundles.Setoid._≈_ Setoid.Algebras.𝔻[ 𝑪 ])\n(Setoid.Homomorphisms.Factor.h .patternInTele0 .patternInTele1)\nRelation.Unary.⊆\nOverture.kernelRel\n(Relation.Binary.Bundles.Setoid._≈_ Setoid.Algebras.𝔻[ 𝑩 ])\n(Setoid.Homomorphisms.Factor.g .patternInTele0 .patternInTele1) →\nIsSurjective (.patternInTele1 .proj₁) →\nSetoid.Algebras.Σ-syntax (hom 𝑪 𝑩)\n(λ .patternInTele2 →\n   (a : Relation.Binary.Bundles.Setoid.Carrier (Algebra.Domain 𝑨)) →\n   (Setoid.Algebras.𝔻[ 𝑩 ] Relation.Binary.Bundles.Setoid.≈\n    Setoid.Homomorphisms.Factor.g .patternInTele0 .patternInTele1 a)\n   (Function.Bundles.Func.to (.patternInTele2 .proj₁)\n    (Setoid.Homomorphisms.Factor.h .patternInTele0 .patternInTele1 a)))"},{"name":"HomFactorEpi","type":"{𝓞 𝓥 α ρᵃ β ρᵇ γ ρᶜ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρᵃ}\n{𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ} (.patternInTele0 : hom 𝑨 𝑩)\n(.patternInTele1 : hom 𝑨 𝑪) →\nOverture.kernelRel\n(Relation.Binary.Bundles.Setoid._≈_ Setoid.Algebras.𝔻[ 𝑪 ])\n(Setoid.Homomorphisms.Factor.h .patternInTele0 .patternInTele1)\nRelation.Unary.⊆\nOverture.kernelRel\n(Relation.Binary.Bundles.Setoid._≈_ Setoid.Algebras.𝔻[ 𝑩 ])\n(Setoid.Homomorphisms.Factor.g .patternInTele0 .patternInTele1) →\nIsSurjective (.patternInTele1 .proj₁) →\nIsSurjective (.patternInTele0 .proj₁) →\nSetoid.Algebras.Σ-syntax (epi 𝑪 𝑩)\n(λ .patternInTele2 →\n   (a : Relation.Binary.Bundles.Setoid.Carrier (Algebra.Domain 𝑨)) →\n   (Setoid.Algebras.𝔻[ 𝑩 ] Relation.Binary.Bundles.Setoid.≈\n    Setoid.Homomorphisms.Factor.g .patternInTele0 .patternInTele1 a)\n   (Function.Bundles.Func.to (.patternInTele2 .proj₁)\n    (Setoid.Homomorphisms.Factor.h .patternInTele0 .patternInTele1 a)))"},{"name":"HomImage-≅","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 𝑨' : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} →\n𝑨 IsHomImageOf 𝑨' → 𝑨 ≅ 𝑩 → 𝑩 IsHomImageOf 𝑨'"},{"name":"HomImage-≅'","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 𝑨' : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} →\n𝑨 IsHomImageOf 𝑨' → 𝑨' ≅ 𝑩 → 𝑨 IsHomImageOf 𝑩"},{"name":"HomImageOfClass","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level} →\nRelation.Unary.Pred (Algebra α ρᵃ) (Agda.Primitive.lsuc α) →\nSet\n(𝑆.𝓞 Agda.Primitive.⊔ 𝑆.𝓥 Agda.Primitive.⊔ Agda.Primitive.lsuc α\n Agda.Primitive.⊔ Agda.Primitive.lsuc ρᵃ)"},{"name":"HomImageOf[_]","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} →\nhom 𝑨 𝑩 → Algebra (α Agda.Primitive.⊔ β Agda.Primitive.⊔ ρᵇ) ρᵇ"},{"name":"HomImages","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level} →\nAlgebra α ρᵃ →\nSet\n(𝑆.𝓞 Agda.Primitive.⊔ 𝑆.𝓥 Agda.Primitive.⊔ α Agda.Primitive.⊔ ρᵃ\n Agda.Primitive.⊔ Agda.Primitive.lsuc β\n Agda.Primitive.⊔ Agda.Primitive.lsuc ρᵇ)"},{"name":"HomKerComp","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρᵃ}\n{𝑩 : Algebra β ρᵇ} (.patternInTele0 : hom 𝑨 𝑩) →\n𝑨 Setoid.Congruences.Basic.∣≈\nOverture.kerRel\n(Relation.Binary.Bundles.Setoid._≈_ (Algebra.Domain 𝑩))\n(Setoid.Homomorphisms.Kernels.h .patternInTele0)"},{"name":"IdHomImage","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} →\n𝑨 IsHomImageOf 𝑨"},{"name":"IsEpi","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra α ρᵃ)\n(𝑩 : Algebra β ρᵇ)\n(h\n : Function.Bundles.Func Setoid.Algebras.𝔻[ 𝑨 ]\n   Setoid.Algebras.𝔻[ 𝑩 ]) →\nSet\n(𝓞 Agda.Primitive.⊔ 𝓥 Agda.Primitive.⊔ α Agda.Primitive.⊔ ρᵃ\n Agda.Primitive.⊔ β\n Agda.Primitive.⊔ ρᵇ)"},{"name":"IsHom","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra α ρᵃ)\n(𝑩 : Algebra β ρᵇ)\n(h\n : Function.Bundles.Func Setoid.Algebras.𝔻[ 𝑨 ]\n   Setoid.Algebras.𝔻[ 𝑩 ]) →\nSet\n(𝓞 Agda.Primitive.⊔ 𝓥 Agda.Primitive.⊔ α Agda.Primitive.⊔ ρᵃ\n Agda.Primitive.⊔ ρᵇ)"},{"name":"IsHomImageOfClass","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝒦 : Relation.Unary.Pred (Algebra α ρᵃ) (Agda.Primitive.lsuc α)} →\nAlgebra α ρᵃ →\nSet\n(𝑆.𝓞 Agda.Primitive.⊔ 𝑆.𝓥 Agda.Primitive.⊔ Agda.Primitive.lsuc α\n Agda.Primitive.⊔ Agda.Primitive.lsuc ρᵃ)"},{"name":"IsMon","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra α ρᵃ)\n(𝑩 : Algebra β ρᵇ)\n(h\n : Function.Bundles.Func Setoid.Algebras.𝔻[ 𝑨 ]\n   Setoid.Algebras.𝔻[ 𝑩 ]) →\nSet\n(𝓞 Agda.Primitive.⊔ 𝓥 Agda.Primitive.⊔ α Agda.Primitive.⊔ ρᵃ\n Agda.Primitive.⊔ β\n Agda.Primitive.⊔ ρᵇ)"},{"name":"Lift-Alg-hom-imageˡ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} (ℓᵃ ℓᵇ : Level) →\n𝑩 IsHomImageOf 𝑨 →\nSetoid.Algebras.Lift-Algˡ 𝑩 ℓᵇ IsHomImageOf\nSetoid.Algebras.Lift-Algˡ 𝑨 ℓᵃ"},{"name":"Lift-Alg-iso","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} {ℓᵃ rᵃ ℓᵇ rᵇ : Level} →\n𝑨 ≅ 𝑩 →\nSetoid.Algebras.Lift-Alg 𝑨 ℓᵃ rᵃ ≅ Setoid.Algebras.Lift-Alg 𝑩 ℓᵇ rᵇ"},{"name":"Lift-Alg-isoʳ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} {ℓᵃ ℓᵇ : Level} →\n𝑨 ≅ 𝑩 →\nSetoid.Algebras.Lift-Algʳ 𝑨 ℓᵃ ≅ Setoid.Algebras.Lift-Algʳ 𝑩 ℓᵇ"},{"name":"Lift-Alg-isoˡ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} {ℓᵃ ℓᵇ : Level} →\n𝑨 ≅ 𝑩 →\nSetoid.Algebras.Lift-Algˡ 𝑨 ℓᵃ ≅ Setoid.Algebras.Lift-Algˡ 𝑩 ℓᵇ"},{"name":"Lift-Alg-⨅≅ˡ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥}\n{α ρᵃ γ β ρᵇ : Level} {𝓘 : Level} {I : Set 𝓘}\n{𝒜 : I → Algebra α ρᵃ} {ℬ : Level.Lift γ I → Algebra β ρᵇ} →\n((i : I) → 𝒜 i ≅ ℬ (Level.lift i)) →\nSetoid.Algebras.Lift-Algˡ (Setoid.Algebras.⨅ 𝒜) γ ≅\nSetoid.Algebras.⨅ ℬ"},{"name":"Lift-HomImage-lemma","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} {γ : Level} →\nSetoid.Algebras.Lift-Alg 𝑨 γ γ IsHomImageOf 𝑩 → 𝑨 IsHomImageOf 𝑩"},{"name":"Lift-assoc","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level} {ρ : Level} →\nSetoid.Algebras.Lift-Alg 𝑨 ℓ₁ ρ ≅\nSetoid.Algebras.Lift-Algʳ (Setoid.Algebras.Lift-Algˡ 𝑨 ℓ₁) ρ"},{"name":"Lift-assoc'","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α : Level}\n{𝑨 : Algebra α α} {β γ : Level} →\nSetoid.Algebras.Lift-Alg 𝑨 (β Agda.Primitive.⊔ γ)\n(β Agda.Primitive.⊔ γ)\n≅ Setoid.Algebras.Lift-Alg (Setoid.Algebras.Lift-Alg 𝑨 β β) γ γ"},{"name":"Lift-assocʳ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ₁ ℓ₂ : Level} →\nSetoid.Algebras.Lift-Algʳ 𝑨 (ℓ₁ Agda.Primitive.⊔ ℓ₂) ≅\nSetoid.Algebras.Lift-Algʳ (Setoid.Algebras.Lift-Algʳ 𝑨 ℓ₁) ℓ₂"},{"name":"Lift-assocˡ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ₁ ℓ₂ : Level} →\nSetoid.Algebras.Lift-Algˡ 𝑨 (ℓ₁ Agda.Primitive.⊔ ℓ₂) ≅\nSetoid.Algebras.Lift-Algˡ (Setoid.Algebras.Lift-Algˡ 𝑨 ℓ₁) ℓ₂"},{"name":"Lift-epi-is-epiˡ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} (h : hom 𝑨 𝑩)\n(ℓᵃ ℓᵇ : Level) →\nIsSurjective (proj₁ h) → IsSurjective (proj₁ (Lift-homˡ h ℓᵃ ℓᵇ))"},{"name":"Lift-hom","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} →\nhom 𝑨 𝑩 →\n(ℓᵃ rᵃ ℓᵇ rᵇ : Level) →\nhom (Setoid.Algebras.Lift-Alg 𝑨 ℓᵃ rᵃ)\n(Setoid.Algebras.Lift-Alg 𝑩 ℓᵇ rᵇ)"},{"name":"Lift-hom-fst","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} →\nhom 𝑨 𝑩 → (ℓ₁ r : Level) → hom (Setoid.Algebras.Lift-Alg 𝑨 ℓ₁ r) 𝑩"},{"name":"Lift-hom-snd","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} →\nhom 𝑨 𝑩 → (ℓ₁ r : Level) → hom 𝑨 (Setoid.Algebras.Lift-Alg 𝑩 ℓ₁ r)"},{"name":"Lift-homʳ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} →\nhom 𝑨 𝑩 →\n(rᵃ rᵇ : Level) →\nhom (Setoid.Algebras.Lift-Algʳ 𝑨 rᵃ)\n(Setoid.Algebras.Lift-Algʳ 𝑩 rᵇ)"},{"name":"Lift-homˡ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} →\nhom 𝑨 𝑩 →\n(ℓᵃ ℓᵇ : Level) →\nhom (Setoid.Algebras.Lift-Algˡ 𝑨 ℓᵃ)\n(Setoid.Algebras.Lift-Algˡ 𝑩 ℓᵇ)"},{"name":"Lift-≅","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level} {ρ : Level} →\n𝑨 ≅ Setoid.Algebras.Lift-Alg 𝑨 ℓ₁ ρ"},{"name":"Lift-≅ʳ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level} →\n𝑨 ≅ Setoid.Algebras.Lift-Algʳ 𝑨 ℓ₁"},{"name":"Lift-≅ˡ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level} →\n𝑨 ≅ Setoid.Algebras.Lift-Algˡ 𝑨 ℓ₁"},{"name":"ToFromLift","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level} {r : Level}\n{b\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Algebra.Domain (Setoid.Algebras.Lift-Alg 𝑨 ℓ₁ r))} →\n(Setoid.Algebras.𝔻[ Setoid.Algebras.Lift-Alg 𝑨 ℓ₁ r ]\n Relation.Binary.Bundles.Setoid.≈\n Function.Bundles.Func.to (ToLift .proj₁)\n (Function.Bundles.Func.to (FromLift .proj₁) b))\nb"},{"name":"ToFromLiftʳ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level}\n(b\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Algebra.Domain (Setoid.Algebras.Lift-Algʳ 𝑨 ℓ₁))) →\n(Setoid.Algebras.𝔻[ Setoid.Algebras.Lift-Algʳ 𝑨 ℓ₁ ]\n Relation.Binary.Bundles.Setoid.≈ b)\nb"},{"name":"ToFromLiftˡ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level}\n(b\n : Relation.Binary.Bundles.Setoid.Carrier\n   (Algebra.Domain (Setoid.Algebras.Lift-Algˡ 𝑨 ℓ₁))) →\n(Setoid.Algebras.𝔻[ Setoid.Algebras.Lift-Algˡ 𝑨 ℓ₁ ]\n Relation.Binary.Bundles.Setoid.≈ Level.lift (Level.Lift.lower b))\nb"},{"name":"ToLift","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level} {r : Level} →\nhom 𝑨 (Setoid.Algebras.Lift-Alg 𝑨 ℓ₁ r)"},{"name":"ToLift-epi","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level} {r : Level} →\nepi 𝑨 (Setoid.Algebras.Lift-Alg 𝑨 ℓ₁ r)"},{"name":"ToLiftʳ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level} →\nhom 𝑨 (Setoid.Algebras.Lift-Algʳ 𝑨 ℓ₁)"},{"name":"ToLiftˡ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} {ℓ = ℓ₁ : Level} →\nhom 𝑨 (Setoid.Algebras.Lift-Algˡ 𝑨 ℓ₁)"},{"name":"compatible-map","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra α ρᵃ)\n(𝑩 : Algebra β ρᵇ) →\nFunction.Bundles.Func Setoid.Algebras.𝔻[ 𝑨 ]\nSetoid.Algebras.𝔻[ 𝑩 ] →\nSet (𝓞 Agda.Primitive.⊔ 𝓥 Agda.Primitive.⊔ α Agda.Primitive.⊔ ρᵇ)"},{"name":"compatible-map-op","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra α ρᵃ)\n(𝑩 : Algebra β ρᵇ) →\nFunction.Bundles.Func Setoid.Algebras.𝔻[ 𝑨 ]\nSetoid.Algebras.𝔻[ 𝑩 ] →\nOverture.OperationSymbolsOf 𝑆 →\nSet (𝓥 Agda.Primitive.⊔ α Agda.Primitive.⊔ ρᵇ)"},{"name":"epi","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra α ρᵃ) →\nAlgebra β ρᵇ →\nSet\n(𝓞 Agda.Primitive.⊔ 𝓥 Agda.Primitive.⊔ α Agda.Primitive.⊔ ρᵃ\n Agda.Primitive.⊔ β\n Agda.Primitive.⊔ ρᵇ)"},{"name":"epi→hom","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra α ρᵃ)\n(𝑩 : Algebra β ρᵇ) →\nepi 𝑨 𝑩 → hom 𝑨 𝑩"},{"name":"epi→ontohom","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra α ρᵃ)\n(𝑩 : Algebra β ρᵇ) →\nepi 𝑨 𝑩 →\nSetoid.Algebras.Σ-syntax (hom 𝑨 𝑩) (λ h → IsSurjective (proj₁ h))"},{"name":"hom","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra α ρᵃ) →\nAlgebra β ρᵇ →\nSet\n(𝓞 Agda.Primitive.⊔ 𝓥 Agda.Primitive.⊔ α Agda.Primitive.⊔ ρᵃ\n Agda.Primitive.⊔ β\n Agda.Primitive.⊔ ρᵇ)"},{"name":"ker-in-con","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρᵃ}\n{𝑩 : Algebra β ρᵇ} (h : hom 𝑨 𝑩) {ℓ = ℓ₁ : Level}\n{θ : Setoid.Congruences.Basic.Con 𝑨 ℓ₁}\n{x y : Relation.Binary.Bundles.Setoid.Carrier (Algebra.Domain 𝑨)} →\nkercon (πhom h θ) .proj₁ x y → θ .proj₁ x y"},{"name":"ker[_⇒_]_","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra α ρᵃ)\n(𝑩 : Algebra β ρᵇ) →\nhom 𝑨 𝑩 → Algebra α ρᵇ"},{"name":"kercon","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρᵃ}\n{𝑩 : Algebra β ρᵇ} (.patternInTele0 : hom 𝑨 𝑩) →\nSetoid.Congruences.Basic.Con 𝑨 ρᵇ"},{"name":"kerquo","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρᵃ}\n{𝑩 : Algebra β ρᵇ} (.patternInTele0 : hom 𝑨 𝑩) →\nAlgebra α ρᵇ"},{"name":"lift-hom-lemma","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} (h : hom 𝑨 𝑩)\n(a : Setoid.Algebras.𝕌[ 𝑨 ]) (ℓᵃ ℓᵇ : Level) →\n(Setoid.Algebras.𝔻[ Setoid.Algebras.Lift-Algˡ 𝑩 ℓᵇ ]\n Relation.Binary.Bundles.Setoid.≈\n Level.lift (Function.Bundles.Func.to (h .proj₁) a))\n(Function.Bundles.Func.to (Lift-homˡ h ℓᵃ ℓᵇ .proj₁)\n (Level.lift a))"},{"name":"mkIsHom","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρᵃ}\n{𝑩 : Algebra β ρᵇ}\n{h\n : Function.Bundles.Func Setoid.Algebras.𝔻[ 𝑨 ]\n   Setoid.Algebras.𝔻[ 𝑩 ]}\n(compatible : compatible-map 𝑨 𝑩 h) →\nIsHom 𝑨 𝑩 h"},{"name":"mkhom","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra α ρᵃ)\n(𝑩 : Algebra β ρᵇ)\n(h\n : Function.Bundles.Func Setoid.Algebras.𝔻[ 𝑨 ]\n   Setoid.Algebras.𝔻[ 𝑩 ]) →\ncompatible-map 𝑨 𝑩 h → hom 𝑨 𝑩"},{"name":"mkiso","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρᵃ}\n{𝑩 : Algebra β ρᵇ} (to : hom 𝑨 𝑩) (from : hom 𝑩 𝑨)\n(to∼from\n : (b : Relation.Binary.Bundles.Setoid.Carrier (Algebra.Domain 𝑩)) →\n   (Setoid.Algebras.𝔻[ 𝑩 ] Relation.Binary.Bundles.Setoid.≈\n    Function.Bundles.Func.to (to .proj₁)\n    (Function.Bundles.Func.to (from .proj₁) b))\n   b)\n(from∼to\n : (a : Relation.Binary.Bundles.Setoid.Carrier (Algebra.Domain 𝑨)) →\n   (Setoid.Algebras.𝔻[ 𝑨 ] Relation.Binary.Bundles.Setoid.≈\n    Function.Bundles.Func.to (from .proj₁)\n    (Function.Bundles.Func.to (to .proj₁) a))\n   a) →\n𝑨 ≅ 𝑩"},{"name":"mon","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra α ρᵃ) →\nAlgebra β ρᵇ →\nSet\n(𝓞 Agda.Primitive.⊔ 𝓥 Agda.Primitive.⊔ α Agda.Primitive.⊔ ρᵃ\n Agda.Primitive.⊔ β\n Agda.Primitive.⊔ ρᵇ)"},{"name":"mon→hom","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra α ρᵃ)\n(𝑩 : Algebra β ρᵇ) →\nmon 𝑨 𝑩 → hom 𝑨 𝑩"},{"name":"mon→intohom","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra α ρᵃ)\n(𝑩 : Algebra β ρᵇ) →\nmon 𝑨 𝑩 →\nSetoid.Algebras.Σ-syntax (hom 𝑨 𝑩) (λ h → IsInjective (proj₁ h))"},{"name":"πepi","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρᵃ}\n{𝑩 : Algebra β ρᵇ} →\nhom 𝑨 𝑩 →\n{ℓ = ℓ₁ : Level} (θ : Setoid.Congruences.Basic.Con 𝑨 ℓ₁) →\nepi 𝑨 (𝑨 Setoid.Congruences.Basic._.╱ θ)"},{"name":"πhom","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρᵃ}\n{𝑩 : Algebra β ρᵇ} →\nhom 𝑨 𝑩 →\n{ℓ = ℓ₁ : Level} (θ : Setoid.Congruences.Basic.Con 𝑨 ℓ₁) →\nhom 𝑨 (𝑨 Setoid.Congruences.Basic._.╱ θ)"},{"name":"πker","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρᵃ}\n{𝑩 : Algebra β ρᵇ} (h : hom 𝑨 𝑩) →\nepi 𝑨 (ker[ 𝑨 ⇒ 𝑩 ] h)"},{"name":"ℓ⨅≅⨅ℓ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥}\n{α ρᵃ : Level} {ℓᵃ : Level} {I : Set ℓᵃ} {𝒜 : I → Algebra α ρᵃ}\n{ℓ = ℓ₁ : Level} →\nSetoid.Algebras.Lift-Alg (Setoid.Algebras.⨅ 𝒜) ℓ₁ ℓ₁ ≅\nSetoid.Algebras.⨅\n(λ i → Setoid.Algebras.Lift-Alg (𝒜 (Level.Lift.lower i)) ℓ₁ ℓ₁)"},{"name":"≅-mkAlgebra","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ}\n(f\n : (o : Overture.OperationSymbolsOf 𝑆) →\n   Overture.Op (Overture.ArityOf 𝑆 o) Setoid.Algebras.𝕌[ 𝑨 ])\n(cong-f\n : (o : Overture.OperationSymbolsOf 𝑆)\n   {u v : Overture.ArityOf 𝑆 o → Setoid.Algebras.𝕌[ 𝑨 ]} →\n   ((i : Overture.ArityOf 𝑆 o) →\n    (Setoid.Algebras.𝔻[ 𝑨 ] Relation.Binary.Bundles.Setoid.≈ u i)\n    (v i)) →\n   (Setoid.Algebras.𝔻[ 𝑨 ] Relation.Binary.Bundles.Setoid.≈ f o u)\n   (f o v)) →\n((o : 𝑆 .proj₁)\n (a\n  : Overture.ArityOf 𝑆 o →\n    Relation.Binary.Bundles.Setoid.Carrier (Algebra.Domain 𝑨)) →\n (Setoid.Algebras.𝔻[ 𝑨 ] Relation.Binary.Bundles.Setoid.≈\n  (o Setoid.Algebras.^ 𝑨) a)\n (f o a)) →\n𝑨 ≅ Setoid.Algebras.mkAlgebra Setoid.Algebras.𝔻[ 𝑨 ] f cong-f"},{"name":"≅-refl","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} →\n𝑨 ≅ 𝑨"},{"name":"≅-sym","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} →\n𝑨 ≅ 𝑩 → 𝑩 ≅ 𝑨"},{"name":"≅-trans","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ γ ρᶜ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ} →\n𝑨 ≅ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≅ 𝑪"},{"name":"≅fromInjective","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} (φ : 𝑨 ≅ 𝑩) →\nIsInjective (_≅_.from φ .proj₁)"},{"name":"≅toInjective","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} (φ : 𝑨 ≅ 𝑩) →\nIsInjective (proj₁ (_≅_.to φ))"},{"name":"≅⨅-refl","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ : Level}\n{𝑨 : Algebra α ρᵃ} →\n𝑨 ≅ Setoid.Algebras.⨅ (λ i → 𝑨)"},{"name":"≅⨅⁺-refl","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥}\n{α ρᵃ : Level} {ι : Level} {𝑨 : Algebra α ρᵃ} →\n𝑨 ≅ Setoid.Algebras.⨅ (λ i → 𝑨)"},{"name":"⊙-epi","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ γ ρᶜ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ} →\nepi 𝑨 𝑩 → epi 𝑩 𝑪 → epi 𝑨 𝑪"},{"name":"⊙-hom","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ γ ρᶜ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ} →\nhom 𝑨 𝑩 → hom 𝑩 𝑪 → hom 𝑨 𝑪"},{"name":"⊙-is-epi","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ γ ρᶜ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ}\n{g\n : Function.Bundles.Func Setoid.Algebras.𝔻[ 𝑨 ]\n   Setoid.Algebras.𝔻[ 𝑩 ]}\n{h\n : Function.Bundles.Func Setoid.Algebras.𝔻[ 𝑩 ]\n   Setoid.Algebras.𝔻[ 𝑪 ]} →\nIsEpi 𝑨 𝑩 g → IsEpi 𝑩 𝑪 h → IsEpi 𝑨 𝑪 (h ⊙ g)"},{"name":"⊙-is-hom","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥} {α ρᵃ β ρᵇ γ ρᶜ : Level}\n{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ}\n{g\n : Function.Bundles.Func Setoid.Algebras.𝔻[ 𝑨 ]\n   Setoid.Algebras.𝔻[ 𝑩 ]}\n{h\n : Function.Bundles.Func Setoid.Algebras.𝔻[ 𝑩 ]\n   Setoid.Algebras.𝔻[ 𝑪 ]} →\nIsHom 𝑨 𝑩 g → IsHom 𝑩 𝑪 h → IsHom 𝑨 𝑪 (h ⊙ g)"},{"name":"⨅-hom","type":"{𝓞 𝓥 𝓘 α ρ : Level} {𝑆 : Signature 𝓞 𝓥} {I : Set 𝓘}\n(𝒜 : I → Algebra α ρ) {β ρᵇ : Level} (ℬ : I → Algebra β ρᵇ) →\n((i : I) → hom (𝒜 i) (ℬ i)) →\nhom (Setoid.Algebras.⨅ 𝒜) (Setoid.Algebras.⨅ ℬ)"},{"name":"⨅-hom-co","type":"{𝓞 𝓥 α ρ 𝓘 β ρᵇ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρ}\n{I : Set 𝓘} (ℬ : I → Algebra β ρᵇ) →\n((i : I) → hom 𝑨 (ℬ i)) → hom 𝑨 (Setoid.Algebras.⨅ ℬ)"},{"name":"⨅-proj","type":"{𝓞 𝓥 𝓘 α ρ : Level} {𝑆 : Signature 𝓞 𝓥} {I : Set 𝓘}\n(𝒜 : I → Algebra α ρ) (i : I) →\nhom (Setoid.Algebras.⨅ 𝒜) (𝒜 i)"},{"name":"⨅≅","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥}\n{α ρᵃ β ρᵇ : Level} {𝓘 : Level} {I : Set 𝓘} {𝒜 : I → Algebra α ρᵃ}\n{ℬ : I → Algebra β ρᵇ} →\n((i : I) → 𝒜 i ≅ ℬ i) → Setoid.Algebras.⨅ 𝒜 ≅ Setoid.Algebras.⨅ ℬ"},{"name":"⨅≅⨅lowerℓρ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥}\n{α ρᵃ : Level} {ℓᵃ : Level} {I : Set ℓᵃ} {𝒜 : I → Algebra α ρᵃ}\n{ℓ = ℓ₁ : Level} {ρ : Level} →\nSetoid.Algebras.⨅ 𝒜 ≅\nSetoid.Algebras.⨅\n(λ i → Setoid.Algebras.Lift-Alg (𝒜 (Level.Lift.lower i)) ℓ₁ ρ)"},{"name":"⨅≅⨅ℓ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥}\n{α ρᵃ : Level} {𝓘 : Level} {I : Set 𝓘} {𝒜 : I → Algebra α ρᵃ}\n{ℓ = ℓ₁ : Level} →\nSetoid.Algebras.⨅ 𝒜 ≅\nSetoid.Algebras.⨅\n(λ i → Setoid.Algebras.Lift-Alg (𝒜 (Level.Lift.lower i)) ℓ₁ ℓ₁)"},{"name":"⨅≅⨅ℓρ","type":"{𝑆.𝓞 𝑆.𝓥 : Level} {𝑆 : Signature 𝑆.𝓞 𝑆.𝓥}\n{α ρᵃ : Level} {ι : Level} {I : Set ι} {𝒜 : I → Algebra α ρᵃ}\n{ℓ = ℓ₁ : Level} {ρ : Level} →\nSetoid.Algebras.⨅ 𝒜 ≅\nSetoid.Algebras.⨅ (λ i → Setoid.Algebras.Lift-Alg (𝒜 i) ℓ₁ ρ)"},{"name":"𝒾𝒹","type":"{𝓞 𝓥 α ρᵃ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρᵃ} → hom 𝑨 𝑨"}],"lane":{"agdaVersion":"2.8.0","iotcm":["IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_show_module_contents_toplevel Simplified \"Setoid.Homomorphisms\")","IOTCM \"<work>\" None Direct (Cmd_show_version)"],"load":"reused","pid":1368034,"root":"<work>","spawned":false},"module":"Setoid.Homomorphisms","modules":["_≅_","IsEpi","IsHom","IsMon"],"project":{"includePaths":["agda-dojang/agda","<work>"],"librariesFile":"<repo>/agda/libraries","registeredLibraries":[{"includes":["agda"],"libFile":"<repo>/agda-dojang/agda-dojang.agda-lib","name":"agda-dojang","root":"<repo>/agda-dojang"},{"includes":["src"],"libFile":"<nix>/standard-library-2.3/standard-library.agda-lib","name":"standard-library-2.3","root":"<nix>/standard-library-2.3"},{"includes":["src"],"libFile":"<nix>/agda-algebras-unstable-2026-09-07/agda-algebras.agda-lib","name":"agda-algebras","root":"<nix>/agda-algebras-unstable-2026-09-07"}],"root":"<work>","rootSource":"server-config","selectedLibraries":["agda-dojang","standard-library","agda-algebras"]}}

agda-mcp

exports_of(module: Setoid.Functions)

answered25 ms (the file already loaded)

elapsedMs: 25exports: 51modules: 2

the whole answer, as the model saw it (14,833 characters of JSON)

{"checkedFromSource":false,"command":{"args":["--interaction-json"],"binary":"agda","cwd":"<repo>"},"elapsedMs":25,"exports":[{"name":"_⊙_","type":"{α ρᵃ β ρᵇ γ ρᶜ : Level} {A : Relation.Binary.Bundles.Setoid α ρᵃ}\n{B : Relation.Binary.Bundles.Setoid β ρᵇ}\n{C : Relation.Binary.Bundles.Setoid γ ρᶜ} →\nFunction.Bundles.Func B C →\nFunction.Bundles.Func A B → Function.Bundles.Func A C"},{"name":"BijInv","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n(f : Function.Bundles.Func 𝑨 𝑩) →\nIsBijective f → Function.Bundles.Func 𝑩 𝑨"},{"name":"Dom","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ} →\nFunction.Bundles.Func 𝑨 𝑩 → Relation.Binary.Bundles.Setoid α ρᵇ"},{"name":"Image_∋_","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ} →\nFunction.Bundles.Func 𝑨 𝑩 →\nRelation.Binary.Bundles.Setoid.Carrier 𝑩 →\nSet (α Agda.Primitive.⊔ β Agda.Primitive.⊔ ρᵇ)"},{"name":"Imagef∋f","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n{F : Function.Bundles.Func 𝑨 𝑩}\n{a : Relation.Binary.Bundles.Setoid.Carrier 𝑨} →\nImage F ∋ Function.Bundles.Func.to F a"},{"name":"Image⊆Range","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n{F : Function.Bundles.Func 𝑨 𝑩}\n{b : Relation.Binary.Bundles.Setoid.Carrier 𝑩} →\nImage F ∋ b → b Relation.Unary.∈ IsInRange F"},{"name":"Img_∋_","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ} →\n(Relation.Binary.Bundles.Setoid.Carrier 𝑨 →\n Relation.Binary.Bundles.Setoid.Carrier 𝑩) →\nRelation.Binary.Bundles.Setoid.Carrier 𝑩 →\nSet (α Agda.Primitive.⊔ β Agda.Primitive.⊔ ρᵇ)"},{"name":"Inv","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n(F : Function.Bundles.Func 𝑨 𝑩)\n{b : Relation.Binary.Bundles.Setoid.Carrier 𝑩} →\nImage F ∋ b → Relation.Binary.Bundles.Setoid.Carrier 𝑨"},{"name":"Inv'","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n(F : Function.Bundles.Func 𝑨 𝑩)\n{b : Relation.Binary.Bundles.Setoid.Carrier 𝑩} →\nb Relation.Unary.∈ IsInRange F →\nRelation.Binary.Bundles.Setoid.Carrier 𝑨"},{"name":"InvIsInverseʳ","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n{F : Function.Bundles.Func 𝑨 𝑩}\n{b : Relation.Binary.Bundles.Setoid.Carrier 𝑩} (q : Image F ∋ b) →\n(𝑩 Relation.Binary.Bundles.Setoid.≈\n Function.Bundles.Func.to F (Inv F q))\nb"},{"name":"InvIsInverseˡ","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n{F : Function.Bundles.Func 𝑨 𝑩}\n{a : Relation.Binary.Bundles.Setoid.Carrier 𝑨} →\n(𝑨 Relation.Binary.Bundles.Setoid.≈ a) a"},{"name":"IsBijective","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ} →\nFunction.Bundles.Func 𝑨 𝑩 →\nSet (α Agda.Primitive.⊔ ρᵃ Agda.Primitive.⊔ β Agda.Primitive.⊔ ρᵇ)"},{"name":"IsInRange","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ} →\nFunction.Bundles.Func 𝑨 𝑩 →\nRelation.Unary.Pred (Relation.Binary.Bundles.Setoid.Carrier 𝑩)\n(α Agda.Primitive.⊔ ρᵇ)"},{"name":"IsInRange→IsInImage","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n{F : Function.Bundles.Func 𝑨 𝑩}\n{b : Relation.Binary.Bundles.Setoid.Carrier 𝑩} →\nb Relation.Unary.∈ IsInRange F → Image F ∋ b"},{"name":"IsInjective","type":"{a α b β : Level} {𝑨 : Relation.Binary.Bundles.Setoid a α}\n{𝑩 : Relation.Binary.Bundles.Setoid b β} →\nFunction.Bundles.Func 𝑨 𝑩 →\nSet (a Agda.Primitive.⊔ α Agda.Primitive.⊔ β)"},{"name":"IsSurjective","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ} →\nFunction.Bundles.Func 𝑨 𝑩 →\nSet (α Agda.Primitive.⊔ β Agda.Primitive.⊔ ρᵇ)"},{"name":"LeftInvPreserves≈","type":"{a α b β : Level} {𝑨 : Relation.Binary.Bundles.Setoid a α}\n{𝑩 : Relation.Binary.Bundles.Setoid b β}\n(F : Function.Bundles.Injection 𝑨 𝑩)\n{b₀ b₁ : Relation.Binary.Bundles.Setoid.Carrier 𝑩}\n(u : Image Function.Bundles.Injection.function F ∋ b₀)\n(v : Image Function.Bundles.Injection.function F ∋ b₁) →\n(𝑩 Relation.Binary.Bundles.Setoid.≈ b₀) b₁ →\n(𝑨 Relation.Binary.Bundles.Setoid.≈\n Inv (Function.Bundles.Injection.function F) u)\n(Inv (Function.Bundles.Injection.function F) v)"},{"name":"RRan","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ} →\nFunction.Bundles.Func 𝑨 𝑩 →\nRelation.Binary.Bundles.Setoid\n(α Agda.Primitive.⊔ β Agda.Primitive.⊔ ρᵇ) (ρᵃ Agda.Primitive.⊔ ρᵇ)"},{"name":"Ran","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ} →\nFunction.Bundles.Func 𝑨 𝑩 →\nRelation.Binary.Bundles.Setoid\n(α Agda.Primitive.⊔ β Agda.Primitive.⊔ ρᵇ) ρᵇ"},{"name":"SurjInv","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n(f : Function.Bundles.Func 𝑨 𝑩) →\nIsSurjective f →\nRelation.Binary.Bundles.Setoid.Carrier 𝑩 →\nRelation.Binary.Bundles.Setoid.Carrier 𝑨"},{"name":"SurjInvIsInverseʳ","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n(f : Function.Bundles.Func 𝑨 𝑩) (fE : IsSurjective f)\n{b : Relation.Binary.Bundles.Setoid.Carrier 𝑩} →\n(𝑩 Relation.Binary.Bundles.Setoid.≈\n Function.Bundles.Func.to f (SurjInv f fE b))\nb"},{"name":"SurjectionIsSurjection","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ} →\nFunction.Bundles.Surjection 𝑨 𝑩 →\nSetoid.Algebras.Σ-syntax (Function.Bundles.Func 𝑨 𝑩)\n(λ g →\n   Function.Structures.IsSurjection\n   (Relation.Binary.Bundles.Setoid._≈_ 𝑨)\n   (Relation.Binary.Bundles.Setoid._≈_ 𝑩)\n   (Function.Bundles.Func.to g))"},{"name":"SurjectionIsSurjective","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ} →\nFunction.Bundles.Surjection 𝑨 𝑩 →\nSetoid.Algebras.Σ-syntax (Function.Bundles.Func 𝑨 𝑩) IsSurjective"},{"name":"[_]⁻¹","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n(F : Function.Bundles.Func 𝑨 𝑩) →\nrange F → Relation.Binary.Bundles.Setoid.Carrier 𝑨"},{"name":"epic-factor","type":"{α ρᵃ β ρᵇ γ ρᶜ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n{𝑪 : Relation.Binary.Bundles.Setoid γ ρᶜ}\n(f : Function.Bundles.Func 𝑨 𝑩) (g : Function.Bundles.Func 𝑨 𝑪)\n(h : Function.Bundles.Func 𝑪 𝑩) →\nIsSurjective f →\n((i : Relation.Binary.Bundles.Setoid.Carrier 𝑨) →\n (𝑩 Relation.Binary.Bundles.Setoid.≈ Function.Bundles.Func.to f i)\n (Function.Bundles.Func.to h (Function.Bundles.Func.to g i))) →\nIsSurjective h"},{"name":"eq","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n{f\n : Relation.Binary.Bundles.Setoid.Carrier 𝑨 →\n   Relation.Binary.Bundles.Setoid.Carrier 𝑩}\n{b : Relation.Binary.Bundles.Setoid.Carrier 𝑩}\n(a : Relation.Binary.Bundles.Setoid.Carrier 𝑨) →\n(𝑩 Relation.Binary.Bundles.Setoid.≈ b) (f a) → Img f ∋ b"},{"name":"eq","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n{F : Function.Bundles.Func 𝑨 𝑩}\n{b : Relation.Binary.Bundles.Setoid.Carrier 𝑩}\n(a : Relation.Binary.Bundles.Setoid.Carrier 𝑨) →\n(𝑩 Relation.Binary.Bundles.Setoid.≈ b)\n(Function.Bundles.Func.to F a) →\nImage F ∋ b"},{"name":"f∈range","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n{F : Function.Bundles.Func 𝑨 𝑩} →\nRelation.Binary.Bundles.Setoid.Carrier 𝑨 → range F"},{"name":"id-is-injective","type":"{a α : Level} {𝑨 : Relation.Binary.Bundles.Setoid a α} →\nIsInjective 𝑖𝑑"},{"name":"image","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n(F : Function.Bundles.Func 𝑨 𝑩) →\nrange F → Relation.Binary.Bundles.Setoid.Carrier 𝑩"},{"name":"inv","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n(f\n : Relation.Binary.Bundles.Setoid.Carrier 𝑨 →\n   Relation.Binary.Bundles.Setoid.Carrier 𝑩)\n{b : Relation.Binary.Bundles.Setoid.Carrier 𝑩} →\nImg f ∋ b → Relation.Binary.Bundles.Setoid.Carrier 𝑨"},{"name":"invIsInvʳ","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n{f\n : Relation.Binary.Bundles.Setoid.Carrier 𝑨 →\n   Relation.Binary.Bundles.Setoid.Carrier 𝑩}\n{b : Relation.Binary.Bundles.Setoid.Carrier 𝑩} (q : Img f ∋ b) →\n(𝑩 Relation.Binary.Bundles.Setoid.≈ f (inv f q)) b"},{"name":"isSurj","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ} →\n(Relation.Binary.Bundles.Setoid.Carrier 𝑨 →\n Relation.Binary.Bundles.Setoid.Carrier 𝑩) →\nSet (α Agda.Primitive.⊔ β Agda.Primitive.⊔ ρᵇ)"},{"name":"isSurj→IsSurjective","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n(F : Function.Bundles.Func 𝑨 𝑩) →\nisSurj (Function.Bundles.Func.to F) → IsSurjective F"},{"name":"liftFunc","type":"{α ρᵃ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{ℓ = ℓ₁ : Level} →\nFunction.Bundles.Func 𝑨 (𝑙𝑖𝑓𝑡 ℓ₁)"},{"name":"lift∼lower","type":"{α ρᵃ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{β : Level}\n(a : Level.Lift β (Relation.Binary.Bundles.Setoid.Carrier 𝑨)) →\n(𝑨 Relation.Binary.Bundles.Setoid.≈ Level.Lift.lower a)\n(Level.Lift.lower a)"},{"name":"lower∼lift","type":"{α ρᵃ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{β : Level} (a : Relation.Binary.Bundles.Setoid.Carrier 𝑨) →\n(𝑨 Relation.Binary.Bundles.Setoid.≈ a) a"},{"name":"preimage","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n(F : Function.Bundles.Func 𝑨 𝑩) →\nrange F → Relation.Binary.Bundles.Setoid.Carrier 𝑨"},{"name":"preimage≈image","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n(F : Function.Bundles.Func 𝑨 𝑩) (r : range F) →\n(𝑩 Relation.Binary.Bundles.Setoid.≈\n Function.Bundles.Func.to F (preimage F r))\n(image F r)"},{"name":"range","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ} →\nFunction.Bundles.Func 𝑨 𝑩 →\nSet (α Agda.Primitive.⊔ β Agda.Primitive.⊔ ρᵇ)"},{"name":"⁻¹IsInverseʳ","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n{F : Function.Bundles.Func 𝑨 𝑩} {bap : range F} →\n(𝑩 Relation.Binary.Bundles.Setoid.≈\n Function.Bundles.Func.to F ([ F ]⁻¹ bap))\n(bap .proj₁)"},{"name":"⁻¹IsInverseˡ","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n{F : Function.Bundles.Func 𝑨 𝑩}\n{a : Relation.Binary.Bundles.Setoid.Carrier 𝑨} →\n(𝑨 Relation.Binary.Bundles.Setoid.≈ [ F ]⁻¹ (f∈range a)) a"},{"name":"∘-epic","type":"{α ρᵃ β ρᵇ γ ρᶜ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n{𝑪 : Relation.Binary.Bundles.Setoid γ ρᶜ} →\nFunction.Bundles.Surjection 𝑨 𝑪 →\nFunction.Bundles.Surjection 𝑪 𝑩 → Function.Bundles.Surjection 𝑨 𝑩"},{"name":"∘-injective-bare","type":"{a α b β c γ : Level} {A : Set a}\n(_≈₁_ : Relation.Binary.Core.Rel A α) {B : Set b}\n(_≈₂_ : Relation.Binary.Core.Rel B β) {C : Set c}\n(_≈₃_ : Relation.Binary.Core.Rel C γ) {f : A → B} {g : B → C} →\nFunction.Definitions.Injective _≈₁_ _≈₂_ f →\nFunction.Definitions.Injective _≈₂_ _≈₃_ g →\nFunction.Definitions.Injective _≈₁_ _≈₃_ (g Function.Base.∘ f)"},{"name":"⊙-IsSurjective","type":"{α ρᵃ β ρᵇ γ ρᶜ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n{𝑪 : Relation.Binary.Bundles.Setoid γ ρᶜ}\n{G : Function.Bundles.Func 𝑨 𝑪} {H : Function.Bundles.Func 𝑪 𝑩} →\nIsSurjective G → IsSurjective H → IsSurjective (H ⊙ G)"},{"name":"⊙-injection","type":"{a α b β c γ : Level} {𝑨 : Relation.Binary.Bundles.Setoid a α}\n{𝑩 : Relation.Binary.Bundles.Setoid b β}\n{𝑪 : Relation.Binary.Bundles.Setoid c γ} →\nFunction.Bundles.Injection 𝑨 𝑩 →\nFunction.Bundles.Injection 𝑩 𝑪 → Function.Bundles.Injection 𝑨 𝑪"},{"name":"⊙-injective","type":"{a α b β c γ : Level} {𝑨 : Relation.Binary.Bundles.Setoid a α}\n{𝑩 : Relation.Binary.Bundles.Setoid b β}\n{𝑪 : Relation.Binary.Bundles.Setoid c γ}\n(f : Function.Bundles.Func 𝑨 𝑩) (g : Function.Bundles.Func 𝑩 𝑪) →\nIsInjective f → IsInjective g → IsInjective (g ⊙ f)"},{"name":"⌜_⌝","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n(F : Function.Bundles.Func 𝑨 𝑩) →\nRelation.Binary.Bundles.Setoid.Carrier 𝑨 → range F"},{"name":"⟦_⟧⁻¹","type":"{α ρᵃ β ρᵇ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n{𝑩 : Relation.Binary.Bundles.Setoid β ρᵇ}\n(F : Function.Bundles.Func 𝑨 𝑩) →\nFunction.Bundles.Func (Ran F) (Dom F)"},{"name":"𝑖𝑑","type":"{α ρᵃ : Level} {A : Relation.Binary.Bundles.Setoid α ρᵃ} →\nFunction.Bundles.Func A A"},{"name":"𝑙𝑖𝑓𝑡","type":"{α ρᵃ : Level} {𝑨 : Relation.Binary.Bundles.Setoid α ρᵃ}\n(ℓ₁ : Level) →\nRelation.Binary.Bundles.Setoid (α Agda.Primitive.⊔ ℓ₁) ρᵃ"}],"lane":{"agdaVersion":"2.8.0","iotcm":["IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_show_module_contents_toplevel Simplified \"Setoid.Functions\")","IOTCM \"<work>\" None Direct (Cmd_show_version)"],"load":"reused","pid":1368034,"root":"<work>","spawned":false},"module":"Setoid.Functions","modules":["Image_∋_","Img_∋_"],"project":{"includePaths":["agda-dojang/agda","<work>"],"librariesFile":"<repo>/agda/libraries","registeredLibraries":[{"includes":["agda"],"libFile":"<repo>/agda-dojang/agda-dojang.agda-lib","name":"agda-dojang","root":"<repo>/agda-dojang"},{"includes":["src"],"libFile":"<nix>/standard-library-2.3/standard-library.agda-lib","name":"standard-library-2.3","root":"<nix>/standard-library-2.3"},{"includes":["src"],"libFile":"<nix>/agda-algebras-unstable-2026-09-07/agda-algebras.agda-lib","name":"agda-algebras","root":"<nix>/agda-algebras-unstable-2026-09-07"}],"root":"<work>","rootSource":"server-config","selectedLibraries":["agda-dojang","standard-library","agda-algebras"]}}

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

agda-mcp

type_of(expr: _≅_.to)

answered3 ms (the file already loaded)

type: {𝓞 𝓥 α ρᵃ β ρᵇ : Level} {𝑆 : Data.Product.Σ (Set 𝓞) (λ F → F → Set 𝓥)} {𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} → 𝑨 ≅ 𝑩 → Data.Product.Σ (Function.Bundles.Func (Algebra.Domain 𝑨) (Algebra.Domain 𝑩)) (IsHom 𝑨 𝑩)elapsedMs: 3

the whole answer, as the model saw it (1,315 characters of JSON)

{"checkedFromSource":false,"command":{"args":["--interaction-json"],"binary":"agda","cwd":"<repo>"},"elapsedMs":3,"expr":"_≅_.to","lane":{"agdaVersion":"2.8.0","iotcm":["IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_infer_toplevel Normalised \"_\\8773_.to\")","IOTCM \"<work>\" None Direct (Cmd_show_version)"],"load":"reused","pid":1368034,"root":"<work>","spawned":false},"project":{"includePaths":["agda-dojang/agda","<work>"],"librariesFile":"<repo>/agda/libraries","registeredLibraries":[{"includes":["agda"],"libFile":"<repo>/agda-dojang/agda-dojang.agda-lib","name":"agda-dojang","root":"<repo>/agda-dojang"},{"includes":["src"],"libFile":"<nix>/standard-library-2.3/standard-library.agda-lib","name":"standard-library-2.3","root":"<nix>/standard-library-2.3"},{"includes":["src"],"libFile":"<nix>/agda-algebras-unstable-2026-09-07/agda-algebras.agda-lib","name":"agda-algebras","root":"<nix>/agda-algebras-unstable-2026-09-07"}],"root":"<work>","rootSource":"server-config","selectedLibraries":["agda-dojang","standard-library","agda-algebras"]},"scope":"toplevel","type":"{𝓞 𝓥 α ρᵃ β ρᵇ : Level}\n{𝑆 : Data.Product.Σ (Set 𝓞) (λ F → F → Set 𝓥)} {𝑨 : Algebra α ρᵃ}\n{𝑩 : Algebra β ρᵇ} →\n𝑨 ≅ 𝑩 →\nData.Product.Σ\n(Function.Bundles.Func (Algebra.Domain 𝑨) (Algebra.Domain 𝑩))\n(IsHom 𝑨 𝑩)"}

the model
Good, `_≅_.to` resolves fine. Now let's check the type of `_≤_` to confirm `p` unfolds to `(f , finj)` shape.

agda-mcp

type_of(expr: _≤_)

answered2 ms (the file already loaded)

type: {𝓞 𝓥 : Level} {𝑆 = ρᵃ : Data.Product.Σ (Set 𝓞) (λ α → α → Set 𝓥)} {α = β : Level} {ρᵃ = ρᵇ : Level} {β = F : Level} {ρᵇ = 𝑆 : Level} → Algebra β ρᵇ → Algebra F 𝑆 → Set (𝓞 Agda.Primitive.⊔ 𝓥 Agda.Primitive.⊔ β Agda.Primit…elapsedMs: 2

the whole answer, as the model saw it (1,373 characters of JSON)

{"checkedFromSource":false,"command":{"args":["--interaction-json"],"binary":"agda","cwd":"<repo>"},"elapsedMs":2,"expr":"_≤_","lane":{"agdaVersion":"2.8.0","iotcm":["IOTCM \"<work>/Subalgebras-sub-trans-iso.agda\" None Direct (Cmd_infer_toplevel Normalised \"_\\8804_\")","IOTCM \"<work>\" None Direct (Cmd_show_version)"],"load":"reused","pid":1368034,"root":"<work>","spawned":false},"project":{"includePaths":["agda-dojang/agda","<work>"],"librariesFile":"<repo>/agda/libraries","registeredLibraries":[{"includes":["agda"],"libFile":"<repo>/agda-dojang/agda-dojang.agda-lib","name":"agda-dojang","root":"<repo>/agda-dojang"},{"includes":["src"],"libFile":"<nix>/standard-library-2.3/standard-library.agda-lib","name":"standard-library-2.3","root":"<nix>/standard-library-2.3"},{"includes":["src"],"libFile":"<nix>/agda-algebras-unstable-2026-09-07/agda-algebras.agda-lib","name":"agda-algebras","root":"<nix>/agda-algebras-unstable-2026-09-07"}],"root":"<work>","rootSource":"server-config","selectedLibraries":["agda-dojang","standard-library","agda-algebras"]},"scope":"toplevel","type":"{𝓞 𝓥 : Level} {𝑆 = ρᵃ : Data.Product.Σ (Set 𝓞) (λ α → α → Set 𝓥)}\n{α = β : Level} {ρᵃ = ρᵇ : Level} {β = F : Level}\n{ρᵇ = 𝑆 : Level} →\nAlgebra β ρᵇ →\nAlgebra F 𝑆 →\nSet\n(𝓞 Agda.Primitive.⊔ 𝓥 Agda.Primitive.⊔ β Agda.Primitive.⊔ ρᵇ\n Agda.Primitive.⊔ F\n Agda.Primitive.⊔ 𝑆)"}

the model
Now let's fill the hole using pattern matching on `p` directly, mirroring the library proof.
files
Edit(replace_all: false, file_path: <work>/Subalgebras-sub-trans-iso.agda, old_string: ≤-trans-≅′ p B≅C = {!!}, new_string: ≤-trans-≅′ (h , hinj) B≅C = ⊙-hom h (_≅_.to B≅C) , ⊙-injective (proj₁ h) (proj₁ (_≅_.to B≅C)) hinj (≅toInjective B≅C))
answered
The file <work>/Subalgebras-sub-trans-iso.agda has been updated successfully. (file state is current in your context — n…
the whole answer, as the model saw it (143 characters of text)
The file <work>/Subalgebras-sub-trans-iso.agda has been updated successfully. (file state is current in your context — no need to Read it back)

agda-mcp

check_file()

answered5.5 s

success: trueholesCount: 0diagnosticsTotal: 0verdict.exitCode: 0elapsedMs: 5485diagnostics: 0holes: 0

the whole answer, as the model saw it (1,818 characters of JSON)

{"checkedFromSource":true,"command":{"args":["-i","agda-dojang/agda","--library-file=agda/libraries","-l","agda-dojang","-l","standard-library","-l","agda-algebras","--safe","-i","<work>","<work>/Subalgebras-sub-trans-iso.agda"],"binary":"<nix>/agdaWithPackages-2.8.0/bin/agda","cwd":"<repo>"},"diagnostics":[],"diagnosticsTotal":0,"elapsedMs":5485,"holes":[],"holesCount":0,"project":{"includePaths":["agda-dojang/agda","<work>"],"librariesFile":"<repo>/agda/libraries","registeredLibraries":[{"includes":["agda"],"libFile":"<repo>/agda-dojang/agda-dojang.agda-lib","name":"agda-dojang","root":"<repo>/agda-dojang"},{"includes":["src"],"libFile":"<nix>/standard-library-2.3/standard-library.agda-lib","name":"standard-library-2.3","root":"<nix>/standard-library-2.3"},{"includes":["src"],"libFile":"<nix>/agda-algebras-unstable-2026-09-07/agda-algebras.agda-lib","name":"agda-algebras","root":"<nix>/agda-algebras-unstable-2026-09-07"}],"root":"<work>","rootSource":"server-config","selectedLibraries":["agda-dojang","standard-library","agda-algebras"]},"success":true,"timedOut":false,"verdict":{"equivalentTo":"equivalent-to: <nix>/agdaWithPackages-2.8.0/bin/agda -i agda-dojang/agda --library-file=agda/libraries -l agda-dojang -l standard-library -l agda-algebras --safe -i <work> <work>/Subalgebras-sub-trans-iso.agda","exitCode":0,"meaning":"success is true if and only if that command exited 0, so it means exactly what green means in a batch build. Unsolved metavariables, unsolved constraints, and open holes all make agda exit non-zero and so make success false; there is no interaction mode anywhere in this server. The verdict is read from the exit code alone — never from the diagnostics text — so a change in Agda's message format can empty the diagnostics list but cannot turn a failing build green."}}

the model
check_file reports success (exit code 0, no diagnostics, no holes) on the final file.

The model’s words and its calls are quoted from transcript.jsonl; every answer below a call is the tool’s own, in full. The client billed 1,030 thinking tokens over the session; their text is not in the archive.

solvedthe judge, in outcome.json

Every gate passed, and the definition does not refer to the library’s own lemma for this statement, so the row counts as a solve.

Agda’s exit code on the file 0

statement preserved yes

last verdict taken from check_file

the library’s own proof in view before the edit yes, the model read the file that holds it

the file the judge read, marked against the obligation it started as

 -- Subalgebras-sub-trans-iso.agda
 --
 -- File: data/benchmarks/agda-algebras-v0/obligations/Subalgebras-sub-trans-iso.agda
 --
 -- Benchmark obligation: algebras-subalgebras-sub-trans-iso
 -- Difficulty: non-obvious
 -- Source: Setoid.Subalgebras.Properties (agda-algebras)
 -- Import stratum: wholesale
 -- Strategy: pairing
 --
 module Subalgebras-sub-trans-iso where
 
 open import AgdaDojang.Debug
 
 open import Agda.Primitive   using ( Level )
 open import Data.Product     using ( _,_ ; proj₁ ; proj₂ )
 
 open import Overture              using ( Signature )
 open import Setoid.Algebras       using ( Algebra )
 open import Setoid.Functions
 open import Setoid.Homomorphisms
 open import Setoid.Subalgebras
 
 ≤-trans-≅′ : {𝓞 𝓥 α ρᵃ β ρᵇ γ ρᶜ : Level} {𝑆 : Signature 𝓞 𝓥}
              {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ}
   →  𝑨 ≤ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≤ 𝑪
-≤-trans-≅′ p B≅C = {!!}
+≤-trans-≅′ (h , hinj) B≅C =
+  ⊙-hom h (_≅_.to B≅C) , ⊙-injective (proj₁ h) (proj₁ (_≅_.to B≅C)) hinj (≅toInjective B≅C)

reports/agent-bench/arm162-mcp-1/subjects/algebras-subalgebras-sub-trans-iso/final/Subalgebras-sub-trans-iso.agda

≤-trans-≅′, shell only

Shell only. The same model finds the same lemmas with grep and find over the library's sources, and its verdicts are runs of agda in the shell, which the archive does not time: the first is refused, the second accepted.

model: Sonnet 5 (claude-sonnet-5)
instrument: shell only
run: arm162-shell-1 2026-09-21
server: the server of 2026-09-21 (fourteen tools, the libraries' sources readable on every arm)
client: 2.1.261 (Claude Code)
turns: 15
tool calls: 14 Read ×1, Bash ×11, Edit ×2
wall clock: 1.2 min (indicative: subjects ran three at a time)
cost, list price: USD 0.17

the statement, as the obligation states it, with the proof removed

{𝓞 𝓥 α ρᵃ β ρᵇ γ ρᶜ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ} →  𝑨 ≤ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≤ 𝑪

the session, 15 turns and 14 tool calls

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

files

Read(file_path: <work>/Subalgebras-sub-trans-iso.agda)

answered

1 -- Subalgebras-sub-trans-iso.agda

the whole answer, as the model saw it (963 characters of text)

1   -- Subalgebras-sub-trans-iso.agda
2   --
3   -- File: data/benchmarks/agda-algebras-v0/obligations/Subalgebras-sub-trans-iso.agda
4   --
5   -- Benchmark obligation: algebras-subalgebras-sub-trans-iso
6   -- Difficulty: non-obvious
7   -- Source: Setoid.Subalgebras.Properties (agda-algebras)
8   -- Import stratum: wholesale
9   -- Strategy: pairing
10  --
11  module Subalgebras-sub-trans-iso where
12  
13  open import AgdaDojang.Debug
14  
15  open import Agda.Primitive   using ( Level )
16  open import Data.Product     using ( _,_ ; proj₁ ; proj₂ )
17  
18  open import Overture              using ( Signature )
19  open import Setoid.Algebras       using ( Algebra )
20  open import Setoid.Functions
21  open import Setoid.Homomorphisms
22  open import Setoid.Subalgebras
23  
24  ≤-trans-≅′ : {𝓞 𝓥 α ρᵃ β ρᵇ γ ρᶜ : Level} {𝑆 : Signature 𝓞 𝓥}
25               {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ}
26    →  𝑨 ≤ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≤ 𝑪
27  ≤-trans-≅′ p B≅C = {!!}
28

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.
shell
Bash(command: grep -n "≤-trans-≅\|_≤_\|_≅_" -r <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/*.agda | head -80)
answered
ugrep: warning: <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/*.agda: No such file or directory
the whole answer, as the model saw it (112 characters of text)
ugrep: warning: <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/*.agda: No such file or directory

shell

Bash(command: find <nix>/agda-algebras-unstable-2026-09-07 -iname "*Subalgebras*")

answered

<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras.lagda.md

the whole answer, as the model saw it (818 characters of text)

<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras.lagda.md
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras
<nix>/agda-algebras-unstable-2026-09-07/src/Legacy/Base/Subalgebras.lagda.md
<nix>/agda-algebras-unstable-2026-09-07/src/Legacy/Base/Subalgebras
<nix>/agda-algebras-unstable-2026-09-07/src/Legacy/Base/Subalgebras/Subalgebras.lagda.md
<nix>/agda-algebras-unstable-2026-09-07/_build/2.8.0/agda/src/Setoid/Subalgebras.agdai
<nix>/agda-algebras-unstable-2026-09-07/_build/2.8.0/agda/src/Setoid/Subalgebras
<nix>/agda-algebras-unstable-2026-09-07/_build/2.8.0/agda/src/Legacy/Base/Subalgebras.agdai
<nix>/agda-algebras-unstable-2026-09-07/_build/2.8.0/agda/src/Legacy/Base/Subalgebras
<nix>/agda-algebras-unstable-2026-09-07/_build/2.8.0/agda/src/Legacy/Base/Subalgebras/Subalgebras.agdai

shell

Bash(command: find <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras -iname "*")

answered

<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras

the whole answer, as the model saw it (915 characters of text)

<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Basic.lagda.md
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Subuniverses.lagda.md
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Subdirect.lagda.md
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/CompleteLattice.lagda.md
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Subdirect
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Subdirect/Basic.lagda.md
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Subdirect/Finite.lagda.md
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Subdirect/BirkhoffSI.lagda.md
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Subdirect/Irreducible.lagda.md

shell

Bash(command: grep -n "≤-trans-≅\|≅\|≤" <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md | head -100)

answered

13:`_≤_`{.AgdaFunction} that the rest of the library relies on: that it is a

the whole answer, as the model saw it (4,561 characters of text)

13:`_≤_`{.AgdaFunction} that the rest of the library relies on: that it is a
18:(`≤-preorder`{.AgdaFunction}), which is the only sensible choice, since mutual
21:Agda's universes are not cumulative, so a `≤` established at one level has to be
47:open import Setoid.Homomorphisms      using  ( hom ; IsHom ; 𝒾𝒹 ; ⊙-hom ; _≅_
48:                                             ; ≅toInjective ; ≅fromInjective ; mkiso
49:                                             ; ≅-sym ; ≅-refl ; ≅-trans
50:                                             ; Lift-≅ˡ ; Lift-≅ ; Lift-≅ʳ)
51:open import Setoid.Subalgebras.Basic  using  ( _≤_ ; _≥_ ; _≤c_ )
60:open _≅_
62:≅→≤ : {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ} → 𝑨 ≅ 𝑩 → 𝑨 ≤ 𝑩
63:≅→≤ φ = (to φ) , ≅toInjective φ
65:≅→≥ : {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ} → 𝑨 ≅ 𝑩 → 𝑨 ≥ 𝑩
66:≅→≥ φ = (from φ) , ≅fromInjective φ
68:≤-refl : {𝑨 𝑩 : Algebra {𝑆 = 𝑆} α ρᵃ} → 𝑨 ≅ 𝑩 → 𝑨 ≤ 𝑩
69:≤-refl = ≅→≤
71:≥-refl : {𝑨 𝑩 : Algebra {𝑆 = 𝑆} α ρᵃ} → 𝑨 ≅ 𝑩 → 𝑨 ≥ 𝑩
72:≥-refl = ≅→≤ ∘ ≅-sym
74:≤-reflexive : {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} → 𝑨 ≤ 𝑨
75:≤-reflexive {𝑨 = 𝑨} = 𝒾𝒹 , id-is-injective {𝑨 = 𝔻[ 𝑨 ]}
78:  ≤-trans : 𝑨 ≤ 𝑩 → 𝑩 ≤ 𝑪 → 𝑨 ≤ 𝑪
79:  ≤-trans ( f , finj ) ( g , ginj ) = (⊙-hom f g) , ⊙-injective (proj₁ f) (proj₁ g) finj ginj
81:  ≤-trans-≅ : 𝑨 ≤ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≤ 𝑪
82:  ≤-trans-≅ (h , hinj) B≅C =
83:    ⊙-hom h (to B≅C) , ⊙-injective (proj₁ h) (proj₁ (to B≅C)) hinj (≅toInjective B≅C)
85:  ≅-trans-≤ : 𝑨 ≅ 𝑩 → 𝑩 ≤ 𝑪 → 𝑨 ≤ 𝑪
86:  ≅-trans-≤ A≅B (h , hinj) =
87:    ⊙-hom (to A≅B) h , ⊙-injective (proj₁ (to A≅B)) (proj₁ h) (≅toInjective A≅B) hinj
91:  ≥-trans A≥B B≥C = ≤-trans B≥C A≥B
93:≤→≤c→≤c : {𝑨 : Algebra {𝑆 = 𝑆} α α}{𝑩 : Algebra {𝑆 = 𝑆} α α}{𝒦 : Pred(Algebra {𝑆 = 𝑆} α α) (ov {𝑆 = 𝑆} α)}
94:  → 𝑨 ≤ 𝑩 → 𝑩 ≤c 𝒦 → 𝑨 ≤c 𝒦
95:≤→≤c→≤c A≤B sB = (proj₁ sB) , (proj₁ (proj₂ sB) , ≤-trans A≤B (proj₂ (proj₂ sB)))
99:  open RelStructs {a = ov {𝑆 = 𝑆} (α ⊔ ρᵃ)} {ℓ = 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρᵃ} (_≅_ {α = α}{ρᵃ = ρᵃ}{𝑆 = 𝑆})
102:  ≤-preorder : IsPreorder _≤_
103:  isEquivalence  ≤-preorder = record { refl = ≅-refl ; sym = ≅-sym ; trans = ≅-trans }
104:  reflexive      ≤-preorder = ≤-refl
105:  trans          ≤-preorder A≤B B≤C = ≤-trans A≤B B≤C
108:  A≥B×B≅C→A≥C : 𝑨 ≥ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≥ 𝑪
109:  A≥B×B≅C→A≥C A≥B B≅C  = ≥-trans A≥B (≅→≥ B≅C)
111:  A≤B×B≅C→A≤C : 𝑨 ≤ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≤ 𝑪
112:  A≤B×B≅C→A≤C A≤B B≅C = ≤-trans  A≤B (≅→≤ B≅C)
114:  A≅B×B≥C→A≥C : 𝑨 ≅ 𝑩 → 𝑩 ≥ 𝑪 → 𝑨 ≥ 𝑪
115:  A≅B×B≥C→A≥C A≅B B≥C = ≥-trans (≅→≥ A≅B) B≥C
117:  A≅B×B≤C→A≤C : 𝑨 ≅ 𝑩 → 𝑩 ≤ 𝑪 → 𝑨 ≤ 𝑪
118:  A≅B×B≤C→A≤C A≅B B≤C = ≤-trans (≅→≤ A≅B) B≤C
123:  (φ : 𝑨 ≅ 𝑩) → IsInjective (proj₁ (to φ))
132:≤-mono : {𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ}{𝒦 𝒦' : Pred (Algebra {𝑆 = 𝑆} α ρᵃ) γ}
133:  → 𝒦 ⊆ 𝒦' → 𝑩 ≤c 𝒦 → 𝑩 ≤c 𝒦'
134:≤-mono KK' (𝑨 , (KA , B≤A)) = 𝑨 , ((KK' KA) , B≤A)
139:Ten lemmas of one shape: transport a `≤` or a `≥` across the isomorphism between
141:of a mixed transitivity lemma from above to one of the `Lift-≅`{.AgdaFunction}
143:`Lift-≤-Lift`{.AgdaFunction} variants then compose two of those.  Either way no
152:+  `≤-Liftˡ`{.AgdaFunction}, `≤-Liftʳ`{.AgdaFunction} and
153:   `≤-Lift`{.AgdaFunction} lift the algebra on the right of `≤`, the larger one;
156:+  `Lift-≤-Liftˡ`{.AgdaFunction}, `Lift-≤-Liftʳ`{.AgdaFunction} and
157:   `Lift-≤-Lift`{.AgdaFunction} lift both algebras at once, and are literally the
166:  → 𝑩 ≤c 𝒦 → (Lift-Algˡ 𝑩 ℓ) ≤c 𝒦
167:Lift-is-sub (𝑨 , (KA , B≤A)) = 𝑨 , (KA , A≥B×B≅C→A≥C B≤A Lift-≅ˡ)
170:  ≤-Liftˡ : {ℓ : Level} → 𝑨 ≤ 𝑩 → 𝑨 ≤ Lift-Algˡ 𝑩 ℓ
171:  ≤-Liftˡ A≤B = A≤B×B≅C→A≤C A≤B Lift-≅ˡ
173:  ≤-Liftʳ : {ρ : Level} → 𝑨 ≤ 𝑩 → 𝑨 ≤ Lift-Algʳ 𝑩 ρ
174:  ≤-Liftʳ A≤B = A≤B×B≅C→A≤C A≤B Lift-≅ʳ
176:  ≤-Lift : {ℓ ρ : Level} → 𝑨 ≤ 𝑩 → 𝑨 ≤ Lift-Alg 𝑩 ℓ ρ
177:  ≤-Lift A≤B = A≤B×B≅C→A≤C  A≤B Lift-≅
180:  ≥-Liftˡ A≥B = A≥B×B≅C→A≥C A≥B Lift-≅ˡ
183:  ≥-Liftʳ A≥B = A≥B×B≅C→A≥C A≥B Lift-≅ʳ
186:  ≥-Lift A≥B = A≥B×B≅C→A≥C A≥B Lift-≅
189:  Lift-≤-Liftˡ : {ℓᵃ ℓᵇ : Level} → 𝑨 ≤ 𝑩 → Lift-Algˡ 𝑨 ℓᵃ ≤ Lift-Algˡ 𝑩 ℓᵇ
190:  Lift-≤-Liftˡ A≤B = ≥-Liftˡ (≤-Liftˡ A≤B)
192:  Lift-≤-Liftʳ : {rᵃ rᵇ : Level} → 𝑨 ≤ 𝑩 → Lift-Algʳ 𝑨 rᵃ ≤ Lift-Algʳ 𝑩 rᵇ
193:  Lift-≤-Liftʳ A≤B = ≥-Liftʳ (≤-Liftʳ A≤B)
195:  Lift-≤-Lift : {a rᵃ b rᵇ : Level}
196:    → 𝑨 ≤ 𝑩 → Lift-Alg 𝑨 a rᵃ ≤ Lift-Alg 𝑩 b rᵇ
197:  Lift-≤-Lift A≤B = ≥-Lift (≤-Lift A≤B)
202:`⨅-≤`{.AgdaFunction} is the compatibility of the subalgebra relation with
203:products: if `ℬ i ≤ 𝒜 i` for every index `i`, then `⨅ ℬ ≤ ⨅ 𝒜`.  The embedding is
221:  ⨅-≤ : (∀ i → ℬ i ≤ 𝒜 i) → ⨅ ℬ ≤ ⨅ 𝒜
222:  ⨅-≤ B≤A = h , hM
228:      homAt = λ i → proj₁ (B≤A i)
241:    hM = λ xy i → (proj₂ (B≤A i)) (xy i)

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

shell

Bash(command: grep -n "⊙-hom\|⊙-injective\b" <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/*.lagda.md | head -30
echo ---
grep -n "^_≤_\|_≤_ " <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Basic.lagda.md | head -20)

answered

<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:34:+ **composition**, `⊙-hom`{.AgdaFunc…

the whole answer, as the model saw it (2,433 characters of text)

<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:34:+  **composition**, `⊙-hom`{.AgdaFunction}, and the homomorphisms that witness
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/HomomorphicImages.lagda.md:39:                                                      ; lift-hom-lemma ; ⊙-hom )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/HomomorphicImages.lagda.md:182:  Lift-HomImage-lemma {γ} φ =  ⊙-hom (φ .proj₁) (from Lift-≅) ,
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/HomomorphicImages.lagda.md:188:  HomImage-≅ φ A≅B = ⊙-hom (φ .proj₁) (to A≅B) , ⊙-IsSurjective (φ .proj₂) (toIsSurjective A≅B)
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/HomomorphicImages.lagda.md:191:  HomImage-≅' φ A'≅B = (⊙-hom (from A'≅B) (proj₁ φ)) , ⊙-IsSurjective (fromIsSurjective A'≅B) (φ .proj₂)
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:66:open import Setoid.Homomorphisms.Properties  using  ( ⊙-hom ; ToLiftˡ ; FromLiftˡ
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:145:  f = ⊙-hom (to ab) (to bc)
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:148:  g = ⊙-hom (from bc) (from ab)
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Properties.lagda.md:73:+  `⊙-hom`{.AgdaFunction} and `⊙-epi`{.AgdaFunction} are the bundled forms.
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Properties.lagda.md:78:`⊙-hom f g` is read as "apply `f`, then `g`".
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Properties.lagda.md:102:  ⊙-hom : hom 𝑨 𝑩 → hom 𝑩 𝑪  → hom 𝑨 𝑪
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Properties.lagda.md:103:  ⊙-hom (h , hhom) (g , ghom) = g ⊙ h , ⊙-is-hom hhom ghom
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Properties.lagda.md:182:  ToLift = ⊙-hom ToLiftˡ ToLiftʳ
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Properties.lagda.md:185:  FromLift = ⊙-hom FromLiftʳ FromLiftˡ
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Properties.lagda.md:255:  Lift-hom-fst φ _ _ = ⊙-hom FromLift φ
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Properties.lagda.md:258:  Lift-hom-snd φ _ _ = ⊙-hom φ ToLift
---
102:  _≤_   -- alias for subalgebra relation

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

shell

Bash(command: grep -n "⊙-injective" -r <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/ 2>/dev/null | head -20
echo ---
sed -n '1,40p' <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Basic.lagda.md)

answered

<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Functions/Injective.lagda.md:91: ⊙-injective : (f : 𝑨 ⟶ 𝑩)(g : 𝑩 ⟶…

the whole answer, as the model saw it (3,246 characters of text)

<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Functions/Injective.lagda.md:91:  ⊙-injective :  (f : 𝑨 ⟶ 𝑩)(g : 𝑩 ⟶ 𝑪)
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Functions/Injective.lagda.md:95:  ⊙-injective _ _ finj ginj = finj ∘ ginj
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Functions/Injective.lagda.md:101:   ; injective = ⊙-injective (function fi) (function gi) (injective fi) (injective gi)
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md:46:open import Setoid.Functions          using  ( id-is-injective ; IsInjective ; ⊙-injective )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md:79:  ≤-trans ( f , finj ) ( g , ginj ) = (⊙-hom f g) , ⊙-injective (proj₁ f) (proj₁ g) finj ginj
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md:83:    ⊙-hom h (to B≅C) , ⊙-injective (proj₁ h) (proj₁ (to B≅C)) hinj (≅toInjective B≅C)
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md:87:    ⊙-hom (to A≅B) h , ⊙-injective (proj₁ (to A≅B)) (proj₁ h) (≅toInjective A≅B) hinj
---
---
layout: default
title : "Setoid.Subalgebras.Basic module (The Agda Universal Algebra Library)"
date : "2021-07-17"
author: "agda-algebras development team"
---

#### Subalgebras of setoid algebras

This is the [Setoid.Subalgebras.Basic][] module of the [Agda Universal Algebra Library][].

`𝑨` is a **subalgebra** of `𝑩`, written `𝑨 ≤ 𝑩`, just in case `𝑨` can be
*homomorphically embedded* in `𝑩`: there is a homomorphism from `𝑨` to `𝑩` whose
underlying map is injective.

Note that the notion of subalgebra that we define here is different from the
standard textbook definition, which defines a *subuniverse* to be a subset of
the carrier of an algebra that is closed under the operations (as we do in the
[Setoid.Subalgebras.Subuniverses][] module); a subalgebra is then a subuniverse
together with the operations of the larger algebra restricted to it.  Nothing in
our definition requires the carrier of a subalgebra of `𝑩` to be a subset of the
carrier of `𝑩`.[^1]

Our subalgebra relation `_≤_`{.AgdaFunction} is clearly reflexive and transitive,
so it is a *preorder*; that is exactly what [Setoid.Subalgebras.Properties][]
proves, as `≤-preorder`{.AgdaFunction}, and it is the only order-theoretic fact
about `_≤_`{.AgdaFunction} that this subtree establishes.

It is not a partial order.  Antisymmetry would require that `𝑨 ≤ 𝑩` and `𝑩 ≤ 𝑨`
imply `𝑨 ≈ 𝑩` for some suitable `≈`, and read as "on the nose" equality that
plainly fails.  The tempting repair is to read `≈` as isomorphism, but that fails
too: `𝑨 ≤ 𝑩` and `𝑩 ≤ 𝑨` supply injective homomorphisms in both directions, and a
pair of injections is not an isomorphism.  Neither map need invert the other, and
in general no isomorphism need exist at all — the free groups on two and on three
generators embed in each other yet are not isomorphic, as their abelianizations
`ℤ²` and `ℤ³` already show.  Extracting a bijection from two injections is
Cantor–Bernstein, which is unavailable constructively, and the bijection it
yields classically need not be a homomorphism.

For **finite** algebras the repair does work, and that is the setting much of this

the model
Now let me write the fix, adding needed imports and the definition.
files
Edit(replace_all: false, file_path: <work>/Subalgebras-sub-trans-iso.agda, old_string: ≤-trans-≅′ p B≅C = {!!}, new_string: ≤-trans-≅′ (h , hinj) B≅C = ⊙-hom h (to B≅C) , ⊙-injective (proj₁ h) (proj₁ (to B≅C)) hinj (≅toInjective B≅C))
answered
The file <work>/Subalgebras-sub-trans-iso.agda has been updated successfully. (file state is current in your context — n…
the whole answer, as the model saw it (143 characters of text)
The file <work>/Subalgebras-sub-trans-iso.agda has been updated successfully. (file state is current in your context — no need to Read it back)
thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

shell

Bash(command: grep -n "⊙-hom\|⊙-injective\|≅toInjective\|^open\|to \b" <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms.lagda.md
echo ---FUNCTIONS---
grep -n "^open\|⊙-injective" <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Functions.lagda.md)

answered

25:+ [Setoid.Homomorphisms.Products][]: the homomorphism into a product induced by a

the whole answer, as the model saw it (852 characters of text)

25:+  [Setoid.Homomorphisms.Products][]: the homomorphism into a product induced by a
40:open import Setoid.Homomorphisms.Basic              public
41:open import Setoid.Homomorphisms.Kernels            public
42:open import Setoid.Homomorphisms.Products           public
43:open import Setoid.Homomorphisms.Noether            public
44:open import Setoid.Homomorphisms.Factor             public
45:open import Setoid.Homomorphisms.Isomorphisms       public
46:open import Setoid.Homomorphisms.HomomorphicImages  public
47:open import Setoid.Homomorphisms.Properties         public
---FUNCTIONS---
45:open import Setoid.Functions.Basic       public
46:open import Setoid.Functions.Bijective   public
47:open import Setoid.Functions.Injective   public
48:open import Setoid.Functions.Inverses    public
49:open import Setoid.Functions.Surjective  public

the model
Good, those are all re-exported publicly. Let's check `≅toInjective` and `to` field, and `_≅_` module in Isomorphisms.lagda.md, then typecheck.

shell

Bash(command: grep -n "≅toInjective\|record _≅_\|to :\|to \b" <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md | head -20)

answered

13:both directions that are mutually inverse up to the setoid equalities of the two

the whole answer, as the model saw it (1,407 characters of text)

13:both directions that are mutually inverse up to the setoid equalities of the two
27:+  `≅toInjective`{.AgdaFunction}: the forward map of an isomorphism is injective;
31:+  `Lift-≅`{.AgdaFunction}: an algebra is isomorphic to each of its universe
45:open import Agda.Primitive              using () renaming ( Set to Type )
49:open import Function                    using ()  renaming ( Func to _⟶_ )
71:open _⟶_ using ( cong ) renaming ( to to _⟨$⟩_ )
87:However, with four components, an equivalent record type is easier to work with.
91:  open Setoid 𝔻[ 𝑨 ] using ( sym ; trans ) renaming ( _≈_ to _≈₁_ )
92:  open Setoid 𝔻[ 𝑩 ] using () renaming ( _≈_ to _≈₂_ ; sym to sym₂ ; trans to trans₂)
94:  record _≅_ : Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ β ⊔ ρᵃ ⊔ ρᵇ ) where
97:      to : hom 𝑨 𝑩
100:      from∼to : ∀ a → from .proj₁ ⟨$⟩ (to .proj₁ ⟨$⟩ a) ≈₁ a
111:      Goal = trans (sym (from∼to x)) (trans ξ (from∼to y))
114:    fromIsSurjective {y} = eq (to .proj₁ ⟨$⟩ y) (sym (from∼to y))
126:and forth between them which compose to the identity map.
145:  f = ⊙-hom (to ab) (to bc)
150:  open Setoid 𝔻[ 𝑪 ] using () renaming ( _≈_ to _≈₃_ ; trans to trans₃ )
152:  τ b = trans₃ (cong (to bc .proj₁) (to∼from ab (from bc .proj₁ ⟨$⟩ b))) (to∼from bc b)
154:  open Setoid 𝔻[ 𝑨 ] using () renaming ( _≈_ to _≈₁_ ; trans to trans₁ )
156:  ν a = trans₁ (cong (from ab .proj₁) (from∼to bc (to ab .proj₁ ⟨$⟩ a))) (from∼to ab a)

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

shell

Bash(command: grep -n "open _≅_\|module _≅_\|open.*_≅_" -r <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms* <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms.lagda.md)

answered

<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/HomomorphicImages.lagda.md:37:open import Setoid.Homomo…

the whole answer, as the model saw it (479 characters of text)

<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/HomomorphicImages.lagda.md:37:open import Setoid.Homomorphisms.Isomorphisms  using  ( _≅_ ; Lift-≅ )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/HomomorphicImages.lagda.md:180:  open _≅_
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/HomomorphicImages.lagda.md:186:  open _≅_
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:132:open _≅_

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

shell

Bash(command: agda --no-default-libraries --library-file <repo>/agda/libraries --library standard-library --library agda-dojang --library agda-algebras --safe -i . Subalgebras-sub-trans-iso.agda)

refusedno timing in the archive

Exit code 42

the whole answer, as the model saw it (326 characters of text)

Exit code 42
Checking Subalgebras-sub-trans-iso (<work>/Subalgebras-sub-trans-iso.agda).
<work>/Subalgebras-sub-trans-iso.agda:28.12-14: error: [NotInScope]
Not in scope:
  to
  at <work>/Subalgebras-sub-trans-iso.agda:28.12-14
    (did you mean
       '_≅_.to' or
       'Setoid.Homomorphisms._≅_.to'?)
when scope checking to

the model
Need to open `_≅_`. Let me add that import/open line.
files
Edit(replace_all: false, file_path: <work>/Subalgebras-sub-trans-iso.agda, old_string: open import Setoid.Subalgebras ≤-trans-≅′, new_string: open import Setoid.Subalgebras open _≅_ ≤-trans-≅′)
answered
The file <work>/Subalgebras-sub-trans-iso.agda has been updated successfully. (file state is current in your context — n…
the whole answer, as the model saw it (143 characters of text)
The file <work>/Subalgebras-sub-trans-iso.agda has been updated successfully. (file state is current in your context — no need to Read it back)
shell
Bash(command: agda --no-default-libraries --library-file <repo>/agda/libraries --library standard-library --library agda-dojang --library agda-algebras --safe -i . Subalgebras-sub-trans-iso.agda)
answeredno timing in the archive
Checking Subalgebras-sub-trans-iso (<work>/Subalgebras-sub-trans-iso.agda).
the whole answer, as the model saw it (75 characters of text)
Checking Subalgebras-sub-trans-iso (<work>/Subalgebras-sub-trans-iso.agda).
the model
The file now type-checks successfully with the exact judging command, confirming success.

The model’s words and its calls are quoted from transcript.jsonl; every answer below a call is the tool’s own, in full. The client billed 704 thinking tokens over the session; their text is not in the archive.

solvedthe judge, in outcome.json

Every gate passed, and the definition does not refer to the library’s own lemma for this statement, so the row counts as a solve.

Agda’s exit code on the file 0

statement preserved yes

last verdict taken from agda in the shell

the library’s own proof in view before the edit yes, the model read the file that holds it

the file the judge read, marked against the obligation it started as

 -- Subalgebras-sub-trans-iso.agda
 --
 -- File: data/benchmarks/agda-algebras-v0/obligations/Subalgebras-sub-trans-iso.agda
 --
 -- Benchmark obligation: algebras-subalgebras-sub-trans-iso
 -- Difficulty: non-obvious
 -- Source: Setoid.Subalgebras.Properties (agda-algebras)
 -- Import stratum: wholesale
 -- Strategy: pairing
 --
 module Subalgebras-sub-trans-iso where
 
 open import AgdaDojang.Debug
 
 open import Agda.Primitive   using ( Level )
 open import Data.Product     using ( _,_ ; proj₁ ; proj₂ )
 
 open import Overture              using ( Signature )
 open import Setoid.Algebras       using ( Algebra )
 open import Setoid.Functions
 open import Setoid.Homomorphisms
 open import Setoid.Subalgebras
 
+open _≅_
+
 ≤-trans-≅′ : {𝓞 𝓥 α ρᵃ β ρᵇ γ ρᶜ : Level} {𝑆 : Signature 𝓞 𝓥}
              {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ}
   →  𝑨 ≤ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≤ 𝑪
-≤-trans-≅′ p B≅C = {!!}
+≤-trans-≅′ (h , hinj) B≅C =
+  ⊙-hom h (to B≅C) , ⊙-injective (proj₁ h) (proj₁ (to B≅C)) hinj (≅toInjective B≅C)

reports/agent-bench/arm162-shell-1/subjects/algebras-subalgebras-sub-trans-iso/final/Subalgebras-sub-trans-iso.agda

≤-trans-≅′, server and shell

Server and shell. Given both, the model reads the library through the shell and takes its verdicts from check_file: the first says no and names what is out of scope, the second says yes.

model: Sonnet 5 (claude-sonnet-5)
instrument: server and shell
run: arm162-both-1 2026-09-21
server: the server of 2026-09-21 (fourteen tools, the libraries' sources readable on every arm)
client: 2.1.261 (Claude Code)
turns: 14
tool calls: 13 Read ×3, Bash ×6, Edit ×2, check_file ×2
wall clock: 46 s (indicative: subjects ran three at a time)
cost, list price: USD 0.19

the statement, as the obligation states it, with the proof removed

{𝓞 𝓥 α ρᵃ β ρᵇ γ ρᶜ : Level} {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ} →  𝑨 ≤ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≤ 𝑪

the session, 14 turns and 13 tool calls

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

files

Read(file_path: <work>/Subalgebras-sub-trans-iso.agda)

answered

1 -- Subalgebras-sub-trans-iso.agda

the whole answer, as the model saw it (963 characters of text)

1   -- Subalgebras-sub-trans-iso.agda
2   --
3   -- File: data/benchmarks/agda-algebras-v0/obligations/Subalgebras-sub-trans-iso.agda
4   --
5   -- Benchmark obligation: algebras-subalgebras-sub-trans-iso
6   -- Difficulty: non-obvious
7   -- Source: Setoid.Subalgebras.Properties (agda-algebras)
8   -- Import stratum: wholesale
9   -- Strategy: pairing
10  --
11  module Subalgebras-sub-trans-iso where
12  
13  open import AgdaDojang.Debug
14  
15  open import Agda.Primitive   using ( Level )
16  open import Data.Product     using ( _,_ ; proj₁ ; proj₂ )
17  
18  open import Overture              using ( Signature )
19  open import Setoid.Algebras       using ( Algebra )
20  open import Setoid.Functions
21  open import Setoid.Homomorphisms
22  open import Setoid.Subalgebras
23  
24  ≤-trans-≅′ : {𝓞 𝓥 α ρᵃ β ρᵇ γ ρᶜ : Level} {𝑆 : Signature 𝓞 𝓥}
25               {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ}
26    →  𝑨 ≤ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≤ 𝑪
27  ≤-trans-≅′ p B≅C = {!!}
28

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.
shell
Bash(command: grep -n "≤-trans-≅\|_≤_\|_≅_" <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/*.agda 2>/dev/null | head -80)
answered
(Bash completed with no output)
the whole answer, as the model saw it (31 characters of text)
(Bash completed with no output)
shell
Bash(command: find <nix>/agda-algebras-unstable-2026-09-07/src/Setoid -iname "*Subalgebra*")
answered
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras.lagda.md
the whole answer, as the model saw it (134 characters of text)
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras.lagda.md <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras
shell
Bash(command: ls <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/)
answered
Basic.lagda.md
the whole answer, as the model saw it (110 characters of text)
Basic.lagda.md CompleteLattice.lagda.md Properties.lagda.md Subdirect Subdirect.lagda.md Subuniverses.lagda.md

shell

Bash(command: grep -n "≤-trans-≅\|^_≤_\|_≤_ \|≅-refl\|module\|open import" <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md)

answered

3:title : "Setoid.Subalgebras.Properties module (The Agda Universal Algebra Library)"

the whole answer, as the model saw it (1,855 characters of text)

3:title : "Setoid.Subalgebras.Properties module (The Agda Universal Algebra Library)"
10:This is the [Setoid.Subalgebras.Properties][] module of the [Agda Universal Algebra Library][].
12:This module establishes the order-theoretic facts about the subalgebra relation
28:module Setoid.Subalgebras.Properties where
30:open import Agda.Primitive using () renaming ( Set to Type )
33:open import Data.Product              using ( _,_ )
34:open import Function                  using ( _∘_ )  renaming ( Func to _⟶_ )
35:open import Level                     using ( Level ; _⊔_ )
36:open import Relation.Binary           using ( Setoid )
37:open import Relation.Unary            using ( Pred ; _⊆_ )
43:open import Overture                  using  ( proj₁ ; proj₂ ; 𝓞 ; 𝓥 ; Signature ; 𝑆 )
44:open import Setoid.Algebras           using  ( Algebra ; Lift-Algˡ ; Lift-Algʳ
46:open import Setoid.Functions          using  ( id-is-injective ; IsInjective ; ⊙-injective )
47:open import Setoid.Homomorphisms      using  ( hom ; IsHom ; 𝒾𝒹 ; ⊙-hom ; _≅_
49:                                             ; ≅-sym ; ≅-refl ; ≅-trans
51:open import Setoid.Subalgebras.Basic  using  ( _≤_ ; _≥_ ; _≤c_ )
77:module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ}{𝑪 : Algebra {𝑆 = 𝑆} γ ρᶜ} where
81:  ≤-trans-≅ : 𝑨 ≤ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≤ 𝑪
82:  ≤-trans-≅ (h , hinj) B≅C =
89:module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ}{𝑪 : Algebra {𝑆 = 𝑆} γ ρᶜ} where
97:module _ {𝑆 : Signature 𝓞 𝓥} {α ρᵃ ρ : Level} where
103:  isEquivalence  ≤-preorder = record { refl = ≅-refl ; sym = ≅-sym ; trans = ≅-trans }
107:module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ}{𝑪 : Algebra {𝑆 = 𝑆} γ ρᶜ} where
169:module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ} where
188:module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ} where
214:module _

the model
Found the existing `≤-trans-≅` proof. Let's read it.

files

Read(file_path: <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md, offset: 70, limit: 40)

answered

70

the whole answer, as the model saw it (1,777 characters of text)

70 
71  ≥-refl : {𝑨 𝑩 : Algebra {𝑆 = 𝑆} α ρᵃ} → 𝑨 ≅ 𝑩 → 𝑨 ≥ 𝑩
72  ≥-refl = ≅→≤ ∘ ≅-sym
73  
74  ≤-reflexive : {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} → 𝑨 ≤ 𝑨
75  ≤-reflexive {𝑨 = 𝑨} = 𝒾𝒹 , id-is-injective {𝑨 = 𝔻[ 𝑨 ]}
76  
77  module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ}{𝑪 : Algebra {𝑆 = 𝑆} γ ρᶜ} where
78    ≤-trans : 𝑨 ≤ 𝑩 → 𝑩 ≤ 𝑪 → 𝑨 ≤ 𝑪
79    ≤-trans ( f , finj ) ( g , ginj ) = (⊙-hom f g) , ⊙-injective (proj₁ f) (proj₁ g) finj ginj
80  
81    ≤-trans-≅ : 𝑨 ≤ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≤ 𝑪
82    ≤-trans-≅ (h , hinj) B≅C =
83      ⊙-hom h (to B≅C) , ⊙-injective (proj₁ h) (proj₁ (to B≅C)) hinj (≅toInjective B≅C)
84  
85    ≅-trans-≤ : 𝑨 ≅ 𝑩 → 𝑩 ≤ 𝑪 → 𝑨 ≤ 𝑪
86    ≅-trans-≤ A≅B (h , hinj) =
87      ⊙-hom (to A≅B) h , ⊙-injective (proj₁ (to A≅B)) (proj₁ h) (≅toInjective A≅B) hinj
88  
89  module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ}{𝑪 : Algebra {𝑆 = 𝑆} γ ρᶜ} where
90    ≥-trans : 𝑨 ≥ 𝑩 → 𝑩 ≥ 𝑪 → 𝑨 ≥ 𝑪
91    ≥-trans A≥B B≥C = ≤-trans B≥C A≥B
92  
93  ≤→≤c→≤c : {𝑨 : Algebra {𝑆 = 𝑆} α α}{𝑩 : Algebra {𝑆 = 𝑆} α α}{𝒦 : Pred(Algebra {𝑆 = 𝑆} α α) (ov {𝑆 = 𝑆} α)}
94    → 𝑨 ≤ 𝑩 → 𝑩 ≤c 𝒦 → 𝑨 ≤c 𝒦
95  ≤→≤c→≤c A≤B sB = (proj₁ sB) , (proj₁ (proj₂ sB) , ≤-trans A≤B (proj₂ (proj₂ sB)))
96  
97  module _ {𝑆 : Signature 𝓞 𝓥} {α ρᵃ ρ : Level} where
98  
99    open RelStructs {a = ov {𝑆 = 𝑆} (α ⊔ ρᵃ)} {ℓ = 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρᵃ} (_≅_ {α = α}{ρᵃ = ρᵃ}{𝑆 = 𝑆})
100   open IsPreorder
101 
102   ≤-preorder : IsPreorder _≤_
103   isEquivalence  ≤-preorder = record { refl = ≅-refl ; sym = ≅-sym ; trans = ≅-trans }
104   reflexive      ≤-preorder = ≤-refl
105   trans          ≤-preorder A≤B B≤C = ≤-trans A≤B B≤C
106 
107 module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ}{𝑪 : Algebra {𝑆 = 𝑆} γ ρᶜ} where
108   A≥B×B≅C→A≥C : 𝑨 ≥ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≥ 𝑪
109   A≥B×B≅C→A≥C A≥B B≅C  = ≥-trans A≥B (≅→≥ B≅C)

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

shell

Bash(command: grep -n "_≤_\|_≥_" <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Basic.lagda.md | head -20)

answered

24:Our subalgebra relation `_≤_`{.AgdaFunction} is clearly reflexive and transitive,

the whole answer, as the model saw it (743 characters of text)

24:Our subalgebra relation `_≤_`{.AgdaFunction} is clearly reflexive and transitive,
27:about `_≤_`{.AgdaFunction} that this subtree establishes.
45:finite algebras `_≤_`{.AgdaFunction} is antisymmetric up to isomorphism, hence a
49:This module defines the subalgebra relation `_≤_`{.AgdaFunction} and the several
81:+  `_IsSubalgebraOf_`{.AgdaFunction}, with the infix alias `_≤_`{.AgdaFunction},
84:+  `_IsSupalgebraOf_`{.AgdaFunction}, aliased `_≥_`{.AgdaFunction}, is the
98:  _≥_   -- alias for supalgebra (aka overalgebra)
102:  _≤_   -- alias for subalgebra relation
181:      same symbol, `_≤_`{.AgdaFunction}.  The two do not collide, because the
186:      as `_≤_`{.AgdaFunction} only where `Sublattice`{.AgdaModule} is opened, as in

the model
Good, matches. Now fill the hole using the same pattern.
files
Edit(replace_all: false, file_path: <work>/Subalgebras-sub-trans-iso.agda, old_string: ≤-trans-≅′ p B≅C = {!!}, new_string: ≤-trans-≅′ (h , hinj) B≅C = ⊙-hom h (to B≅C) , ⊙-injective (proj₁ h) (proj₁ (to B≅C)) hinj (≅toInjective B≅C))
answered
The file <work>/Subalgebras-sub-trans-iso.agda has been updated successfully. (file state is current in your context — n…
the whole answer, as the model saw it (143 characters of text)
The file <work>/Subalgebras-sub-trans-iso.agda has been updated successfully. (file state is current in your context — no need to Read it back)

agda-mcp

check_file()

answered5.1 s

success: falseholesCount: 0diagnosticsTotal: 1verdict.exitCode: 42elapsedMs: 5060diagnostics: 1holes: 0

the whole answer, as the model saw it (2,245 characters of JSON)

{"checkedFromSource":true,"command":{"args":["-i","agda-dojang/agda","--library-file=agda/libraries","-l","agda-dojang","-l","standard-library","-l","agda-algebras","--safe","-i","<work>","<work>/Subalgebras-sub-trans-iso.agda"],"binary":"<nix>/agdaWithPackages-2.8.0/bin/agda","cwd":"<repo>"},"diagnostics":[{"code":"NotInScope","col":12,"file":"<work>/Subalgebras-sub-trans-iso.agda","involved":{"candidates":["_≅_.to","Setoid.Homomorphisms._≅_.to"]},"line":28,"message":"Not in scope:\n  to\n  at <work>/Subalgebras-sub-trans-iso.agda:28.12-14\n    (did you mean\n       '_≅_.to' or\n       'Setoid.Homomorphisms._≅_.to'?)\nwhen scope checking to","range":{"endCol":14,"endLine":28,"startCol":12,"startLine":28},"severity":"error"}],"diagnosticsTotal":1,"elapsedMs":5060,"holes":[],"holesCount":0,"project":{"includePaths":["agda-dojang/agda","<work>"],"librariesFile":"<repo>/agda/libraries","registeredLibraries":[{"includes":["agda"],"libFile":"<repo>/agda-dojang/agda-dojang.agda-lib","name":"agda-dojang","root":"<repo>/agda-dojang"},{"includes":["src"],"libFile":"<nix>/standard-library-2.3/standard-library.agda-lib","name":"standard-library-2.3","root":"<nix>/standard-library-2.3"},{"includes":["src"],"libFile":"<nix>/agda-algebras-unstable-2026-09-07/agda-algebras.agda-lib","name":"agda-algebras","root":"<nix>/agda-algebras-unstable-2026-09-07"}],"root":"<work>","rootSource":"server-config","selectedLibraries":["agda-dojang","standard-library","agda-algebras"]},"success":false,"timedOut":false,"verdict":{"equivalentTo":"equivalent-to: <nix>/agdaWithPackages-2.8.0/bin/agda -i agda-dojang/agda --library-file=agda/libraries -l agda-dojang -l standard-library -l agda-algebras --safe -i <work> <work>/Subalgebras-sub-trans-iso.agda","exitCode":42,"meaning":"success is true if and only if that command exited 0, so it means exactly what green means in a batch build. Unsolved metavariables, unsolved constraints, and open holes all make agda exit non-zero and so make success false; there is no interaction mode anywhere in this server. The verdict is read from the exit code alone — never from the diagnostics text — so a change in Agda's message format can empty the diagnostics list but cannot turn a failing build green."}}

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

shell

Bash(command: grep -n "record _≅_\|to \|from \|≅toInjective\|module.*≅" <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/*.lagda.md 2>/dev/null | grep -i "to\|≅" | head -40)

answered

<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Factor.lagda.md:14:`h`: there is a homomorphism `φ` fro…

the whole answer, as the model saw it (6,291 characters of text)

<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Factor.lagda.md:14:`h`: there is a homomorphism `φ` from the codomain of `h` to the codomain of `g`
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Factor.lagda.md:31:-- Imports from Agda and the Agda Standard Library -------------------------------------------------
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Factor.lagda.md:33:open import Function     renaming ( Func to _⟶_ )  using ( _∘_ ; _$_ )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Factor.lagda.md:40:-- Imports from the Agda Universal Algebra Library ------------------------------------------------
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Factor.lagda.md:72:  open Setoid 𝔻[ 𝑩 ]  using ()         renaming ( _≈_ to _≈₂_ )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Factor.lagda.md:73:  open Setoid 𝔻[ 𝑪 ]  using ( trans )  renaming ( _≈_ to _≈₃_ ; sym to sym₃ )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Factor.lagda.md:74:  open _⟶_            using ( cong )   renaming ( to to _⟨$⟩_ )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Factor.lagda.md:119:      open _⟶_ φ using () renaming (cong to φcong)
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Factor.lagda.md:157:      is obtained from `HomFactor`{.AgdaFunction}.
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:12:A **homomorphism** from `𝑨` to `𝑩` is a setoid function `h : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]`
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:17:Two things distinguish this from an ordinary type-based definition, where
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:21:    cannot fail to send equal arguments to equal results.
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:22:2.  Compatibility is asserted up to the equality *of the codomain*, not up to
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:25:    appeal to extensionality.
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:50:-- Imports from Agda and the Agda Standard Library ------------------------------
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:51:open import Agda.Primitive           using () renaming ( Set to Type )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:53:open import Function.Bundles         using () renaming ( Func to _⟶_ )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:58:-- Imports from the Agda Universal Algebra Library ---------------------------
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:75:setoid function `h` from the domain of `𝑨` to that of `𝑩`, together with a proof
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:79:`h` and a `compatible-map`{.AgdaFunction} proof never has to write the `Σ`-pair
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:84:  open _⟶_ {a = α}{ρᵃ}{β}{ρᵇ}{From = 𝔻[ 𝑨 ]}{To = 𝔻[ 𝑩 ]} renaming (to to _⟨$⟩_ )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:88:    where open Setoid 𝔻[ 𝑩 ] using() renaming ( _≈_ to _≈₂_ )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Basic.lagda.md:128:monomorphism into a subalgebra and an epimorphism into a homomorphic image.
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:13:both directions that are mutually inverse up to the setoid equalities of the two
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:18:`from∼to`{.AgdaField}, and derives from it that each direction is both injective
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:27:+  `≅toInjective`{.AgdaFunction}: the forward map of an isomorphism is injective;
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:31:+  `Lift-≅`{.AgdaFunction}: an algebra is isomorphic to each of its universe
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:44:-- Imports from Agda (builtin/primitive) and the Agda Standard Library ---------------------
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:45:open import Agda.Primitive              using () renaming ( Set to Type )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:47:open import Data.Unit.Polymorphic.Base  using ()      renaming ( ⊤ to 𝟙 ; tt to ∗ )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:49:open import Function                    using ()  renaming ( Func to _⟶_ )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:55:-- Imports from the Agda Universal Algebra Library -----------------------------------------
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:71:open _⟶_ using ( cong ) renaming ( to to _⟨$⟩_ )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:87:However, with four components, an equivalent record type is easier to work with.
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:91:  open Setoid 𝔻[ 𝑨 ] using ( sym ; trans ) renaming ( _≈_ to _≈₁_ )
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:92:  open Setoid 𝔻[ 𝑩 ] using () renaming ( _≈_ to _≈₂_ ; sym to sym₂ ; trans to trans₂)
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:94:  record _≅_ : Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ β ⊔ ρᵃ ⊔ ρᵇ ) where
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:97:      to : hom 𝑨 𝑩
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:98:      from : hom 𝑩 𝑨
<nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Homomorphisms/Isomorphisms.lagda.md:99:      to∼from : ∀ b → to .proj₁ ⟨$⟩ (from .proj₁ ⟨$⟩ b) ≈₂ b

thought
The model thought here, of unrecorded length. The archive keeps the block’s signature and not its text, so nothing is quoted.

files

Read(file_path: <nix>/agda-algebras-unstable-2026-09-07/src/Setoid/Subalgebras/Properties.lagda.md, offset: 40, limit: 30)

answered

40 import Relation.Binary.Reasoning.Setoid as SetoidReasoning

the whole answer, as the model saw it (1,390 characters of text)

40  import Relation.Binary.Reasoning.Setoid as SetoidReasoning
41  
42  -- Imports from the Agda Universal Algebra Library ----------------------------------
43  open import Overture                  using  ( proj₁ ; proj₂ ; 𝓞 ; 𝓥 ; Signature ; 𝑆 )
44  open import Setoid.Algebras           using  ( Algebra ; Lift-Algˡ ; Lift-Algʳ
45                                               ; Lift-Alg ; ov ; ⨅ ; 𝔻[_] )
46  open import Setoid.Functions          using  ( id-is-injective ; IsInjective ; ⊙-injective )
47  open import Setoid.Homomorphisms      using  ( hom ; IsHom ; 𝒾𝒹 ; ⊙-hom ; _≅_
48                                               ; ≅toInjective ; ≅fromInjective ; mkiso
49                                               ; ≅-sym ; ≅-refl ; ≅-trans
50                                               ; Lift-≅ˡ ; Lift-≅ ; Lift-≅ʳ)
51  open import Setoid.Subalgebras.Basic  using  ( _≤_ ; _≥_ ; _≤c_ )
52  
53  private variable α ρᵃ β ρᵇ γ ρᶜ ι : Level
54  ```
55  -->
56  
57  The subalgebra relation is a *preorder*, i.e., a reflexive, transitive binary relation.
58  
59  ```agda
60  open _≅_
61  
62  ≅→≤ : {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ} → 𝑨 ≅ 𝑩 → 𝑨 ≤ 𝑩
63  ≅→≤ φ = (to φ) , ≅toInjective φ
64  
65  ≅→≥ : {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra {𝑆 = 𝑆} β ρᵇ} → 𝑨 ≅ 𝑩 → 𝑨 ≥ 𝑩
66  ≅→≥ φ = (from φ) , ≅fromInjective φ
67  
68  ≤-refl : {𝑨 𝑩 : Algebra {𝑆 = 𝑆} α ρᵃ} → 𝑨 ≅ 𝑩 → 𝑨 ≤ 𝑩
69  ≤-refl = ≅→≤

the model
They have `open _≅_` at top level. I'll use `_≅_.to` directly instead of adding an open, to avoid extra top-level opens interfering (though allowed). Simplest: use qualified `_≅_.to`.
files
Edit(replace_all: false, file_path: <work>/Subalgebras-sub-trans-iso.agda, old_string: ≤-trans-≅′ (h , hinj) B≅C = ⊙-hom h (to B≅C) , ⊙-injective (proj₁ h) (proj₁ (to B≅C)) hinj (≅toInjective B≅C), new_string: ≤-trans-≅′ (h , hinj) B≅C = ⊙-hom h (_≅_.to B≅C) , ⊙-injective (proj₁ h) (proj₁ (_≅_.to B≅C)) hinj (≅toInjective B≅C))
answered
The file <work>/Subalgebras-sub-trans-iso.agda has been updated successfully. (file state is current in your context — n…
the whole answer, as the model saw it (143 characters of text)
The file <work>/Subalgebras-sub-trans-iso.agda has been updated successfully. (file state is current in your context — no need to Read it back)

agda-mcp

check_file()

answered6.0 s

success: trueholesCount: 0diagnosticsTotal: 0verdict.exitCode: 0elapsedMs: 5982diagnostics: 0holes: 0

the whole answer, as the model saw it (1,818 characters of JSON)

{"checkedFromSource":true,"command":{"args":["-i","agda-dojang/agda","--library-file=agda/libraries","-l","agda-dojang","-l","standard-library","-l","agda-algebras","--safe","-i","<work>","<work>/Subalgebras-sub-trans-iso.agda"],"binary":"<nix>/agdaWithPackages-2.8.0/bin/agda","cwd":"<repo>"},"diagnostics":[],"diagnosticsTotal":0,"elapsedMs":5982,"holes":[],"holesCount":0,"project":{"includePaths":["agda-dojang/agda","<work>"],"librariesFile":"<repo>/agda/libraries","registeredLibraries":[{"includes":["agda"],"libFile":"<repo>/agda-dojang/agda-dojang.agda-lib","name":"agda-dojang","root":"<repo>/agda-dojang"},{"includes":["src"],"libFile":"<nix>/standard-library-2.3/standard-library.agda-lib","name":"standard-library-2.3","root":"<nix>/standard-library-2.3"},{"includes":["src"],"libFile":"<nix>/agda-algebras-unstable-2026-09-07/agda-algebras.agda-lib","name":"agda-algebras","root":"<nix>/agda-algebras-unstable-2026-09-07"}],"root":"<work>","rootSource":"server-config","selectedLibraries":["agda-dojang","standard-library","agda-algebras"]},"success":true,"timedOut":false,"verdict":{"equivalentTo":"equivalent-to: <nix>/agdaWithPackages-2.8.0/bin/agda -i agda-dojang/agda --library-file=agda/libraries -l agda-dojang -l standard-library -l agda-algebras --safe -i <work> <work>/Subalgebras-sub-trans-iso.agda","exitCode":0,"meaning":"success is true if and only if that command exited 0, so it means exactly what green means in a batch build. Unsolved metavariables, unsolved constraints, and open holes all make agda exit non-zero and so make success false; there is no interaction mode anywhere in this server. The verdict is read from the exit code alone — never from the diagnostics text — so a change in Agda's message format can empty the diagnostics list but cannot turn a failing build green."}}

the model
The verdict on the final file is success (exit code 0, no diagnostics).

The model’s words and its calls are quoted from transcript.jsonl; every answer below a call is the tool’s own, in full. The client billed 496 thinking tokens over the session; their text is not in the archive.

solvedthe judge, in outcome.json

Every gate passed, and the definition does not refer to the library’s own lemma for this statement, so the row counts as a solve.

Agda’s exit code on the file 0

statement preserved yes

last verdict taken from check_file

the library’s own proof in view before the edit yes, the model read the file that holds it

the file the judge read, marked against the obligation it started as

 -- Subalgebras-sub-trans-iso.agda
 --
 -- File: data/benchmarks/agda-algebras-v0/obligations/Subalgebras-sub-trans-iso.agda
 --
 -- Benchmark obligation: algebras-subalgebras-sub-trans-iso
 -- Difficulty: non-obvious
 -- Source: Setoid.Subalgebras.Properties (agda-algebras)
 -- Import stratum: wholesale
 -- Strategy: pairing
 --
 module Subalgebras-sub-trans-iso where
 
 open import AgdaDojang.Debug
 
 open import Agda.Primitive   using ( Level )
 open import Data.Product     using ( _,_ ; proj₁ ; proj₂ )
 
 open import Overture              using ( Signature )
 open import Setoid.Algebras       using ( Algebra )
 open import Setoid.Functions
 open import Setoid.Homomorphisms
 open import Setoid.Subalgebras
 
 ≤-trans-≅′ : {𝓞 𝓥 α ρᵃ β ρᵇ γ ρᶜ : Level} {𝑆 : Signature 𝓞 𝓥}
              {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ}
   →  𝑨 ≤ 𝑩 → 𝑩 ≅ 𝑪 → 𝑨 ≤ 𝑪
-≤-trans-≅′ p B≅C = {!!}
+≤-trans-≅′ (h , hinj) B≅C =
+  ⊙-hom h (_≅_.to B≅C) , ⊙-injective (proj₁ h) (proj₁ (_≅_.to B≅C)) hinj (≅toInjective B≅C)

reports/agent-bench/arm162-both-1/subjects/algebras-subalgebras-sub-trans-iso/final/Subalgebras-sub-trans-iso.agda

Did the tools change the score?¶

On this benchmark, no. The readers this server is for already give the model a batch type-checker, so a verdict is not what the server adds. What it adds is information a batch check does not carry: the type of a name, the goal at a hole, what a module exports, what the library holds. The obligations here were mined from libraries that already contain their proofs, and a model that can read those sources into its context needs little of that information to score, so the score did not move. What moved is how the model worked and what a session cost, and the table records both. The early signs are in the sessions above, where questions stood in for trials.

55 obligations mined from the Agda standard library and agda-algebras, Sonnet 5, one row per instrument and server. Solved and restated are the archive’s judge’s columns; a restated row type-checks by calling the library’s own lemma and is never counted a solve.

instrument	server	solved	restated	lost to a gate	cost, list price	turns	run
shell only	the server of 2026-09-21	50	0	5	USD 2.88	308	arm162-shell-1
server only	the server of 2026-09-21	47	6	2	USD 5.28	342	arm162-mcp-1
server and shell	the server of 2026-09-21	51	2	2	USD 4.25	327	arm162-both-1
server only	the server of 2026-09-25	46	8	1	USD 4.63	359	arm184-mcp-1
server and shell	the server of 2026-09-25	49	2	4	USD 4.00	318	arm184-both-1
server only	the server of 2026-09-26	48	7	0	USD 3.83	345	arm-surface-mcp-1
server only	the server of 2026-09-26	45	8	2	USD 3.74	349	arm-surface-mcp-2
server and shell	the server of 2026-09-26	46	4	5	USD 3.55	318	arm-surface-both-1
server only, four tools	the server of 2026-09-26	52	1	2	USD 3.78	458	arm-verdict-mcp-1
server only, four tools	the server of 2026-09-26	53	2	0	USD 3.84	461	arm-verdict-mcp-2

The shell alone solved 50, inside the 45 to 53 of 55 the server arms solved: on these obligations the tools changed how the model worked, not what it solved.
Offered the server and a shell together, the model took 55 of 55 verdicts from check_file in arm162-both-1 and 55 of 55 verdicts from check_file in arm184-both-1 and 55 of 55 verdicts from check_file in arm-surface-both-1, and ran agda in the shell 0 times in arm162-both-1 and 0 times in arm184-both-1 and 0 times in arm-surface-both-1: the verdict is the tool it would not give up.
A sweep with the server cost more: USD 3.55 to USD 5.28 across the 9 arms that had it, against USD 2.88 with the shell alone in arm162-shell-1; the arms on the newest server, of 2026-09-26, cost USD 3.55 to USD 3.84. agda-native-air’s reading is that the tools’ descriptions, re-read on every turn, were part of the difference, and that cutting them closed that part and not the whole; the rest is output and turns.
Waiting on Agda was a small part of a session: 8 % to 11 % of its wall clock at the median, at most 45 %. The rest is the model’s own turns, which is where a faster server cannot help and a smaller one might.

What this does not show¶

That the server makes the model smarter. On these obligations every instrument scores about the same, and the table above is the whole of the evidence. The page is about what the server makes cheap, what it keeps expensive and why, and what a model does with the difference.
That the model found the proof unaided. In all three sessions the library's own proof of this lemma came into view before the model's edit, and the judge records that beside each verdict. The sessions show how each instrument is used, not a proof found from nothing. The one archived session on this row where that read was refused is Opus 5's on the first server, which built the proof from type queries and a probe; agda-native-air's own demo replays it, and it is linked below.
A comparison with no type-checker at all. That would measure the checker, which every reader here already grants, and not the server.
Anything about statements with no proof on disk. The score block lists every tier that has been run and committed; the one above was mined from libraries that already contain the answers. Whether the information the server offers matters when nothing on disk does is a separate measurement, and it will be reported the way this one is, with its run ids, whichever way it goes.

Go deeper¶

agda-native-air's demo replays five sessions from the same archive, Opus 5's on this lemma among them, and carries the full benchmark table; the archive itself is reports/agent-bench/, with every transcript, verdict and final file this page was built from.
ADR 0002 is the server's design record, with the field measurements the third clock quotes; ADR 0001 § 9 is the benchmark's, and reading the results says for every number in it what it is a win or a loss for.
The agent that never called the server is the story of why the verdict travels with the command it is equivalent to, and the typechecker as a reward signal is what the exit code is worth to a loop that trains or evaluates a model.
The field reports are the sessions in real developments, written up in both directions, where the whole-library check is the gate and the server's verdict is the instrument.