X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Ftutorial%2Fchapter12.ma;h=47f8a971f76e7460457d2bc56d84fa8b807cc17e;hb=bd1b3551dc0832f90c5d6389882bad89458b0692;hp=233b0bbba9d9a08274ee20ea4b0a96053ce5591d;hpb=bce3dca819b8f60c6a10b24f48c44b66e13ec376;p=helm.git

diff --git a/matita/matita/lib/tutorial/chapter12.ma b/matita/matita/lib/tutorial/chapter12.ma
index 233b0bbba..47f8a971f 100644
--- 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. *)