To me as a programmer, to write mathematical proofs that are mechanically checked by a computer feels empowering. To have these proofs as executable programs feels even more empowering. Therefore, our proofs have a computational aspect and vice-versa: our programs have a logical aspect. To be able to get an instant feedback while proving a theorem is amazing. With Agda, a dependently typed functional programming language, one can interactively write a proof by getting guidance from Agda as to what is left to prove. Furthermore, Agda checks the correctness of proofs by following a set of rules. Unlike with pen and paper proofs, proofs in Agda are much more rigorous because there is no room for hand-waving nor unwarranted claims for something to be trivial. An uninformed mathematician will likely find this comparison to Agda hard to believe.

A few years ago when I got interested in type theory, I had an ongoing conversation with a friend of mine that was interested in the topic too. We talked a lot about programming languages and type theory. One interesting thing that I realized at the time was that the product of the unit type and a type A is in a way equivalent to that same type A. To be more precise, it is isomorphic. Isomorphism is an equivalence relation, hence it is reflexive, symmetric and transitive. In the conversation the two of us had, I kept on insisting on this equivalence without being explicit that I meant isomorphism and at first he didn’t understand how these two could possibly be the same.

Now that I’ve been working through a book titled Programming Language Foundations in Agda by Wadler and Kokke, I am happy there is a succinct way not only to express this isomorphism in Agda, but to prove it. That unit is the left identity to product up to isomorphism can be named ⊤-identityˡ and expressed as follows (as given in the book):

import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl) open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩) open import Data.Unit using (⊤; tt) infix 0 _≃_ record _≃_ (A B : Set) : Set where field to : A → B from : B → A from∘to : ∀ (x : A) → from (to x) ≡ x to∘from : ∀ (y : B) → to (from y) ≡ y open _≃_ ⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A ⊤-identityˡ = record { to = λ{ ⟨ tt , x ⟩ → x } ; from = λ{ x → ⟨ tt , x ⟩ } ; from∘to = λ{ ⟨ tt , x ⟩ → refl } ; to∘from = λ{ x → refl } }

I kept the definition of isomorphism from the book, although Agda’s standard library defines it too, where it is known as _↔_; the rest are imported from the standard library.

The right identity can be proved in a similar matter, but as pointed out in the book, it can also be proved via the left identity and commutativity of product up to isomorphism:

⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A ⊤-identityʳ {A} = ≃-begin (A × ⊤) ≃⟨ ×-comm ⟩ (⊤ × A) ≃⟨ ⊤-identityˡ ⟩ A ≃-∎

The ×-comm theorem is formally stated as:

×-comm : ∀ {A B : Set} → A × B ≃ B × A

Its proof and remaining definitions, theorems and proofs are given at the end of this article for completeness.

A weak form of isomorphism is embedding, a relation that is reflexive, transitive and antisymmetric. The Programming Language Foundations in Agda book describes embedding this way: “While an isomorphism shows that two types are in one-to-one correspondence, an embedding shows that the first type is included in the second; or, equivalently, that there is a many-to-one correspondence between the second type and the first.”

This is how embedding is formally defined in the book:

infix 0 _≲_ record _≲_ (A B : Set) : Set where field to : A → B from : B → A from∘to : ∀ (x : A) → from (to x) ≡ x

I am interested in embedded domain specific languages and their realization via freer monads. It is a topic that I started looking at fairly recently. In particular, I got to reading a paper Freer Monads, More Extensible Effects by Oleg Kiselyov and Hiromi Ishii and a Haskell package that implements the freer monad: freer-simple. A very important concept is natural transformation, which is a way of translating one language into another. I am expecting that here natural transformations will not be isomorphisms, but probably embeddings. The reason is that when translating from a less powerful language into a more powerful language there will be strictly fewer concepts to translate (e.g., from a DSL console language to the IO monad) than in the translation the other way around. Unfortunately, I won’t be able to find this out in Haskell, but luckily there is Agda. My plan is to implement the freer monad in Agda and to prove or disprove natural transformations as embeddings.

