...

[helm.git] / matita / matita / lib / tutorial / chapter12.ma

diff --git a/matita/matita/lib/tutorial/chapter12.ma b/matita/matita/lib/tutorial/chapter12.ma
index 233b0bbba9d9a08274ee20ea4b0a96053ce5591d..47f8a971f76e7460457d2bc56d84fa8b807cc17e 100644 (file)
--- a/matita/matita/lib/tutorial/chapter12.ma
+++ b/matita/matita/lib/tutorial/chapter12.ma
@@ -446,7 +446,14 @@ qed.
  some other type T dependent over n the following equation should hold:
  f … (t … p x) = t … p (f … x) (i.e. transporting and applying f should commute
  because f should be insensitive too up to ≃ to the actual representation of the
- integral indexes). *) 
+ integral indexes).
+
+ Luckily enough, in practice types dependent overs setoids occur very rarely.
+ Most examples of dependent types are indexed over discrete objects, like
+ natural, integers and rationals, that admit an unique representation.
+ For continuity reasons, types dependent over real numbers can also be
+ represented as types dependent over a dense subset of the reals, like the
+ rational numbers. *)
 
 (****** Avoiding setoids *******)
 
@@ -474,4 +481,4 @@ qed.
     already satisfies for free all required equations
  4) normal forms are usually smaller than other forms. By sticking to normal
     forms both the memory consumption and the computational cost of operations
-    may be reduced. *)
\ No newline at end of file
+    may be reduced. *)