mod change (-x)

[helm.git] / helm / software / matita / contribs / assembly / compiler / sigma.ma

diff --git a/helm/software/matita/contribs/assembly/compiler/sigma.ma b/helm/software/matita/contribs/assembly/compiler/sigma.ma
old mode 100755 (executable)
new mode 100644 (file)
index b43e4bb..e9c234e
--- a/helm/software/matita/contribs/assembly/compiler/sigma.ma
+++ b/helm/software/matita/contribs/assembly/compiler/sigma.ma
@@ -39,23 +39,11 @@ notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
 
 notation "\ll term 19 a, break term 19 b \gg"
 with precedence 90 for @{'dependent_pair (λx:?.? x) $a $b}.
-interpretation "dependent pair" 'dependent_pair \eta.c a b = (sigma_intro _ c a b).
+interpretation "dependent pair" 'dependent_pair \eta.c a b = (sigma_intro ? c a b).
 
-interpretation "sigma" 'Sigma \eta.x = (sigma _ x).
+interpretation "sigma" 'Sigma \eta.x = (sigma ? x).
 
 definition sigmaFst ≝
 λT:Type.λf:T → Type.λs:sigma T f.match s with [ sigma_intro x _ ⇒ x ].
 definition sigmaSnd ≝
 λT:Type.λf:T → Type.λs:sigma T f.match s return λs.f (sigmaFst ?? s) with [ sigma_intro _ x ⇒ x ].
-
-(* tripla dipendente, suggerimento \SHcy *)
-
-inductive bisigma (A,B:Type) (P:A → B → Type) : Type ≝
-    bisigma_intro: ∀x:A.∀y:B.P x y → bisigma A B P.
-
-definition bisigmaFst ≝
-λT1,T2:Type.λf:T1 → T2 → Type.λs:bisigma T1 T2 f.match s with [ bisigma_intro x _ _ ⇒ x ].
-definition bisigmaSnd ≝
-λT1,T2:Type.λf:T1 → T2 → Type.λs:bisigma T1 T2 f.match s with [ bisigma_intro _ x _ ⇒ x ].
-definition bisigmaThd ≝
-λT1,T2:Type.λf:T1 → T2 → Type.λs:bisigma T1 T2 f.match s return λs.f (bisigmaFst ??? s) (bisigmaSnd ??? s) with [ bisigma_intro _ _ x ⇒ x ].