X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=3c0ba7090406c43aef3f0cbd8df79d2143efd902;hb=89e21dbecca75a5320f50ecb53a39699f8ace8f1;hp=dcc7e9a81a86a15834228419c50ffdf9bf2b837b;hpb=7fd4f2f66fb8fe010bbd2bfe1f6b542c2da6c83f;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index dcc7e9a81..3c0ba7090 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -240,7 +240,7 @@ reaching the end of the formalization, but we had to assume the proof
 of the extensionality of the `U_x` construction (while there is no
 need to assume the same property for `F_x`!). 
 
-The current version of the formaliztion uses `Id`. 
+The current version of the formalization uses `Id`. 
 
 The standard library and the `include` command
 ----------------------------------------------
@@ -923,11 +923,11 @@ Thus the statement `Im[d(a,i)] ⊆ V` unfolds to
 
 That, up to rewriting with the equation defining `x`, is what we mean.
 Since we decided to use `Id` the rewriting always work (the elimination
-prnciple for `Id` is Leibnitz's equality, that is quantified over
+principle for `Id` is Leibnitz's equality, that is quantified over
 the context. 
 
 The problem that arises if we decide to make `S` a setoid is that 
-`V` has to be extensional w.r.t. the equality of `S` (i.e. the charactestic
+`V` has to be extensional w.r.t. the equality of `S` (i.e. the characteristic
 functional proposition has to quotient its input with a relation bigger
 than the one of `S`.
 
@@ -1013,7 +1013,7 @@ there is still some work to do.
 D[retr-3]
 To use the equation defining `b` we have to eliminate `H`. Unfolding
 definitions in `x` tell us there is still something to do. The `nrewrite`
-tactic is a shorcut for the elimination principle of the equlity.
+tactic is a shortcut for the elimination principle of the equality.
 It accepts an additional argument `<` or `>` to rewrite left-to-right
 or right-to-left.