1 (* (C) 2014 Luca Bressan *)
5 definition ePi: ∀B: ecl. edcl B → 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))
11 | #x #x' #h #y @((h …)⁻¹)
12 | #x #x' #x'' #h1 #h2 #y @((h1 …)•(h2 …))
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).
19 definition eTo: ecl → ecl → ecl ≝
20 λB,C. ePi B (constant_edcl B C).
22 definition Lift: ∀A,B: ecl. Sup (eTo A B) → edcl B → edcl A ≝
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
32 | cut (y∘(f◽(ıx)) ≃ y∘ı(f˙x))
37 | #x1 #x2 #x3 #y #d1 #d2
38 cut (y∘(f◽d1)∘(f◽d2) ≃ y∘(f◽d1)•(f◽d2))
40 | cut (Eq (C (f˙x3)) (y∘(f◽d1)•(f◽d2)) (y∘(f◽(d1•d2))))
48 definition Shift: ∀B: ecl. edcl B → ecl → edcl B.
53 | #y1 #y2 #e @(f◽…) @Pres_eq @e
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)
60 | #h @Tra [ @(y∘(ıx)) | @Not_dep | @Pres_id ]
62 | #x1 #x2 #x3 #f #d1 #d2 #y @(f◽…)
63 @Tra [ @(y∘(d2⁻¹•d1⁻¹)) | @Clos_comp | @Not_dep ]
68 definition eSigma: ∀B: ecl. edcl B → ecl ≝
71 (λz,z'. ∃d: π1 z ≃ π1 z'. (π2 z)∘d ≃ π2 z')
73 % [ * #b #c %{ıb} @Pres_id
74 | * #b #c * #b' #c' * #d #h %{(d⁻¹)}
76 | @Tra [ @(c∘d∘d⁻¹) | @Pres_eq @(h⁻¹) | @Clos_comp ]
77 | @Tra [ @(c∘ıb) | @Not_dep | @Pres_id ]
79 | * #b #c * #b' #c' * #b'' #c'' * #d1 #h1 * #d2 #h2 %{(d1•d2)}
82 | @Tra [ @(c'∘d2) | @Pres_eq @h1 | @h2 ]
87 definition eTimes: ecl → ecl → ecl ≝
88 λB,C. eSigma B (constant_edcl B C).
90 definition mk_eSigma: ∀B: ecl. ∀C: edcl B. ePi B (Shift B C (eSigma B C)).
95 @Tra [ @c1 | @Pres_id | @d ]
97 | #b1 #b2 #d #y %{d} @inverse_Subst
101 definition eSig1: ∀B: ecl. ∀C: edcl B. Sup (eTo (eSigma B C) B) ≝
103 * #b1 #c1 * #b2 #c2 * #db #dc @db
106 definition eSig2: ∀B: ecl. ∀C: edcl B. Sup (ePi (eSigma B C) (Lift … (eSig1 …) C …)) ≝
108 * #b1 #c1 * #b2 #c2 * #db #dc @dc