matita/matita/contribs/mf/singleton.ma

   1 (* (C) 2014 Luca Bressan *)
   2
   3 include "model.ma".
   4 include "pisigma.ma".
   5
   6 definition en1: est ≝
   7  mk_est n1 (λz,z'. z = z') ?.
   8  % #x [ % | #y * % | #y #z * * % ]
   9 qed.
  10
  11 definition estar: en1 ≝ ⋆.
  12
  13 definition en1_rect_Type0: ∀Q: edst en1. eto (Q estar) (epi en1 Q).
  14  #Q @(〈?, ?〉)
  15  [ #h @(〈n1_rect_Type0 (λw. Q w) h, ?〉)
  16    * * #d
  17    @(rewrite_l … h (λz. (subst … d z) ≃ z) … (n1_rect_Type0 … h estar) (reflexivity …))
  18    @tra [ @(h∘(ı…)) | @not_dep | @pres_id ]
  19  | #y1 #y2 #d * @d
  20  ]
  21 qed.
  22
  23 definition edn1: ∀I: est. edst I ≝ λI. constant_edst I en1.
  24