1 (* (C) 2014 Luca Bressan *)
5 definition epi: ∀B: est. edst B → est ≝
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 set morphisms" 'ap f d = (sig2 ?? f ?? d).
17 interpretation "Support of set morphisms" 'sup_f f d = (sig1 ?? f d).
19 definition eto: est → est → est ≝
20 λB,C. epi B (constant_edst B C).
22 definition lift: ∀A,B: est. sup (eto A B) → edst B → edst A ≝
24 mk_edst A (λa: sup A. dsup … C (sig1 … f a))
25 (λx1,x2,d. subst … (sig2 … f … d)) ?.
26 letin B' ≝ (constant_edst 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 (y∘(f◽d1)•(f◽d2) ≃ y∘(f◽(d1•d2)))
48 definition shift: ∀B: est. edst B → est → edst 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: est. edst B → est ≝
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: est → est → est ≝
88 λB,C. esigma B (constant_edst B C).
90 definition mk_esigma: ∀B: est. ∀C: edst 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: est. ∀C: edst B. sup (eto (esigma B C) B) ≝
103 * #b1 #c1 * #b2 #c2 * #db #dc @db
106 definition esig2: ∀B: est. ∀C: edst B. sup (epi (esigma B C) (lift … (esig1 …) C …)) ≝
108 * #b1 #c1 * #b2 #c2 * #db #dc @dc