import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; cong) open Eq.≡-Reasoning open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) open import Data.Unit using (⊤; tt) open import Function using (_∘_) infix 0 _≃_ record _≃_ (A B : Set) : Set where field to : A → B from : B → A from∘to : ∀ (x : A) → from (to x) ≡ x to∘from : ∀ (y : B) → to (from y) ≡ y open _≃_ ⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A ⊤-identityˡ = record { to = λ{ ⟨ tt , x ⟩ → x } ; from = λ{ x → ⟨ tt , x ⟩ } ; from∘to = λ{ ⟨ tt , x ⟩ → refl } ; to∘from = λ{ x → refl } } ≃-refl : ∀ {A : Set} ----- → A ≃ A ≃-refl = record { to = λ{x → x} ; from = λ{y → y} ; from∘to = λ{x → refl} ; to∘from = λ{y → refl} } ≃-trans : ∀ {A B C : Set} → A ≃ B → B ≃ C ----- → A ≃ C ≃-trans A≃B B≃C = record { to = to B≃C ∘ to A≃B ; from = from A≃B ∘ from B≃C ; from∘to = λ{x → begin (from A≃B ∘ from B≃C) ((to B≃C ∘ to A≃B) x) ≡⟨⟩ from A≃B (from B≃C (to B≃C (to A≃B x))) ≡⟨ cong (from A≃B) (from∘to B≃C (to A≃B x)) ⟩ from A≃B (to A≃B x) ≡⟨ from∘to A≃B x ⟩ x ∎} ; to∘from = λ{y → begin (to B≃C ∘ to A≃B) ((from A≃B ∘ from B≃C) y) ≡⟨⟩ to B≃C (to A≃B (from A≃B (from B≃C y))) ≡⟨ cong (to B≃C) (to∘from A≃B (from B≃C y)) ⟩ to B≃C (from B≃C y) ≡⟨ to∘from B≃C y ⟩ y ∎} } module ≃-Reasoning where infix 1 ≃-begin_ infixr 2 _≃⟨_⟩_ infix 3 _≃-∎ ≃-begin_ : ∀ {A B : Set} → A ≃ B ----- → A ≃ B ≃-begin A≃B = A≃B _≃⟨_⟩_ : ∀ (A : Set) {B C : Set} → A ≃ B → B ≃ C ----- → A ≃ C A ≃⟨ A≃B ⟩ B≃C = ≃-trans A≃B B≃C _≃-∎ : ∀ (A : Set) ----- → A ≃ A A ≃-∎ = ≃-refl open ≃-Reasoning ×-comm : ∀ {A B : Set} → A × B ≃ B × A ×-comm = record { to = λ{ ⟨ x , y ⟩ → ⟨ y , x ⟩ } ; from = λ{ ⟨ y , x ⟩ → ⟨ x , y ⟩ } ; from∘to = λ{ ⟨ x , y ⟩ → refl } ; to∘from = λ{ ⟨ y , x ⟩ → refl } } ⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A ⊤-identityʳ {A} = ≃-begin (A × ⊤) ≃⟨ ×-comm ⟩ (⊤ × A) ≃⟨ ⊤-identityˡ ⟩ A ≃-∎

“While an isomorphism shows that two types are in one-to-one correspondence, an embedding shows that the first type is included in the second; or, equivalently, that there is a many-to-one correspondence between the second type and the first.” — I don’t understand why if A is included in the B, then B is many-to-one relation with A. How to build intuition about that?

I believe this would be a good example. Take A to have two values, e.g., A = {Red, Blue} and B to be the set of natural numbers. Then take the f : A -> B function to be given with f(Red) = 0 and f(Blue) = 1. Next, take g : B -> A to be defined as g(0) = Red and g(n) = Blue for any n > 0. Here you have an embedding A ≲ B with to = f and from = g. All natural numbers but 0 map to Blue via g. For any n > 0, you have f(g(n)) = 1, which shows this is not an isomorphism. Hopefully this answers it.