update in standard library

[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..07a5fd19f04586d76a2bfa627ede33b789a69c9d 100644 (file)
--- a/matita/matita/lib/tutorial/chapter12.ma
+++ b/matita/matita/lib/tutorial/chapter12.ma
@@ -16,6 +16,7 @@ include "basics/relations.ma".
 include "basics/types.ma".
 include "arithmetics/nat.ma".
 include "hints_declaration.ma".
+include "basics/core_notation/invert_1.ma".
 
 (******************* Quotienting in type theory **********************)
 
@@ -50,7 +51,7 @@ record setoid : Type[1] ≝ {
 (* Note that carrier has been defined as a coercion so that when S is a setoid
  we can write x:S in place of x: carrier S. *)
 
-(* We use the notation ≃ for the equality over setoid elements. *)
+(* We use the notation ≃ for the equality on setoid elements. *)
 notation "hvbox(n break ≃ m)"
   non associative with precedence 45
 for @{ 'congruent $n $m }.
@@ -72,7 +73,7 @@ definition Z: setoid ≝
  @(injective_plus_r … H4)
 qed.
 
-(* The two integers (0,1) and (1,2) are equal up to â\89\9d, written
+(* The two integers (0,1) and (1,2) are equal up to â\89\83, written
    〈0,1〉 ≃ 〈1,2〉. Unfolding the notation, that corresponds to
    eqrel ? (eq_setoid ?) 〈0,1〉 〈1,2〉 which means that the two
    pairs are to be compare according to the equivalence relation
@@ -140,7 +141,7 @@ record morphism (I,O: setoid) : Type[0] ≝ {
  ; mor_proper: proper … mor_carr
  }.
 
-(* We introduce a notation for morhism using a long arrow. *)
+(* We introduce a notation for morphism using the symbols of an arrow followed by a dot. *)
 notation "hvbox(I break ⤞ O)"
   right associative with precedence 20
 for @{ 'morphism $I $O }.
@@ -150,7 +151,7 @@ interpretation "morphism" 'morphism I O = (morphism I O).
 (* By declaring mor_carr as a coercion it is possible to write f x for
    mor_carr f x in order to apply a morphism f to an argument. *)
 
-(* Example: oppositive of an integer number. We first implement the function
+(* Example: opposite of an integer number. We first implement the function
   over Z and then lift it to a morphism. The proof obligation is to prove
   properness. *)
 definition opp: Z → Z ≝ λc.〈\snd c,\fst c〉.
@@ -178,7 +179,7 @@ unification hint 0 ≔ x:Z ;
 
 (* Example: we state that opp is proper and we will prove it without using
  automation and without referring to OPP. When we apply the universal mor_proper
- property of morhisms, Matita looks for the morphism associate to opp x and
+ property of morphisms, Matita looks for the morphism associate to opp x and
  finds it thanks to the second unification hint above, completing the proof. *)
 example ex2: ∀x,y. x ≃ y → opp x ≃ opp y.
  #x #y #EQ @mor_proper @EQ
@@ -446,7 +447,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 +482,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. *)