michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fixed left inverse in Isomorphism

Browse source
This commit is contained in:
Philip Wadler 2019-01-22 11:58:24 +00:00
parent d53a239a39
commit 472c0b8565
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/plfa/Isomorphism.lagda
View file

@ -149,8 +149,8 @@ Let's unpack the definition. An isomorphism between sets `A` and `B` consists
of four things: of four things:
+ A function `to` from `A` to `B`, + A function `to` from `A` to `B`,
+ A function `from` from `B` back to `A`, + A function `from` from `B` back to `A`,
+ Evidence `from∘to` asserting that `from` is a *right-identity* for `to`, + Evidence `from∘to` asserting that `from` is a *left-inverse* for `to`,
+ Evidence `to∘from` asserting that `to` is a *left-identity* for `from`. + Evidence `to∘from` asserting that `from` is a *right-inverse* for `to`.
In particular, the third asserts that `from ∘ to` is the identity, and In particular, the third asserts that `from ∘ to` is the identity, and
the fourth that `to ∘ from` is the identity, hence the names. the fourth that `to ∘ from` is the identity, hence the names.
The declaration `open _≃_` makes available the names `to`, `from`, The declaration `open _≃_` makes available the names `to`, `from`,
@ -216,7 +216,7 @@ and `from` to be the identity function:
In the above, `to` and `from` are both bound to identity functions, In the above, `to` and `from` are both bound to identity functions,
and `from∘to` and `to∘from` are both bound to functions that discard and `from∘to` and `to∘from` are both bound to functions that discard
their argument and return `refl`. In this case, `refl` alone is an their argument and return `refl`. In this case, `refl` alone is an
adequate proof since for the left inverse, `to (from x)` adequate proof since for the left inverse, `from (to x)`
simplifies to `x`, and similarly for the right inverse. simplifies to `x`, and similarly for the right inverse.
To show isomorphism is symmetric, we simply swap the roles of `to` To show isomorphism is symmetric, we simply swap the roles of `to`
@ -326,8 +326,8 @@ record _≲_ (A B : Set) : Set where
open _≲_ open _≲_
\end{code} \end{code}
It is the same as an isomorphism, save that it lacks the `to∘from` field. It is the same as an isomorphism, save that it lacks the `to∘from` field.
Hence, we know that `from` is right-inverse to `to`, but not that `to` Hence, we know that `from` is left-inverse to `to`, but not that `from`
is left-inverse to `from`. is right-inverse to `to`.
Embedding is reflexive and transitive, but not symmetric. The proofs Embedding is reflexive and transitive, but not symmetric. The proofs
are cut down versions of the similar proofs for isomorphism: are cut down versions of the similar proofs for isomorphism: