Permalink
Browse files

Minor edit.

  • Loading branch information...
larrytheliquid committed Jul 14, 2012
1 parent b57f304 commit 257779135b8b5606e0e622794719b3047d146343
Showing with 1 addition and 1 deletion.
  1. +1 −1 posts/finite-isomorphic-types.md
@@ -310,7 +310,7 @@ After doing a little bit of surveying I've found some more serious attempts at c
## Adieu
I hope to have at least wet your appetite to the fun that can be had with constructively definable isomorphisms between types. Even though we have only dealt with a finite universe, when `Σ`, `Π`, and something like `FinW` are added I think it becomes a fairly interesting universe to play in. The denotational semantics as a family of types indexed by the naturals also seems like a simple and modular way to discover, and _simply_ prove things about, finite isomorphic types. I think that this implicit style relying on canonicity is more elegant than the explicit approach of a separate proof object (and at the very least a more pragmatic way to get simpler proofs).
I hope to have at least whet your appetite to the fun that can be had with constructively definable isomorphisms between types. Even though we have only dealt with a finite universe, when `Σ`, `Π`, and something like `FinW` are added I think it becomes a fairly interesting universe to play in. The denotational semantics as a family of types indexed by the naturals also seems like a simple and modular way to discover, and _simply_ prove things about, finite isomorphic types. I think that this implicit style relying on canonicity is more elegant than the explicit approach of a separate proof object (and at the very least a more pragmatic way to get simpler proofs).
----------------------------------------------------------------------

0 comments on commit 2577791

Please sign in to comment.