X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Fmf%2Fsingleton.ma;fp=matita%2Fmatita%2Fcontribs%2Fmf%2Fsingleton.ma;h=4a2d6854f5c9c3e42cc0aae8633c33cddccea947;hb=b3aa03ebf904d8c7290aa44b4ce80bf3f976fb2e;hp=0000000000000000000000000000000000000000;hpb=e83cd27fc0694c34baf35c8b80d32317e51be707;p=helm.git

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.
+