matita/matita/contribs/mf/pisigma2.ma

   1 (* (C) 2014 Luca Bressan *)
   2
   3 include "model.ma".
   4
   5 definition ePi: ∀B: ecl. edcl B → ecl ≝
   6  λB,C. mk_ecl
   7  (Σh: ∀y: Sup B. Sup (dSup … C y). ∀y1,y2: Sup B. ∀d: y1 ≃ y2. Subst … d (h y1) ≃ h y2)
   8  (λz,z'. ∀y: Sup B. Eq … ((Sig1 … z) y) ((Sig1 … z') y))
   9  ?.
  10  % [ #x #y @(ı…)
  11    | #x #x' #h #y @((h …)⁻¹)
  12    | #x #x' #x'' #h1 #h2 #y @((h1 …)•(h2 …))
  13    ]
  14 qed.
  15
  16 interpretation "Properness of col morphisms" 'ap f d = (Sig2 ?? f ?? d).
  17 interpretation "Support of col morphisms" 'sup_f f d = (Sig1 ?? f d).
  18
  19 definition eTo: ecl → ecl → ecl ≝
  20  λB,C. ePi B (constant_edcl B C).
  21
  22 definition Lift: ∀A,B: ecl. Sup (eTo A B) → edcl B → edcl A ≝
  23  λA,B,f,C.
  24  mk_edcl A (λa: Sup A. dSup … C (Sig1 … f a))
  25  (λx1,x2,d. Subst … (Sig2 … f … d)) ?.
  26  letin B' ≝ (constant_edcl A B)
  27  % [ #x1 #x2 #d #y #y' #e @(Pres_eq … e)
  28    | #x1 #x2 #d1 #d2 #y @Not_dep
  29    | #x #y
  30      cut (y∘(ı(f˙x)) ≃ y)
  31      [ @Pres_id
  32      | cut (y∘(f◽(ıx)) ≃ y∘ı(f˙x))
  33        [ @Not_dep
  34        | @Tra
  35        ]
  36      ]
  37    | #x1 #x2 #x3 #y #d1 #d2
  38      cut (y∘(f◽d1)∘(f◽d2) ≃ y∘(f◽d1)•(f◽d2))
  39      [ @Clos_comp
  40      | cut (Eq (C (f˙x3)) (y∘(f◽d1)•(f◽d2)) (y∘(f◽(d1•d2))))
  41        [ @Not_dep
  42        | #e1 #e2 @(e2•e1)
  43        ]
  44      ]
  45    ]
  46 qed.
  47
  48 definition Shift: ∀B: ecl. edcl B → ecl → edcl B.
  49  #B #C #D %
  50  [ #b @(eTo (C b) D)
  51  | #x1 #x2 #d #f %
  52    [ #y @(f˙(y∘d⁻¹))
  53    | #y1 #y2 #e @(f◽…) @Pres_eq @e
  54    ]
  55  | %
  56    [ #x1 #x2 #d #f1 #f2 #h #y @(h (y∘d⁻¹))
  57    | #x1 #x2 #d1 #d2 #f #y @(f◽…) @Not_dep
  58    | #x #f #y @(f◽…) cut (y∘(ıx) ≃ y)
  59      [ @Pres_id
  60      | #h @Tra [ @(y∘(ıx)) | @Not_dep | @Pres_id ]
  61      ]
  62    | #x1 #x2 #x3 #f #d1 #d2 #y @(f◽…)
  63      @Tra [ @(y∘(d2⁻¹•d1⁻¹)) | @Clos_comp | @Not_dep ]
  64    ]
  65  ]
  66 qed.
  67
  68 definition eSigma: ∀B: ecl. edcl B → ecl ≝
  69  λB,C. mk_ecl
  70  (Σy: B. C y)
  71  (λz,z'. ∃d: π1 z ≃ π1 z'. (π2 z)∘d ≃ π2 z')
  72  ?.
  73  % [ * #b #c %{ıb} @Pres_id
  74    | * #b #c * #b' #c' * #d #h %{(d⁻¹)}
  75      @Tra [ @(c∘d•d⁻¹)
  76           | @Tra [ @(c∘d∘d⁻¹) | @Pres_eq @(h⁻¹) | @Clos_comp ]
  77           | @Tra [ @(c∘ıb) | @Not_dep | @Pres_id ]
  78           ]
  79    | * #b #c * #b' #c' * #b'' #c'' * #d1 #h1 * #d2 #h2 %{(d1•d2)}
  80      @Tra [ @(c∘d1∘d2)
  81           | @Sym @Clos_comp
  82           | @Tra [ @(c'∘d2) | @Pres_eq @h1 | @h2 ]
  83           ]
  84    ]
  85 qed.
  86
  87 definition eTimes: ecl → ecl → ecl ≝
  88  λB,C. eSigma B (constant_edcl B C).
  89
  90 definition mk_eSigma: ∀B: ecl. ∀C: edcl B. ePi B (Shift B C (eSigma B C)).
  91  #B #C %
  92  [ #b %
  93    [ #c @〈b, c〉
  94    | #c1 #c2 #d %{(ıb)}
  95      @Tra [ @c1 | @Pres_id | @d ]
  96    ]
  97  | #b1 #b2 #d #y %{d} @inverse_Subst
  98  ]
  99 qed.
 100
 101 definition eSig1: ∀B: ecl. ∀C: edcl B. Sup (eTo (eSigma B C) B) ≝
 102  λB,C. 〈π1 …, ?〉.
 103  * #b1 #c1 * #b2 #c2 * #db #dc @db
 104 qed.
 105
 106 definition eSig2: ∀B: ecl. ∀C: edcl B. Sup (ePi (eSigma B C) (Lift … (eSig1 …) C …)) ≝
 107  λB,C. 〈π2 …, ?〉.
 108  * #b1 #c1 * #b2 #c2 * #db #dc @dc
 109 qed.
 110