From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 5 Jan 2018 19:20:09 +0000 (+0100)
Subject: beginning of minimalist foundation from a student of Milly
X-Git-Tag: make_still_working~381
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=b3aa03ebf904d8c7290aa44b4ce80bf3f976fb2e

beginning of minimalist foundation from a student of Milly
---

diff --git a/matita/matita/contribs/mf/de.ma b/matita/matita/contribs/mf/de.ma
new file mode 100644
index 000000000..47b33dde8
--- /dev/null
+++ b/matita/matita/contribs/mf/de.ma
@@ -0,0 +1,70 @@
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+
+definition eDe: est → est.
+ #I %
+ [ @(De I)
+ | @De_rect_Type1
+   [ #z @(z = c_unit …)
+   | #i * [ 2: #i' @(i ≃ i') | 3,4: #_ #_ ] @falsum
+   | #F1 #F2 #H1 #H2 * [ 3: #F1' #F2' @(H1 F1' ∧ H2 F2') | 2: #_ | 4: #_ #_ ] @falsum
+   | #F1 #F2 #H1 #H2 * [ 4: #F1' #F2' @(H1 F1' ∧ H2 F2') | 2: #_ | 3: #_ #_ ] @falsum
+   ]
+ | %
+   [ @De_rect_CProp0
+     [ %
+     | @rfl
+     | #F1 #F2 #H1 #H2 % [ @H1 | @H2 ]
+     | #F1 #F2 #H1 #H2 % [ @H1 | @H2 ]
+     ]
+   | @De_rect_CProp0
+     [ * [ #_ % | #i #abs @(De_clash_unit_ev I i abs)
+         | #F1 #F2 #abs @(De_clash_unit_times I F1 F2 abs)
+         | #F1 #F2 #abs @(De_clash_unit_plus I F1 F2 abs) ]
+     | #i * [ @falsum_rect_CProp0 | #i' @sym | 3,4: #F1' #F2' #abs @abs ]
+     | #F1 #F2 #H1 #H2 * [ @falsum_rect_CProp0 | #i' #abs @abs 
+                         | #F1' #F2' * #K1 #K2 % [ @H1 @K1 | @H2 @K2 ]
+                         | #F1' #F2' #abs @abs ]
+     | #F1 #F2 #H1 #H2 * [ @falsum_rect_CProp0 | #i' #abs @abs
+                         | #F1' #F2' #abs @abs
+                         | #F1' #F2' * #K1 #K2 % [ @H1 @K1 | @H2 @K2 ] ]
+     ]
+   | @De_rect_CProp0
+     [ * [ #F'' #_ #h @h
+         | #i' #F'' #abs @(falsum_rect_CProp0 … (De_clash_unit_ev I i' abs))
+         | #F1' #F2' #F'' #abs @(falsum_rect_CProp0 … (De_clash_unit_times I F1' F2' abs))
+         | #F1' #F2' #F'' #abs @(falsum_rect_CProp0 … (De_clash_unit_plus I F1' F2' abs))
+         ]
+     | #i * [ #F'' @falsum_rect_CProp0
+            | #i' * [ #_ #abs @abs
+                    | #i'' @tra
+                    | 3,4: #F1'' #F2'' #_ #abs @abs
+                    ]
+            | 3,4: #F1' #F2' #F'' @falsum_rect_CProp0
+            ]
+     | #F1 #F2 #H1 #H2 * [ #F'' @falsum_rect_CProp0
+                         | #i' #F'' @falsum_rect_CProp0
+                         | #F1' #F2' * [ #_ #abs @abs
+                                       | #i'' #_ #abs @abs
+                                       | #F1'' #F2'' * #H11 #H12 * #H21 #H22 %
+                                         [ @(H1 F1' F1'' H11 H21) | @(H2 F2' F2'' H12 H22) ]
+                                       | #F1'' #F2'' #_ #abs @abs
+                                       ]
+                         | #F1' #F2' #F'' @falsum_rect_CProp0
+                         ]
+     | #F1 #F2 #H1 #H2 * [ #F'' @falsum_rect_CProp0
+                         | #i' #F'' @falsum_rect_CProp0
+                         | #F1' #F2' #F'' @falsum_rect_CProp0
+                         | #F1' #F2' * [ #_ #abs @abs
+                                       | #i'' #_ #abs @abs
+                                       | #F1'' #F2'' #_ #abs @abs
+                                       | #F1'' #F2'' * #H11 #H12 * #H21 #H22 %
+                                         [ @(H1 F1' F1'' H11 H21) | @(H2 F2' F2'' H12 H22) ]
+                                       ]
+                         ]
+     ]
+   ]
+ ]
+qed.
+
diff --git a/matita/matita/contribs/mf/empty.ma b/matita/matita/contribs/mf/empty.ma
new file mode 100644
index 000000000..a402ef217
--- /dev/null
+++ b/matita/matita/contribs/mf/empty.ma
@@ -0,0 +1,23 @@
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+include "pisigma.ma".
+include "pisigma2.ma".
+
+definition en0: est ≝
+ mk_est n0 (λz,z'. z = z') ?.
+ % #x [ % | #y * % | #y #z #h * @h ]
+qed.
+
+definition en0_rect_Type0: ∀Q: edst en0. epi en0 Q ≝ 
+ λQ. 〈n0_rect_Type0 …, ?〉.
+ @(n0_rect_CProp0).
+qed.
+
+definition en0_rect_Type1: ∀Q: edcl (est_into_ecl en0). ePi … Q ≝ 
+ λQ. 〈n0_rect_Type1 …, ?〉.
+ @(n0_rect_CProp1).
+qed.
+
+definition edn0: ∀I: est. edst I ≝ λI. constant_edst I en0.
+
diff --git a/matita/matita/contribs/mf/interface.ma b/matita/matita/contribs/mf/interface.ma
new file mode 100644
index 000000000..4f9f0c011
--- /dev/null
+++ b/matita/matita/contribs/mf/interface.ma
@@ -0,0 +1,27 @@
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+
+include "pisigma2.ma".
+include "power_one.ma".
+include "power.ma".
+
+include "pisigma.ma".
+include "empty.ma".
+include "singleton.ma".
+include "list.ma".
+include "plus.ma".
+include "de.ma".
+
+definition eFalsum: eprop ≝ Falsum.
+definition eId: ∀B: ecl. Sup B → Sup B → eprop ≝ Eq.
+definition eImplies: eprop → eprop → eprop ≝ Implies.
+definition eConj: eprop → eprop → eprop ≝ Conj.
+definition eDisj: eprop → eprop → eprop ≝ Disj.
+
+definition efalsum: eprops ≝ falsum.
+definition eid: ∀B: est. sup B → sup B → eprops ≝ eq.
+definition eimplies: eprops → eprops → eprops ≝ implies.
+definition econj: eprops → eprops → eprops ≝ conj.
+definition edisj: eprops → eprops → eprops ≝ disj.
+
diff --git a/matita/matita/contribs/mf/list.ma b/matita/matita/contribs/mf/list.ma
new file mode 100644
index 000000000..122002c67
--- /dev/null
+++ b/matita/matita/contribs/mf/list.ma
@@ -0,0 +1,197 @@
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+include "pisigma.ma".
+
+definition proj1: ∀C: est. ∀r: list (Σx. Σy. x ≃ y). list C ≝
+ λC. lift_to_list … (π1 …).
+
+definition proj2: ∀C: est. ∀r: list (Σx. Σy. x ≃ y). list C ≝
+ λC. lift_to_list … (λz: Σx. Σy. x ≃ y. π1 (π2 z)).
+
+definition elist: est → est ≝
+ λC. mk_est
+ (list C)
+ (λz,z'. ∃l: list (Σx. Σy. x ≃ y). (proj1 … l = z) ∧ (proj2 … l = z'))
+ ?.
+ % [ @list_rect_CProp0 
+     [ %{ϵ} % %
+     | #l #c * #r * #h1 #h2
+       %{⌈r, 〈c, 〈c, ıc〉〉⌉}
+       % [ @(rewrite_l … ⌈proj1 … r, c⌉
+             (λz. z = ⌈l, c⌉)
+             (rewrite_l … (proj1 … r) (λz. ⌈proj1 … r, c⌉ = ⌈z, c⌉) (reflexivity …) … h1)
+             … (reflexivity …))
+         | @(rewrite_l … ⌈proj2 … r, c⌉
+             (λz. z = ⌈l, c⌉)
+             (rewrite_l … (proj2 … r) (λz. ⌈proj2 … r, c⌉ = ⌈z, c⌉) (reflexivity …) … h2)
+             … (reflexivity …))
+         ]
+     ]
+   | @list_rect_CProp0 
+     [ *
+       [ //
+       | #l2' #c * *
+         [ * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs))
+         | #r #s * normalize #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
+         ]
+       ]
+     | #l1' #c1 #h *
+       [ * *
+         [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
+         | #r #s * #_ normalize #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
+         ]
+       | #l2' #c2 * *
+         [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
+         | #r #s * #h1 #h2
+           cut (∃l. (proj1 … l = l2') ∧ (proj2 … l = l1'))
+           [ @(h l2') %{r} % [ @(injectivity_cons1 … h1) | @(injectivity_cons1 … h2) ]
+           | * #r' * #h1' #h2' %{⌈r', 〈c2, 〈c1, ?〉〉⌉}
+             [ cut (π1 (π2 s) = c2)
+               [ cut (⌈proj2 … r, π1 (π2 s)⌉ = ⌈l2', c2⌉)
+                 [ @(rewrite_l … (proj2 … ⌈r, s⌉)
+                     (λz. z = ⌈l2', c2⌉) h2 … (reflexivity …))
+                 | @injectivity_cons2
+                 ]
+               | #k2 cut (π1 s = c1)
+                 [ cut (⌈proj1 … r, sig1 … s⌉ = ⌈l1', c1⌉)
+                   [ @(rewrite_l … (proj1 … ⌈r, s⌉)
+                       (λz. z = ⌈l1', c1⌉) h1 … (reflexivity …))
+                   | @injectivity_cons2
+                   ]
+                 | #k1 cut (π1 (π2 s) ≃ π1 s)
+                   [ @((π2 (π2 s))⁻¹)
+                   | #e cut (c2 ≃ π1 s)
+                     [ @(rewrite_l … (π1 (π2 s)) (λz. z ≃ π1 s) e … k2)
+                     | #e' @(rewrite_l … (π1 s) (λz. c2 ≃ z) e' … k1)
+                     ]
+                   ]
+                 ]
+               ]
+             | 
+               % [ @(rewrite_l … (proj1 … r') (λz. ⌈proj1 … r', c2⌉ = ⌈z, c2⌉) (reflexivity …) … h1')
+                 | @(rewrite_l … (proj2 … r') (λz. ⌈proj2 … r', c1⌉ = ⌈z, c1⌉) (reflexivity …) … h2')
+                 ]
+             ]
+           ]
+         ]
+       ]
+     ]
+   | @list_rect_CProp0 
+     [ *
+       [ *
+         [ //
+         | #l3' #c3 #_ //
+         ]
+       | #l2 #c2 *
+         [ #_ #_ %{ϵ} % %
+         | #l3' #c3 * *
+           [ * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs))
+           | #r1' #s1 * #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
+           ]
+         ]
+       ]
+     | #l1' #c1 #h *
+       [ *
+         [ * | #l3' #c3 * ] *
+         [ 1,3: * #abs @(falsum_rect_CProp0 … (list_clash … abs))
+         | 2,4: #r' #s * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
+         ]
+       | #l2' #c2 *
+         [ #_ * *
+           [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
+           | #r' #s * #_ #abs @(falsum_rect_CProp0 … (list_clash … abs⁻¹))
+           ]
+         | #l3' #c3 * *
+           [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
+           | #r1 #s1 * #h1 #h2 * *
+             [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
+             | #r2 #s2 * #h3 #h4
+               cut (⌈proj1 … r1, π1 s1⌉ = ⌈l1', c1⌉)
+               [ @(rewrite_l … (proj1 … ⌈r1, s1⌉)
+                   (λz. z = ⌈l1', c1⌉) h1 … (reflexivity …))
+               | -h1 #h1
+                 cut (⌈proj2 … r1, π1 (π2 s1)⌉ = ⌈l2', c2⌉)
+                 [ @(rewrite_l … (proj2 … ⌈r1, s1⌉)
+                     (λz. z = ⌈l2', c2⌉) h2 … (reflexivity …))
+                 | -h2 #h2
+                   cut (⌈proj1 … r2, π1 s2⌉ = ⌈l2', c2⌉)
+                   [ @(rewrite_l … (proj1 … ⌈r2, s2⌉)
+                       (λz. z = ⌈l2', c2⌉) h3 … (reflexivity …))
+                   | -h3 #h3
+                     cut (⌈proj2 … r2, π1 (π2 s2)⌉ = ⌈l3', c3⌉)
+                     [ @(rewrite_l … (proj2 … ⌈r2, s2⌉)
+                         (λz. z = ⌈l3', c3⌉) h4 … (reflexivity …))
+                     | -h4 #h4
+                       cut (∃l. (proj1 … l = l1') ∧ (proj2 … l = l3'))
+                       [ @(h l2' l3')
+                         [ %{r1} @(mk_conj … (injectivity_cons1 … h1) (injectivity_cons1 … h2))
+                         | %{r2} @(mk_conj … (injectivity_cons1 … h3) (injectivity_cons1 … h4))
+                         ]
+                       | * #r * #e1 #e2 %{⌈r, 〈c1, 〈c3, ?〉〉⌉}
+                         [ @(tra …
+                             (rewrite_l … (π1 s1) (λz. z ≃ c2)
+                              (rewrite_l … (π1 (π2 s1)) (λz. π1 s1 ≃ z) (π2 (π2 s1))
+                                … (injectivity_cons2 … h2))
+                              … (injectivity_cons2 … h1))
+                             (rewrite_l … (π1 (π2 s2)) (λz. c2 ≃ z)
+                               (rewrite_l … (π1 s2) (λz. z ≃ π1 (π2 s2)) (π2 (π2 s2))
+                                … (injectivity_cons2 … h3))
+                              … (injectivity_cons2 … h4)))
+                         | %
+                           [ @(rewrite_l … (proj1 … r) (λz. ⌈proj1 … r, c1⌉ = ⌈z, c1⌉) (reflexivity …) … e1)
+                           | @(rewrite_l … (proj2 … r) (λz. ⌈proj2 … r, c3⌉ = ⌈z, c3⌉) (reflexivity …) … e2)
+                           ]
+                         ]
+                       ]
+                     ]
+                   ]
+                 ]
+               ]
+             ]
+           ]
+         ]
+       ]
+     ]
+   ]
+qed.
+
+definition eepsilon: ∀C: est. elist C ≝ epsilon.
+
+definition econs: ∀C: est. eto (elist C) (eto C (elist C)) ≝
+ λC. 〈λl. 〈cons … l, ?〉, ?〉.
+ [ #c1 #c2 #d
+   cut (subst C (constant_edst C (elist C)) c1 c2 d ⌈l, c1⌉ = ⌈l, c1⌉)
+   [ %
+   | #h @(rewrite_l (list (sup C)) ⌈l, c1⌉ (λz. eq (elist C) z ⌈l, c2⌉) ?
+          (subst C (constant_edst C (elist C)) c1 c2 d ⌈l, c1⌉) h)
+     @(list_rect_CProp0 … l)
+     [ %{⌈ϵ, 〈c1, 〈c2, d〉〉⌉} % %
+     | #l' #c * *
+       [ * #abs @(falsum_rect_CProp0 … (list_clash … abs))
+       | #r' #s * #h1 #h2 %{⌈⌈r', 〈c, 〈c, ıc〉〉⌉, 〈c1, 〈c2, d〉〉⌉} %
+         [ change with (⌈⌈proj1 … , ?⌉, ?⌉) in ⊢ (??%?);
+           cut (proj1 … r' = l')
+           [ @(injectivity_cons1 … h1)
+           | #h @(rewrite_l ????? h) @reflexivity
+           ]
+         | @(rewrite_l … ⌈⌈proj2 … r', c⌉, c2⌉ (λz. z = ⌈⌈l', c⌉, c2⌉) ?
+             (proj2 … ⌈⌈r', 〈c, 〈c, ıc〉〉⌉, 〈c1, 〈c2, d〉〉⌉) (reflexivity …))
+           cut (proj2 … r' = l')
+           [ @(injectivity_cons1 …
+               (rewrite_l … (proj2 … ⌈r', s⌉) (λz. ⌈proj2 … r', sig1 … (sig2 … s)⌉ = z)
+                (reflexivity …) ⌈l', c2⌉ h2))
+           | #h @(rewrite_l … l' (λz. ⌈⌈z, c⌉, c2⌉ = ⌈⌈l', c⌉, c2⌉) (reflexivity …)
+                  (proj2 C r') (symmetry … h))
+           ]
+         ]
+       ]
+     ]
+   ]
+ | #l1 #l2 * #r * #h1 #h2 #c %{⌈r, 〈c, 〈c, ıc〉〉⌉} %
+   [ @(rewrite_l … l1 (λz. ⌈z, c⌉ = ⌈l1, c⌉) (reflexivity …) (proj1 … r) (symmetry … h1))
+   | @(rewrite_l … l2 (λz. ⌈z, c⌉ = ⌈l2, c⌉) (reflexivity …) (proj2 … r) (symmetry … h2))
+   ]
+ ]
+qed.
+
diff --git a/matita/matita/contribs/mf/mTT.ma b/matita/matita/contribs/mf/mTT.ma
new file mode 100644
index 000000000..7bcc7ce62
--- /dev/null
+++ b/matita/matita/contribs/mf/mTT.ma
@@ -0,0 +1,274 @@
+(* (C) 2014 Luca Bressan *)
+
+include "notations.ma".
+
+universe constraint Type[0] < Type[1].
+universe constraint Type[1] < Type[2].
+
+notation "'cl'" with precedence 90 for @{ Type[1] }.
+notation "'st'" with precedence 90 for @{ Type[0] }.
+notation "'prop'" with precedence 90 for @{ CProp[1] }.
+notation "'props'" with precedence 90 for @{ CProp[0] }.
+
+record Sigma (B: cl) (C: B → cl) : cl ≝
+ { Sig1: B
+ ; Sig2: C Sig1
+ }.
+interpretation "Strong Indexed Sum" 'sigma x = (Sigma ? x).
+interpretation "Strong Indexed Sum constructor" 'mk_sigma x y = (mk_Sigma ?? x y).
+interpretation "First projection of Strong Indexed Sum" 'sig1 x = (Sig1 ?? x).
+interpretation "Second projection of Strong Indexed Sum" 'sig2 x = (Sig2 ?? x).
+
+definition Times: cl → cl → cl ≝
+ λB,C. Sigma B (λ_. C).
+interpretation "Binary collection product" 'times B C = (Times B C).
+
+inductive n0: st ≝ .
+
+inductive n1: st ≝ 
+ star: n1.
+interpretation "Element of the singleton" 'star = star.
+
+record sigma (B: st) (C : B → st) : st ≝
+ { sig1: B
+ ; sig2: C sig1
+ }.
+interpretation "Strong Indexed Sum set" 'sigma x = (sigma ? x).
+interpretation "Strong Indexed Sum set constructor" 'mk_sigma x y = (mk_sigma ?? x y).
+interpretation "First projection of Strong Indexed Sum set" 'sig1 x = (sig1 ?? x).
+interpretation "Second projection of Strong Indexed Sum set" 'sig2 x = (sig2 ?? x).
+
+definition times: st → st → st ≝
+ λB,C. sigma B (λ_. C).
+interpretation "Binary set product" 'times B C = (times B C).
+
+inductive list (C: st) : st (*CSC: Type[0]*) ≝ 
+   epsilon: list C
+ | cons: list C → C → list C.
+interpretation "Empty list" 'epsilon = (epsilon ?).
+interpretation "List constructor" 'cons l c = (cons ? l c).
+
+inductive plus (B: st) (C: st) : st ≝ 
+   inl: B → plus B C
+ | inr: C → plus B C.
+interpretation "Disjoint Sum set" 'plus B C = (plus B C).  
+
+inductive Falsum: prop ≝ .
+interpretation "Falsum" 'falsum = Falsum.
+
+inductive Disj (B: prop) (C: prop) : prop ≝ 
+   lOr: B → Disj B C
+ | rOr: C → Disj B C.
+interpretation "Disjunction" 'disj B C = (Disj B C).
+
+record Conj (B: prop) (C: prop) : prop ≝ 
+ { Conj1: B
+ ; Conj2: C
+ }.
+interpretation "Conjunction" 'conj B C = (Conj B C).
+
+definition Implies: prop → prop → prop ≝
+ λB,C: prop. B → C.
+interpretation "Implication" 'implies B C = (Implies B C).
+
+record Exists (B: cl) (C: B → prop) : prop ≝ 
+ { Ex1: B
+ ; Ex2: C Ex1
+ }.
+interpretation "Existential quantification" 'exists x = (Exists ? x).
+interpretation "Existential quantification constructor" 'mk_exists x y = (mk_Exists ?? x y).
+
+definition Forall: ∀B: cl. (B → prop) → prop ≝ λB,C. ∀b: B. C b.
+
+inductive Id (A: cl) (a: A) : A → prop ≝
+ Reflexivity: Id A a a.
+interpretation "Propositional Equality" 'id a b = (Id ? a b).
+interpretation "Reflexivity in Extensional Collections" 'rfl x = (Reflexivity ? x).
+
+definition Verum: prop ≝ Implies Falsum Falsum.
+interpretation "Verum" 'verum = Verum.
+
+inductive falsum: props ≝ .
+interpretation "Small Falsum" 'falsum = falsum.
+
+inductive disj (B: props) (C: props) : props ≝ 
+   lor: B → disj B C
+ | ror: C → disj B C.
+interpretation "Small Disjunction" 'disj B C = (disj B C).
+
+record conj (B: props) (C: props) : props ≝ 
+ { conj1: B
+ ; conj2: C
+ }.
+interpretation "Small Conjunction" 'conj B C = (conj B C).
+
+definition implies: props → props → props ≝
+ λB,C. B → C.
+interpretation "Small Implication" 'implies B C = (implies B C).
+
+record exists (B: st) (C: B → props) : props ≝ 
+ { exs1: B
+ ; exs2: C exs1
+ }.
+interpretation "Small Existential quantification" 'exists x = (exists ? x).
+interpretation "Small Existential quantification constructor" 'mk_exists x y = (mk_exists ?? x y).
+
+definition forall: ∀B: st. (B → props) → props ≝ λB,C. ∀b: B. C b.
+
+inductive id (A: st) (a: A) : A → props ≝
+ reflexivity: id A a a.
+interpretation "Small Propositional Equality" 'id a b = (id ? a b).
+interpretation "Reflexivity in Extensional Sets" 'rfl x = (reflexivity ? x).
+
+definition verum: props ≝ implies falsum falsum.
+interpretation "Verum" 'verum = verum.
+
+definition fun_to_props: st → cl ≝ λB. B → props.
+
+lemma Symmetry: ∀A: cl. ∀x,x': A. x = x' → x' = x.
+ #A #x #x' * %
+qed.
+interpretation "Symmetry in Intensional Collections" 'sym d = (Symmetry ??? d).
+
+lemma Transitivity: ∀A: cl. ∀x,x',x'': A. x = x' → x' = x'' → x = x''.
+ #A #x #x' #x'' * * %
+qed.
+interpretation "Transitivity in Intensional Collections" 'tra d = (Transitivity ???? d).
+
+lemma rewrite_l: ∀A: st. ∀x: A. ∀P: A → props. P x → ∀y: A. x = y → P y.
+ #A #x #P #h #y * @h
+qed.
+
+notation "hvbox(> h)" 
+ non associative with precedence 45
+ for @{ 'rewrite_l $h }.
+interpretation "Rewrite left" 'rewrite_l h = (rewrite_l ????? h).
+
+lemma symmetry: ∀A: st. ∀x,x': A. x = x' → x' = x.
+ #A #x #x' * %
+qed.
+interpretation "Symmetry in Intensional Sets" 'sym d = (symmetry ??? d).
+
+notation "hvbox(< h)" 
+ non associative with precedence 45
+ for @{ 'rewrite_r $h }.
+interpretation "Rewrite right" 'rewrite_r h = (rewrite_l ????? (symmetry ??? h)).
+
+lemma transitivity: ∀A: st. ∀x,x',x'': A. x = x' → x' = x'' → x = x''.
+ #A #x #x' #x'' * * %
+qed.
+interpretation "Transitivity in Intensional Sets" 'tra d = (transitivity ???? d).
+
+definition lift_to_list: ∀A,A': st. (A → A') → list A → list A' ≝ 
+ λA,A',f. list_rect_Type0 … (λ_. list A') ϵ (λl,x,l'. ⌈l', f x⌉).
+
+definition proj_l: ∀B,C: st. B → plus B C → B ≝ 
+ λB,C,b'. plus_rect_Type0 B C (λ_. B) (λb. b) (λ_. b').
+
+definition proj_r: ∀B,C: st. C → plus B C → C ≝ 
+ λB,C,c'. plus_rect_Type0 B C (λ_. C) (λ_. c') (λc. c).
+
+lemma injectivity_inl: ∀B,C: st. ∀x,x'. inl B C x = inl B C x' → x = x'.
+ #B #C #x #x'
+ @(rewrite_l … (inl … x) (λz. proj_l … x (inl … x) = proj_l … x z)
+   (ı(proj_l … x (inl … x))) (inl … x'))
+qed.
+
+lemma injectivity_inr: ∀B,C: st. ∀y,y'. inr B C y = inr B C y' → y = y'.
+ #B #C #y #y'
+ @(rewrite_l … (inr … y) (λz. proj_r … y (inr … y) = proj_r … y z)
+   (ı(proj_r … y (inr … y))) (inr … y'))
+qed.
+
+lemma injectivity_cons1: ∀C: st. ∀l,l': list C. ∀c,c': C. ⌈l, c⌉ = ⌈l', c'⌉ → l = l'.
+ #C #l1 #l2 #c1 #c2
+ @(rewrite_l … ⌈l1, c1⌉
+   (list_rect_Type1 … (λ_. props) ⊥ (λl,c,h. l1 = l))
+   (ı…) ⌈l2, c2⌉)
+qed.
+
+lemma injectivity_cons2: ∀C: st. ∀l,l': list C. ∀c,c': C. ⌈l, c⌉ = ⌈l', c'⌉ → c = c'.
+ #C #l1 #l2 #c1 #c2
+ @(rewrite_l … ⌈l1, c1⌉
+   (list_rect_Type1 … (λ_. props) ⊥ (λl,c,h. c1 = c))
+   (ı…) ⌈l2, c2⌉)
+qed.
+
+lemma plus_clash: ∀B,C: st. ∀b: B. ∀c: C. inl … b = inr … c → ⊥.
+ #B #C #b #c #h
+ @(rewrite_l … (inl … b) (plus_rect_Type1 … (λ_. props) (λ_. ⊤) (λ_. ⊥))
+   (λx. x) … h)
+qed.
+
+lemma list_clash: ∀C: st. ∀l: list C. ∀c: C. ϵ = ⌈l, c⌉ → ⊥.
+ #C #l #c #h
+ @(rewrite_l … ϵ (list_rect_Type1 … (λ_. props) ⊤ (λ_,_,_. ⊥))
+   (λx. x) … h)
+qed.
+
+definition nat: st ≝ list n1.
+definition zero: nat ≝ ϵ.
+definition succ: nat → nat ≝ λn. cons … n ⋆.
+definition nat_rect_Type0: ∀Q: nat → st. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
+ #Q #h0 #hi @list_rect_Type0 [ @h0 | #n @n1_rect_Type0 @(hi n) ]
+qed.
+definition nat_rect_Type1: ∀Q: nat → cl. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
+ #Q #h0 #hi @list_rect_Type1 [ @h0 | #n @n1_rect_Type1 @(hi n) ]
+qed.
+definition nat_rect_CProp0: ∀Q: nat → props. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
+ #Q #h0 #hi @list_rect_CProp0 [ @h0 | #n @n1_rect_CProp0 @(hi n) ]
+qed.
+definition nat_rect_CProp1: ∀Q: nat → prop. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
+ #Q #h0 #hi @list_rect_CProp1 [ @h0 | #n @n1_rect_CProp1 @(hi n) ]
+qed.
+
+inductive De (I: st) : st ≝
+ | c_unit: De I
+ | c_ev: I → De I
+ | c_times: De I → De I → De I
+ | c_plus: De I → De I → De I.
+
+definition int: ∀I: st. De I → (I → st) → st.
+ #I @De_rect_Type1
+ [ #_ @n1
+ | #i #X @(X i)
+ | #L #R #intL #intR #X @((intL X)×(intR X))
+ | #L #R #intL #intR #X @((intL X)+(intR X))
+ ]
+qed.
+
+definition napply: nat → (st → st) → st → st.
+ @nat_rect_Type1
+ [ #F #X @X
+ | #_ #F' #F #X @(F' F X)
+ ]
+qed.
+
+definition mu: ∀I: st. (I → De I) → I → st.
+ #I #F #i @(Σn: nat. napply n (λX: st. int I (F i) (λ_. X)) n0)
+qed.
+
+definition is_c_unit: ∀I: st. ∀F: De I. props.
+ #I * [ @verum | #_ @falsum | 3,4: #_ #_ @falsum ]
+qed.
+
+lemma De_clash_unit_ev: ∀I: st. ∀i: I. c_ev I i = c_unit I → falsum.
+ #I #i #h
+ @(rewrite_l (De I) (c_unit I) (is_c_unit I) (λx. x) (c_ev I i) h⁻¹)
+qed.
+lemma De_clash_unit_times: ∀I: st. ∀F,G: De I. c_times I F G = c_unit I → falsum.
+ #I #F #G #h
+ @(rewrite_l (De I) (c_unit I) (is_c_unit I) (λx. x) (c_times I F G) h⁻¹)
+qed.
+lemma De_clash_unit_plus: ∀I: st. ∀F,G: De I. c_plus I F G = c_unit I → falsum.
+ #I #F #G #h
+ @(rewrite_l (De I) (c_unit I) (is_c_unit I) (λx. x) (c_plus I F G) h⁻¹)
+qed.
+
+inductive mu_ (I: st) (F: I → De I) : I → De I → st ≝
+   fold_unit: ∀i: I. mu_ I F i (c_unit I)
+ | fold_ev: ∀i,i': I. mu_ I F i' (F i') → mu_ I F i (c_ev I i')
+ | fold_times: ∀i: I. ∀G1,G2: De I. mu_ I F i G1 → mu_ I F i G2 → mu_ I F i (c_times I G1 G2)
+ | fold_plusL: ∀i: I. ∀G1,G2: De I. mu_ I F i G1 → mu_ I F i (c_plus I G1 G2)
+ | fold_plusR: ∀i: I. ∀G1,G2: De I. mu_ I F i G2 → mu_ I F i (c_plus I G1 G2).
+
diff --git a/matita/matita/contribs/mf/model.ma b/matita/matita/contribs/mf/model.ma
new file mode 100644
index 000000000..4cc7e45de
--- /dev/null
+++ b/matita/matita/contribs/mf/model.ma
@@ -0,0 +1,190 @@
+(* (C) 2014 Luca Bressan *)
+
+include "mTT.ma".
+
+record is_Equiv (Sup: cl) (Eq: Sup → Sup → prop) : prop ≝
+ { Rfl_: ∀x. Eq x x
+ ; Sym_: ∀x,x'. Eq x x' → Eq x' x
+ ; Tra_: ∀x,x',x''. Eq x x' → Eq x' x'' → Eq x x''
+ }.
+
+record ecl: Type[2] ≝ 
+ { Sup:> cl
+ ; Eq: Sup → Sup → prop
+ ; is_ecl: is_Equiv Sup Eq
+ }.
+interpretation "Equality in Extensional Collections" 'eq a b = (Eq ? a b).
+
+definition Rfl: ∀B: ecl. ∀x: B. x ≃ x ≝
+ λB. Rfl_ … (is_ecl B).
+interpretation "Reflexivity in Extensional Collections" 'rfl x = (Rfl ? x).
+
+definition Sym: ∀B: ecl. ∀x,x': B. x ≃ x' → x' ≃ x ≝
+ λB. Sym_ … (is_ecl B).
+interpretation "Symmetry in Extensional Collections" 'sym d = (Sym ??? d).
+
+definition Tra: ∀B: ecl. ∀x,x',x'': B. x ≃ x' → x' ≃ x'' → x ≃ x'' ≝
+ λB. Tra_ … (is_ecl B).
+interpretation "Transitivity in Extensional Collections" 'tra d d' = (Tra ???? d d').
+
+record is_Subst (A: ecl)
+                (dSup: A → ecl)
+                (Subst: ∀x1,x2: A. x1 ≃ x2 → dSup x1 → dSup x2) : prop ≝
+ { Pres_eq_:   ∀x1,x2: A. ∀d: x1 ≃ x2. ∀y,y': dSup x1.
+                y ≃ y' → Subst … d y ≃ Subst … d y'
+ ; Not_dep_:   ∀x1,x2: A. ∀d,d': x1 ≃ x2. ∀y: dSup x1.
+                Subst … d y ≃ Subst … d' y
+ ; Pres_id_:   ∀x: A. ∀y: dSup x.
+                Subst … (ı x) y ≃ y
+ ; Clos_comp_: ∀x1,x2,x3: A. ∀y: dSup x1. ∀d: x1 ≃ x2. ∀d': x2 ≃ x3.
+                Subst … d' (Subst … d y) ≃ Subst … (d•d') y
+ }.
+
+record edcl (A: ecl) : Type[2] ≝ 
+ { dSup:1> Sup A → ecl
+ ; Subst: ∀x1,x2: Sup A. x1 ≃ x2 → Sup (dSup x1) → Sup (dSup x2)
+ ; is_edcl: is_Subst A dSup Subst
+ }.
+interpretation "Substitution morphisms for Extensional Collections"
+ 'subst d y = (Subst ???? d y).
+
+definition Pres_eq: ∀B: ecl. ∀C: edcl B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y,y': C x1.
+                     y ≃ y' → y∘d ≃ y'∘d ≝
+ λB,C. Pres_eq_ … (is_edcl … C).
+definition Not_dep: ∀B: ecl. ∀C: edcl B. ∀x1,x2: B. ∀d,d': x1 ≃ x2. ∀y: C x1.
+                     y∘d ≃ y∘d' ≝
+ λB,C. Not_dep_ … (is_edcl … C).
+definition Pres_id: ∀B: ecl. ∀C: edcl B. ∀x: B. ∀y: C x.
+                     y∘(ıx) ≃ y ≝
+ λB,C. Pres_id_ … (is_edcl … C).
+definition Clos_comp: ∀B: ecl. ∀C: edcl B. ∀x1,x2,x3: B. ∀y: C x1. ∀d: x1 ≃ x2. ∀d': x2 ≃ x3.
+                       y∘d∘d' ≃ y∘d•d' ≝
+ λB,C. Clos_comp_ … (is_edcl … C).
+
+definition constant_edcl: ∀A: ecl. ecl → edcl A ≝
+ λA,Y. mk_edcl … (λ_. Y) (λx1,x2,d,y. y) ?.
+ % [ #x1 #x2 #d #y #y' #h @h
+   | #x1 #x2 #_ #_ #y @(ıy)
+   | #_ #y @(ıy)
+   | #x1 #x2 #x3 #y #_ #_ @(ıy)
+   ]
+qed.
+
+lemma inverse_Subst: ∀B: ecl. ∀C: edcl B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y: C x2.
+ y∘d⁻¹∘d ≃ y.
+ #B #C #x1 #x2 #d #y
+ @(Tra … (y∘d⁻¹∘d) (y∘d⁻¹•d) y)
+ [ @Clos_comp
+ | @(Tra … (y∘d⁻¹•d) (y∘ıx2) y)
+   [ @Not_dep | @Pres_id ]
+ ]
+qed.
+
+record is_equiv (sup: st) (eq: sup → sup → props) : props ≝
+ { rfl_: ∀x. eq x x
+ ; sym_: ∀x,x'. eq x x' → eq x' x
+ ; tra_: ∀x,x',x''. eq x x' → eq x' x'' → eq x x''
+ }.
+
+record est: Type[1] ≝ 
+ { sup:> st
+ ; eq: sup → sup → props
+ ; is_est: is_equiv sup eq
+ }.
+interpretation "Equality in Extensional Sets" 'eq a b = (eq ? a b).
+
+definition rfl: ∀B: est. ∀x: B. x ≃ x ≝
+ λB. rfl_ … (is_est B).
+interpretation "Reflexivity in Extensional Sets" 'rfl x = (rfl ? x).
+
+definition sym: ∀B: est. ∀x,x': B. x ≃ x' → x' ≃ x ≝
+ λB. sym_ … (is_est B).
+interpretation "Symmetry in Extensional Sets" 'sym d = (sym ??? d).
+
+definition tra: ∀B: est. ∀x,x',x'': B. x ≃ x' → x' ≃ x'' → x ≃ x'' ≝
+ λB. tra_ … (is_est B).
+interpretation "Transitivity in Extensional Sets" 'tra d d' = (tra ???? d d').
+
+definition est_into_ecl: est → ecl ≝ 
+ λB. mk_ecl (sup B) (eq B) ?.
+ % [ @rfl | @sym | @tra ]
+qed.
+
+record is_subst (A: est)
+                (dsup: A → est)
+                (subst: ∀x1,x2: A. x1 ≃ x2 → dsup x1 → dsup x2) : props ≝
+ { pres_eq_:   ∀x1,x2: A. ∀d: x1 ≃ x2. ∀y,y': dsup x1.
+                y ≃ y' → subst … d y ≃ subst … d y'
+ ; not_dep_:   ∀x1,x2: A. ∀d1,d2: x1 ≃ x2. ∀y: dsup x1.
+                subst … d1 y ≃ subst … d2 y
+ ; pres_id_:   ∀x: sup A. ∀y: dsup x.
+                subst … (ıx) y ≃ y
+ ; clos_comp_: ∀x1,x2,x3: A. ∀y: dsup x1. ∀d1: x1 ≃ x2. ∀d2: x2 ≃ x3.
+                subst … d2 (subst … d1 y) ≃ subst … (d1•d2) y
+ }.
+
+record edst (A: est) : Type[1] ≝ 
+ { dsup:1> sup A → est
+ ; subst: ∀x1,x2: sup A. x1 ≃ x2 → sup (dsup x1) → sup (dsup x2)
+ ; is_edst: is_subst A dsup subst
+ }.
+interpretation "Substitution morphisms for Extensional Sets"
+ 'subst p a = (subst ???? p a).
+
+definition pres_eq: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y,y': C x1.
+                     y ≃ y' → y∘d ≃ y'∘d ≝
+ λB,C. pres_eq_ … (is_edst … C).
+definition not_dep: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d,d': x1 ≃ x2. ∀y: C x1.
+                     y∘d ≃ y∘d' ≝
+ λB,C. not_dep_ … (is_edst … C).
+definition pres_id: ∀B: est. ∀C: edst B. ∀x: B. ∀y: C x.
+                     y∘(ıx) ≃ y ≝
+ λB,C. pres_id_ … (is_edst … C).
+definition clos_comp: ∀B: est. ∀C: edst B. ∀x1,x2,x3: B. ∀y: C x1. ∀d: x1 ≃ x2. ∀d': x2 ≃ x3.
+                       y∘d∘d' ≃ y∘(d•d') ≝
+ λB,C. clos_comp_ … (is_edst … C).
+
+definition constant_edst: ∀A: est. est → edst A ≝
+ λA,Y. mk_edst … (λ_. Y) (λx1,x2,d,y. y) ?.
+ % [ #x1 #x2 #d #y #y' #h @h
+   | #x1 #x2 #_ #_ #y @(ıy)
+   | #_ #y @(ıy)
+   | #x1 #x2 #x3 #y #_ #_ @(ıy)
+   ]
+qed.
+
+lemma inverse_subst: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y: C x2.
+ y∘d⁻¹∘d ≃ y.
+ #B #C #x1 #x2 #d #y
+ @tra [ @(y∘d⁻¹•d)
+      | @clos_comp
+      | @tra [ @(y∘ıx2) | @not_dep | @pres_id ]
+      ]
+qed.
+
+lemma inverse_subst2: ∀B: est. ∀C: edst B. ∀x1,x2: B. ∀d: x1 ≃ x2. ∀y: C x1.
+ y∘d∘d⁻¹ ≃ y.
+ #B #C #x1 #x2 #d #y @tra [ @(y∘d•d⁻¹)
+                          | @clos_comp
+                          | @tra [ @(y∘(ıx1)) | @not_dep | @pres_id ]
+                          ]
+qed.
+
+lemma eq_reflexivity: ∀B: est. ∀b1,b2: B. b1 = b2 → b1 ≃ b2.
+ #B #b1 #b2 #h @(rewrite_l … b1 (λz. b1 ≃ z) (ıb1) … h)
+qed.
+
+definition eprop: Type[2] ≝ prop.
+
+definition eprop_into_ecl: eprop → ecl ≝
+ λP. mk_ecl P (λ_,_. ⊤) ?.
+ % //
+qed.
+
+definition eprops: Type[1] ≝ props.
+
+definition eprops_into_est: eprops → est ≝
+ λP. mk_est P (λ_,_. ⊤) ?.
+ % //
+qed.
+
diff --git a/matita/matita/contribs/mf/notations.ma b/matita/matita/contribs/mf/notations.ma
new file mode 100644
index 000000000..87c797807
--- /dev/null
+++ b/matita/matita/contribs/mf/notations.ma
@@ -0,0 +1,114 @@
+(* (C) 2014 Luca Bressan *)
+
+notation "hvbox(a break \to b)"
+ right associative with precedence 20
+ for @{ \forall $_:$a.$b }.
+
+notation < "hvbox(Σ ident i : ty break . p)"
+ left associative with precedence 20
+for @{'sigma (λ${ident i}: $ty. $p) }.
+notation < "hvbox(Σ ident i break . p)"
+ with precedence 20
+for @{'sigma (λ${ident i}. $p) }.
+
+notation > "Σ list1 ident x sep , opt (: T). term 19 Px"
+  with precedence 20
+  for ${ default
+          @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}: $T. $acc)} } }
+          @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}. $acc)} } }
+       }.
+
+notation "hvbox(π1 s)"
+ non associative with precedence 70
+ for @{ 'sig1 $s) }.
+notation "hvbox(π2 s)"
+ non associative with precedence 70
+ for @{ 'sig2 $s) }.
+
+notation "hvbox(〈 term 19 a, break term 19 b 〉)"
+ with precedence 90 for @{ 'mk_sigma $a $b }.
+
+notation "hvbox(B break × C)" 
+ left associative with precedence 55
+ for @{ 'times $B $C }.
+
+notation "⋆"
+ non associative with precedence 90
+ for @{ 'star }.
+
+notation "ϵ"
+ non associative with precedence 90
+ for @{ 'epsilon }.
+notation "⌈ l, c ⌉"
+ non associative with precedence 90
+ for @{ 'cons $l $c }.
+
+notation "hvbox(B break + C)" 
+ left associative with precedence 50
+ for @{ 'plus $B $C }.
+
+notation "⊥"
+ non associative with precedence 90
+ for @{ 'falsum }.
+
+notation "hvbox(B break ∨ C)" 
+ left associative with precedence 50
+ for @{ 'disj $B $C }.
+
+notation "hvbox(B break ∧ C)" 
+ left associative with precedence 60
+ for @{ 'conj $B $C }.
+
+notation < "hvbox(B break → C)" 
+ left associative with precedence 60
+ for @{ 'implies $B $C }.
+
+notation < "hvbox(∃ ident i : ty break . p)"
+ left associative with precedence 20
+for @{'exists (λ${ident i}: $ty. $p) }.
+notation < "hvbox(∃ ident i break . p)"
+ with precedence 20
+for @{'exists (λ${ident i}. $p) }.
+
+notation > "∃ list1 ident x sep , opt (: T). term 19 Px"
+  with precedence 20
+  for ${ default
+          @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}: $T. $acc)} } }
+          @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}. $acc)} } }
+       }.
+notation "hvbox(« term 19 a, break term 19 b »)"
+ with precedence 90 for @{ 'mk_exists $a $b }.
+
+notation "⊤"
+ non associative with precedence 90
+ for @{ 'verum }.
+
+notation "hvbox(a break = b)" 
+ non associative with precedence 45
+ for @{ 'id $a $b }.
+
+notation "hvbox(a break ≃ b)" 
+ non associative with precedence 45
+ for @{ 'eq $a $b }.
+
+notation "hvbox(ı x)" 
+ non associative with precedence 90
+ for @{ 'rfl $x }.
+notation "hvbox(d⁻¹)"
+ non associative with precedence 80
+ for @{ 'sym $d }.
+notation "hvbox(d break • d')" 
+ left associative with precedence 60
+ for @{ 'tra $d $d' }.
+
+notation "hvbox(y break ∘ d)"
+ non associative with precedence 50
+ for @{ 'subst $d $y }.
+
+notation "hvbox(f ◽ d)"
+ non associative with precedence 40
+ for @{ 'ap $f $d}.
+notation "hvbox(f ˙ d)"
+ non associative with precedence 60
+ for @{ 'sup_f $f $d}.
+
diff --git a/matita/matita/contribs/mf/pisigma.ma b/matita/matita/contribs/mf/pisigma.ma
new file mode 100644
index 000000000..85e39d73a
--- /dev/null
+++ b/matita/matita/contribs/mf/pisigma.ma
@@ -0,0 +1,110 @@
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+
+definition epi: ∀B: est. edst B → est ≝
+ λB,C. mk_est
+ (Σh: ∀y: sup B. sup (dsup … C y). ∀y1,y2: sup B. ∀d: y1 ≃ y2. subst … d (h y1) ≃ h y2)
+ (λz,z'. ∀y: sup B. eq … ((sig1 … z) y) ((sig1 … z') y))
+ ?.
+ % [ #x #y @(ı…)
+   | #x #x' #h #y @((h …)⁻¹)
+   | #x #x' #x'' #h1 #h2 #y @((h1 …)•(h2 …))
+   ]
+qed.
+
+interpretation "Properness of set morphisms" 'ap f d = (sig2 ?? f ?? d).
+interpretation "Support of set morphisms" 'sup_f f d = (sig1 ?? f d).
+
+definition eto: est → est → est ≝
+ λB,C. epi B (constant_edst B C).
+
+definition lift: ∀A,B: est. sup (eto A B) → edst B → edst A ≝
+ λA,B,f,C.
+ mk_edst A (λa: sup A. dsup … C (sig1 … f a))
+ (λx1,x2,d. subst … (sig2 … f … d)) ?.
+ letin B' ≝ (constant_edst A B)
+ % [ #x1 #x2 #d #y #y' #e @(pres_eq … e)
+   | #x1 #x2 #d1 #d2 #y @not_dep
+   | #x #y
+     cut (y∘(ı(f˙x)) ≃ y)
+     [ @pres_id
+     | cut (y∘(f◽(ıx)) ≃ y∘ı(f˙x))
+       [ @not_dep
+       | @tra
+       ]
+     ]
+   | #x1 #x2 #x3 #y #d1 #d2
+     cut (y∘(f◽d1)∘(f◽d2) ≃ y∘(f◽d1)•(f◽d2))
+     [ @clos_comp
+     | cut (y∘(f◽d1)•(f◽d2) ≃ y∘(f◽(d1•d2)))
+       [ @not_dep
+       | #e1 #e2 @(e2•e1)
+       ]
+     ]
+   ]
+qed.
+
+definition shift: ∀B: est. edst B → est → edst B.
+ #B #C #D %
+ [ #b @(eto (C b) D)
+ | #x1 #x2 #d #f %
+   [ #y @(f˙(y∘d⁻¹))
+   | #y1 #y2 #e @(f◽…) @pres_eq @e
+   ]
+ | %
+   [ #x1 #x2 #d #f1 #f2 #h #y @(h (y∘d⁻¹))
+   | #x1 #x2 #d1 #d2 #f #y @(f◽…) @not_dep
+   | #x #f #y @(f◽…) cut (y∘(ıx) ≃ y)
+     [ @pres_id
+     | #h @tra [ @(y∘(ıx)) | @not_dep | @pres_id ]
+     ]
+   | #x1 #x2 #x3 #f #d1 #d2 #y @(f◽…)
+     @tra [ @(y∘(d2⁻¹•d1⁻¹)) | @clos_comp | @not_dep ]
+   ]
+ ]
+qed.
+
+definition esigma: ∀B: est. edst B → est ≝ 
+ λB,C. mk_est 
+ (Σy: B. C y)
+ (λz,z'. ∃d: π1 z ≃ π1 z'. (π2 z)∘d ≃ π2 z')
+ ?.
+ % [ * #b #c %{ıb} @pres_id
+   | * #b #c * #b' #c' * #d #h %{(d⁻¹)}
+     @tra [ @(c∘d•d⁻¹)
+          | @tra [ @(c∘d∘d⁻¹) | @pres_eq @(h⁻¹) | @clos_comp ]
+          | @tra [ @(c∘ıb) | @not_dep | @pres_id ]
+          ]
+   | * #b #c * #b' #c' * #b'' #c'' * #d1 #h1 * #d2 #h2 %{(d1•d2)}
+     @tra [ @(c∘d1∘d2)
+          | @sym @clos_comp
+          | @tra [ @(c'∘d2) | @pres_eq @h1 | @h2 ]
+          ]
+   ]
+qed.
+
+definition etimes: est → est → est ≝
+ λB,C. esigma B (constant_edst B C).
+
+definition mk_esigma: ∀B: est. ∀C: edst B. epi B (shift B C (esigma B C)).
+ #B #C %
+ [ #b %
+   [ #c @〈b, c〉
+   | #c1 #c2 #d %{(ıb)}
+     @tra [ @c1 | @pres_id | @d ]
+   ]
+ | #b1 #b2 #d #y %{d} @inverse_subst
+ ]
+qed.
+
+definition esig1: ∀B: est. ∀C: edst B. sup (eto (esigma B C) B) ≝
+ λB,C. 〈π1 …, ?〉.
+ * #b1 #c1 * #b2 #c2 * #db #dc @db
+qed.
+
+definition esig2: ∀B: est. ∀C: edst B. sup (epi (esigma B C) (lift … (esig1 …) C …)) ≝ 
+ λB,C. 〈π2 …, ?〉.
+ * #b1 #c1 * #b2 #c2 * #db #dc @dc
+qed.
+
diff --git a/matita/matita/contribs/mf/pisigma2.ma b/matita/matita/contribs/mf/pisigma2.ma
new file mode 100644
index 000000000..24a950c2f
--- /dev/null
+++ b/matita/matita/contribs/mf/pisigma2.ma
@@ -0,0 +1,110 @@
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+
+definition ePi: ∀B: ecl. edcl B → ecl ≝
+ λB,C. mk_ecl
+ (Σh: ∀y: Sup B. Sup (dSup … C y). ∀y1,y2: Sup B. ∀d: y1 ≃ y2. Subst … d (h y1) ≃ h y2)
+ (λz,z'. ∀y: Sup B. Eq … ((Sig1 … z) y) ((Sig1 … z') y))
+ ?.
+ % [ #x #y @(ı…)
+   | #x #x' #h #y @((h …)⁻¹)
+   | #x #x' #x'' #h1 #h2 #y @((h1 …)•(h2 …))
+   ]
+qed.
+
+interpretation "Properness of col morphisms" 'ap f d = (Sig2 ?? f ?? d).
+interpretation "Support of col morphisms" 'sup_f f d = (Sig1 ?? f d).
+
+definition eTo: ecl → ecl → ecl ≝
+ λB,C. ePi B (constant_edcl B C).
+
+definition Lift: ∀A,B: ecl. Sup (eTo A B) → edcl B → edcl A ≝
+ λA,B,f,C.
+ mk_edcl A (λa: Sup A. dSup … C (Sig1 … f a))
+ (λx1,x2,d. Subst … (Sig2 … f … d)) ?.
+ letin B' ≝ (constant_edcl A B)
+ % [ #x1 #x2 #d #y #y' #e @(Pres_eq … e)
+   | #x1 #x2 #d1 #d2 #y @Not_dep
+   | #x #y
+     cut (y∘(ı(f˙x)) ≃ y)
+     [ @Pres_id
+     | cut (y∘(f◽(ıx)) ≃ y∘ı(f˙x))
+       [ @Not_dep
+       | @Tra
+       ]
+     ]
+   | #x1 #x2 #x3 #y #d1 #d2
+     cut (y∘(f◽d1)∘(f◽d2) ≃ y∘(f◽d1)•(f◽d2))
+     [ @Clos_comp
+     | cut (Eq (C (f˙x3)) (y∘(f◽d1)•(f◽d2)) (y∘(f◽(d1•d2))))
+       [ @Not_dep
+       | #e1 #e2 @(e2•e1)
+       ]
+     ]
+   ]
+qed.
+
+definition Shift: ∀B: ecl. edcl B → ecl → edcl B.
+ #B #C #D %
+ [ #b @(eTo (C b) D)
+ | #x1 #x2 #d #f %
+   [ #y @(f˙(y∘d⁻¹))
+   | #y1 #y2 #e @(f◽…) @Pres_eq @e
+   ]
+ | %
+   [ #x1 #x2 #d #f1 #f2 #h #y @(h (y∘d⁻¹))
+   | #x1 #x2 #d1 #d2 #f #y @(f◽…) @Not_dep
+   | #x #f #y @(f◽…) cut (y∘(ıx) ≃ y)
+     [ @Pres_id
+     | #h @Tra [ @(y∘(ıx)) | @Not_dep | @Pres_id ]
+     ]
+   | #x1 #x2 #x3 #f #d1 #d2 #y @(f◽…)
+     @Tra [ @(y∘(d2⁻¹•d1⁻¹)) | @Clos_comp | @Not_dep ]
+   ]
+ ]
+qed.
+
+definition eSigma: ∀B: ecl. edcl B → ecl ≝ 
+ λB,C. mk_ecl
+ (Σy: B. C y)
+ (λz,z'. ∃d: π1 z ≃ π1 z'. (π2 z)∘d ≃ π2 z')
+ ?.
+ % [ * #b #c %{ıb} @Pres_id
+   | * #b #c * #b' #c' * #d #h %{(d⁻¹)}
+     @Tra [ @(c∘d•d⁻¹)
+          | @Tra [ @(c∘d∘d⁻¹) | @Pres_eq @(h⁻¹) | @Clos_comp ]
+          | @Tra [ @(c∘ıb) | @Not_dep | @Pres_id ]
+          ]
+   | * #b #c * #b' #c' * #b'' #c'' * #d1 #h1 * #d2 #h2 %{(d1•d2)}
+     @Tra [ @(c∘d1∘d2)
+          | @Sym @Clos_comp
+          | @Tra [ @(c'∘d2) | @Pres_eq @h1 | @h2 ]
+          ]
+   ]
+qed.
+
+definition eTimes: ecl → ecl → ecl ≝
+ λB,C. eSigma B (constant_edcl B C).
+
+definition mk_eSigma: ∀B: ecl. ∀C: edcl B. ePi B (Shift B C (eSigma B C)).
+ #B #C %
+ [ #b %
+   [ #c @〈b, c〉
+   | #c1 #c2 #d %{(ıb)}
+     @Tra [ @c1 | @Pres_id | @d ]
+   ]
+ | #b1 #b2 #d #y %{d} @inverse_Subst
+ ]
+qed.
+
+definition eSig1: ∀B: ecl. ∀C: edcl B. Sup (eTo (eSigma B C) B) ≝
+ λB,C. 〈π1 …, ?〉.
+ * #b1 #c1 * #b2 #c2 * #db #dc @db
+qed.
+
+definition eSig2: ∀B: ecl. ∀C: edcl B. Sup (ePi (eSigma B C) (Lift … (eSig1 …) C …)) ≝ 
+ λB,C. 〈π2 …, ?〉.
+ * #b1 #c1 * #b2 #c2 * #db #dc @dc
+qed.
+
diff --git a/matita/matita/contribs/mf/plus.ma b/matita/matita/contribs/mf/plus.ma
new file mode 100644
index 000000000..141c83e39
--- /dev/null
+++ b/matita/matita/contribs/mf/plus.ma
@@ -0,0 +1,96 @@
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+include "pisigma.ma".
+
+definition eplus: est → est → est ≝
+ λB,C. mk_est
+ (B+C)
+ (λz,z'. (∃b: B. ∃b': B. (z = inl … b) ∧ ((z' = inl … b') ∧ (b ≃ b')))
+         ∨ (∃c: C. ∃c': C. (z = inr … c) ∧ ((z' = inr … c') ∧ (c ≃ c'))))
+ ?.
+ % [ * #x [ %1 | %2 ] %{x} %{x} %
+     [ 1,3: @(reflexivity …)
+     | 2: @(mk_conj … (reflexivity …) (ıx)) 
+     | 4: @(mk_conj … (reflexivity …) (ıx))
+     ]
+   | #z1 #z2 * * #x1 * #x2 * #h1 * #h2 #e [ %1 | %2 ] %{x2} %{x1} %
+     [ 1,3: @h2
+     | 2,4: % [ 1,3: @h1
+              | 2,4: @(e⁻¹)
+              ]
+     ]
+   | #z1 #z2 #z3 * * #x1 * #x12 * #h1 * #h12 #e12 * * #x23 * #x3 * #h23 * #h3 #e23
+     [ %1 %{x1} %{x3} %
+       [ @h1
+       | % [ @h3
+           | @(e12• 
+               (rewrite_l … x23 (λz. z ≃ x3) e23 … 
+                (injectivity_inl … (h12⁻¹•h23)⁻¹)))
+           ]
+       ]
+     | @(falsum_rect_CProp0 … (plus_clash … (h12⁻¹•h23)))
+     | @(falsum_rect_CProp0 … (plus_clash … ((h12⁻¹•h23)⁻¹)))
+     | %2 %{x1} %{x3} %
+       [ @h1
+       | % [ @h3
+           | @(e12•
+               (rewrite_l … x23 (λz. z ≃ x3) e23 …
+                (injectivity_inr … (h12⁻¹•h23)⁻¹)))
+           ]
+       ]
+     ]
+   ]
+qed.
+
+definition einl: ∀B,C: est. eto B (eplus B C) ≝
+ λB,C. 〈inl …, ?〉.
+ #x #y #h %1 %{x} %{y} % % [ % | @h ]
+qed.
+
+definition einr: ∀B,C: est. eto C (eplus B C) ≝
+ λB,C. 〈inr …, ?〉.
+ #x #y #h %2 %{x} %{y} % % [ % | @h ]
+qed.
+
+lemma injectivity_einl: ∀B,C: est. ∀b,b': B. (einl B C)˙b ≃ (einl B C)˙b' → b ≃ b'.
+ #B #C #b #b' * * #z * #z' * #h1 * #h2 #h3
+ [ @(rewrite_l … z (λw. w ≃ b')
+     (rewrite_l … z' (λw. z ≃ w) h3 … (symmetry … (injectivity_inl … h2))) …
+     (symmetry … (injectivity_inl … h1)))
+ | @(falsum_rect_CProp0 … (plus_clash … h1))
+ ]
+qed.
+
+lemma injectivity_einr: ∀B,C: est. ∀c,c': C. (einr B C)˙c ≃ (einr B C)˙c' → c ≃ c'.
+ #B #C #c #c' * * #z * #z' * #h1 * #h2 #h3
+ [ @(falsum_rect_CProp0 … (plus_clash … (symmetry … h1)))
+ | @(rewrite_l … z (λw. w ≃ c')
+     (rewrite_l … z' (λw. z ≃ w) h3 … (symmetry … (injectivity_inr … h2))) …
+     (symmetry … (injectivity_inr … h1)))
+ ]
+qed.
+
+definition edplus: ∀I: est. edst I → edst I → edst I.
+ #I #B #C %
+ [ @(λi. eplus (B i) (C i))
+ | #i1 #i2 #e * #x [ @(inl … (x∘e)) | @(inr … (x∘e)) ]
+ | % [ #i1 #i2 #e * #x1 * #x2 #h
+       cases h * #z1 * #z2 * #h1 * #h2 #d
+         [ 1: %1 %{(x1∘e)} %{(x2∘e)} % [ % | % [ % | @(pres_eq … (injectivity_einl … h)) ]]
+         | 2,4: @(falsum_rect_CProp0 … (plus_clash … h1))
+         | 3: @(falsum_rect_CProp0 … (plus_clash … h2⁻¹))
+         | 5,7: @(falsum_rect_CProp0 … (plus_clash … h1⁻¹))
+         | 6: @(falsum_rect_CProp0 … (plus_clash … h2))
+         | 8: %2 %{(x1∘e)} %{(x2∘e)} % [ % | % [ % | @(pres_eq … (injectivity_einr … h)) ]]
+         ]
+     | #i1 #i2 #e1 #e2 * #x [ %1 | %2 ] %{(x∘e1)} %{(x∘e2)} %
+       [ 1,3: % | 2,4: % [ 1,3: % | 2,4: @not_dep ]]
+     | #i * #x [ %1 | %2 ] %{(x∘ıi)} %{x} %
+       [ 1,3: % | 2,4: % [ 1,3: % | 2,4: @pres_id ]]
+     | #i1 #i2 #i3 * #x #d1 #d2 [ %1 | %2 ] %{(x∘d1∘d2)} %{(x∘d1•d2)} %
+       [ 1,3: % | 2,4: % [ 1,3: % | 2,4: @clos_comp ]]
+     ]
+ ]
+qed.
+
diff --git a/matita/matita/contribs/mf/power.ma b/matita/matita/contribs/mf/power.ma
new file mode 100644
index 000000000..27a84ec3b
--- /dev/null
+++ b/matita/matita/contribs/mf/power.ma
@@ -0,0 +1,17 @@
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+
+definition fun_to_power_one: est → ecl ≝ 
+ λB. mk_ecl
+ (Σh: fun_to_props B. ∀y1,y2: B. eq … y1 y2 → (conj (h y1 → h y2) (h y2 → h y1)))
+ (λz,z'. ∀y: B. conj ((Sig1 … z) y → (Sig1 … z') y)
+                         (implies ((Sig1 … z') y) ((Sig1 … z) y)))
+ ?.
+ % [ #x #y % #h @h 
+   | #x #x' #h #b % #k cases (h b) [ #_ #r | #r #_ ] @(r k) 
+   | #x #x' #x'' #h1 #h2 #b cases (h1 b) #k10 #k01 cases (h2 b) #k21 #k12 %
+     #r [ @(k21 (k10 r)) | @(k01 (k12 r)) ]
+   ]
+qed.
+
diff --git a/matita/matita/contribs/mf/power_one.ma b/matita/matita/contribs/mf/power_one.ma
new file mode 100644
index 000000000..0be6282ae
--- /dev/null
+++ b/matita/matita/contribs/mf/power_one.ma
@@ -0,0 +1,28 @@
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+
+definition power_one: ecl ≝
+ mk_ecl props (λz,z'. (z → z') ∧ (z' → z)) ?.
+ % [ #x % #h @h
+   | #x #y * #h1 #h2 % [ @h2 | @h1 ]
+   | #x #y #z #h1 #h2 % cases h1 #hxy #hyx cases h2 #hyz #hzy
+     [ #hx @(hyz (hxy hx))
+     | #hz @(hyx (hzy hz))
+     ]
+   ]
+qed.
+
+definition dpower_one: ∀I: ecl. edcl I.
+ #I %
+ [ #i @power_one
+ | #i1 #i2 #e #p @p
+ | %
+   [ #i1 #i2 #_ #y #y' #h @h
+   | #i1 #i2 #_ #_ @Rfl
+   | #i @Rfl
+   | #i1 #i2 #i3 #y #_ #_ @Rfl
+   ]
+ ]
+qed.
+
diff --git a/matita/matita/contribs/mf/root b/matita/matita/contribs/mf/root
new file mode 100644
index 000000000..bb65fd45c
--- /dev/null
+++ b/matita/matita/contribs/mf/root
@@ -0,0 +1 @@
+baseuri=cic:/matita/minimalist_foundation/
diff --git a/matita/matita/contribs/mf/singleton.ma b/matita/matita/contribs/mf/singleton.ma
new file mode 100644
index 000000000..4a2d6854f
--- /dev/null
+++ b/matita/matita/contribs/mf/singleton.ma
@@ -0,0 +1,24 @@
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+include "pisigma.ma".
+
+definition en1: est ≝
+ mk_est n1 (λz,z'. z = z') ?.
+ % #x [ % | #y * % | #y #z * * % ]
+qed.
+
+definition estar: en1 ≝ ⋆.
+
+definition en1_rect_Type0: ∀Q: edst en1. eto (Q estar) (epi en1 Q).
+ #Q @(〈?, ?〉)
+ [ #h @(〈n1_rect_Type0 (λw. Q w) h, ?〉)
+   * * #d
+   @(rewrite_l … h (λz. (subst … d z) ≃ z) … (n1_rect_Type0 … h estar) (reflexivity …))
+   @tra [ @(h∘(ı…)) | @not_dep | @pres_id ]
+ | #y1 #y2 #d * @d
+ ]
+qed.
+
+definition edn1: ∀I: est. edst I ≝ λI. constant_edst I en1.
+