From 674990de8344d66c67fb8e306edef5b19170af8a Mon Sep 17 00:00:00 2001 From: Peter Thiemann Date: Mon, 1 Jun 2026 12:13:30 +0200 Subject: [PATCH 1/3] new instance; link fixed --- web/TableOfContents.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/web/TableOfContents.md b/web/TableOfContents.md index 5e3bcf7d2..13360e197 100644 --- a/web/TableOfContents.md +++ b/web/TableOfContents.md @@ -44,8 +44,10 @@ $endfor$ ### 2026 * [Jeremy Siek, Indiana University][IU-2026] + * [Peter Thiemann, Albert-Ludwigs University][Freiburg-2026] [IU-2026]: https://jsiek.github.io/PLFA-Spring-2026/ +[Freiburg-2026]: https://proglang.github.io/teaching/26ss/eopl.html ### 2025 * [Peter Thiemann, Albert-Ludwigs University][Freiburg-2025] From 00832906e9b0a37715826e3fb11d18a571926e54 Mon Sep 17 00:00:00 2001 From: Peter Thiemann Date: Thu, 4 Jun 2026 17:33:44 +0200 Subject: [PATCH 2/3] =?UTF-8?q?alternative=20proof=20for=20=E2=89=B2-antis?= =?UTF-8?q?ym?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/plfa/part1/Isomorphism.lagda.md | 52 +++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/src/plfa/part1/Isomorphism.lagda.md b/src/plfa/part1/Isomorphism.lagda.md index 39545c835..cca394a40 100644 --- a/src/plfa/part1/Isomorphism.lagda.md +++ b/src/plfa/part1/Isomorphism.lagda.md @@ -425,6 +425,58 @@ last combines the left inverse of `B ≲ A` with the equivalences of the `to` and `from` components from the two embeddings to obtain the right inverse of the isomorphism. +The previous proof can also be shortened by doing more work in the +patterns on the left-hand side. If the two proofs that the embedding +functions correspond are both matched against `refl`, then Agda records +that the corresponding functions are the same: + +```agda +≲-antisym′ : ∀ {A B : Set} + → (A≲B : A ≲ B) + → (B≲A : B ≲ A) + → (to A≲B ≡ from B≲A) + → (from A≲B ≡ to B≲A) + ------------------- + → A ≃ B +≲-antisym′ A≲B B≲A refl refl = + record + { to = to A≲B + ; from = from A≲B + ; from∘to = from∘to A≲B + ; to∘from = from∘to B≲A + } +``` + +After matching the third parameter, called `to≡from` above, against +`refl`, Agda knows that `to A≲B` and `from B≲A` are the same function. +After matching the fourth parameter, called `from≡to` above, against +`refl`, Agda knows that `from A≲B` and `to B≲A` are the same function. +Hence the type of `from∘to B≲A`, + + ∀ (y : B) → from B≲A (to B≲A y) ≡ y + +is the same as the type required for `to∘from`, + + ∀ (y : B) → to A≲B (from A≲B y) ≡ y. + +One subtlety is why Agda accepts these `refl` patterns at all. The +equalities compare projections from two records, rather than variables +written directly on the left-hand side. Agda silently η-expands record +values. This property is called η-equality for records: a record is +determined by its fields. A value `A≲B` is definitionally the same as +the record obtained by projecting out all its fields and putting them +back together. For an embedding, this means `A≲B` is the same as + + record + { to = to A≲B + ; from = from A≲B + ; from∘to = from∘to A≲B + } + +and similarly for `B≲A`. This η-expansion lets pattern matching on +`refl` refine the corresponding record fields, which is why the shorter +proof can replace the whole equational derivation by `from∘to B≲A`. + # Equational reasoning for embedding We can also support tabular reasoning for embedding, From f94c2a1e3f723d1d46365a10b36a2f06e5f09c5b Mon Sep 17 00:00:00 2001 From: Peter Thiemann Date: Fri, 5 Jun 2026 20:53:42 +0200 Subject: [PATCH 3/3] rewritten as requested by @wadler --- src/plfa/part1/Isomorphism.lagda.md | 92 +++++++++++------------------ 1 file changed, 34 insertions(+), 58 deletions(-) diff --git a/src/plfa/part1/Isomorphism.lagda.md b/src/plfa/part1/Isomorphism.lagda.md index cca394a40..99f80522c 100644 --- a/src/plfa/part1/Isomorphism.lagda.md +++ b/src/plfa/part1/Isomorphism.lagda.md @@ -392,7 +392,8 @@ are cut down versions of the similar proofs for isomorphism: It is also easy to see that if two types embed in each other, and the embedding functions correspond, then they are isomorphic. This is a -weak form of anti-symmetry: +weak form of anti-symmetry. The proof does some of the work by +matching the evidence that the functions correspond against `refl`: ```agda ≲-antisym : ∀ {A B : Set} @@ -402,43 +403,7 @@ weak form of anti-symmetry: → (from A≲B ≡ to B≲A) ------------------- → A ≃ B -≲-antisym A≲B B≲A to≡from from≡to = - record - { to = to A≲B - ; from = from A≲B - ; from∘to = from∘to A≲B - ; to∘from = λ{y → - begin - to A≲B (from A≲B y) - ≡⟨ cong (to A≲B) (cong-app from≡to y) ⟩ - to A≲B (to B≲A y) - ≡⟨ cong-app to≡from (to B≲A y) ⟩ - from B≲A (to B≲A y) - ≡⟨ from∘to B≲A y ⟩ - y - ∎} - } -``` - -The first three components are copied from the embedding, while the -last combines the left inverse of `B ≲ A` with the equivalences of -the `to` and `from` components from the two embeddings to obtain -the right inverse of the isomorphism. - -The previous proof can also be shortened by doing more work in the -patterns on the left-hand side. If the two proofs that the embedding -functions correspond are both matched against `refl`, then Agda records -that the corresponding functions are the same: - -```agda -≲-antisym′ : ∀ {A B : Set} - → (A≲B : A ≲ B) - → (B≲A : B ≲ A) - → (to A≲B ≡ from B≲A) - → (from A≲B ≡ to B≲A) - ------------------- - → A ≃ B -≲-antisym′ A≲B B≲A refl refl = +≲-antisym A≲B B≲A to≡from@refl from≡to@refl = record { to = to A≲B ; from = from A≲B @@ -447,35 +412,46 @@ that the corresponding functions are the same: } ``` -After matching the third parameter, called `to≡from` above, against -`refl`, Agda knows that `to A≲B` and `from B≲A` are the same function. -After matching the fourth parameter, called `from≡to` above, against -`refl`, Agda knows that `from A≲B` and `to B≲A` are the same function. -Hence the type of `from∘to B≲A`, - - ∀ (y : B) → from B≲A (to B≲A y) ≡ y - -is the same as the type required for `to∘from`, - - ∀ (y : B) → to A≲B (from A≲B y) ≡ y. +The first three components are copied from the embedding `A≲B`. For +the last component, matching `to≡from` against `refl` tells Agda that +`to A≲B` and `from B≲A` are the same function, while matching +`from≡to` against `refl` tells Agda that `from A≲B` and `to B≲A` are +the same function. Hence `from∘to B≲A` has the required type. One subtlety is why Agda accepts these `refl` patterns at all. The equalities compare projections from two records, rather than variables written directly on the left-hand side. Agda silently η-expands record values. This property is called η-equality for records: a record is -determined by its fields. A value `A≲B` is definitionally the same as -the record obtained by projecting out all its fields and putting them -back together. For an embedding, this means `A≲B` is the same as +determined by its fields. A record value is definitionally equal to the +record obtained by projecting out all its fields and putting them back +together. Thus, when checking the left-hand side, Agda may view the two +embeddings as record - { to = to A≲B - ; from = from A≲B - ; from∘to = from∘to A≲B + { to = f + ; from = g + ; from∘to = p } -and similarly for `B≲A`. This η-expansion lets pattern matching on -`refl` refine the corresponding record fields, which is why the shorter -proof can replace the whole equational derivation by `from∘to B≲A`. +and + + record + { to = h + ; from = k + ; from∘to = q + } + +where `f` is `to A≲B`, `g` is `from A≲B`, `h` is `to B≲A`, and `k` is +`from B≲A`. After this expansion, the equality arguments have types +`f ≡ k` and `g ≡ h`, so matching them against `refl` identifies +`f` with `k`, and `g` with `h`. It is not that η-expanding `A≲B` +computes `to A≲B` to something new; rather, η-expansion lets Agda +expose the fields of record variables while solving the pattern match. +Under these identifications, `from∘to B≲A` has type + + ∀ (y : B) → to A≲B (from A≲B y) ≡ y + +which is exactly the type required for `to∘from`. # Equational reasoning for embedding