module WeaklyInitialSetsOfCovers where
open import TypeTheory public
record Fam (l : Level) : Set (lsuc l) where
constructor mkFam
field
base : Set l
fiber : base → Set l
open Fam public
wisc : {l : Level} → Set l → Fam l → Prop (lsuc l)
wisc {l} A W =
(E : Set l)
(q : E → A)
(_ : surjection q)
→
∃ c ∶ base W ,
∃ f ∶ (fiber W c → E),
surjection (q ∘ f)
wAC :
{l : Level}
{A : Set l}
(W : Fam l)
(_ : wisc A W)
(B : A → Set l)
(P : (x : A) → B x → Prop l)
(_ : ∀ x → ∃ (B x) (P x))
→
∃ c ∶ base W ,
∃ p ∶ (fiber W c → A),
∃ q ∶ ((z : fiber W c) → B (p z)),
(surjection p ∧ ∀ z → P (p z) (q z))
wAC {l} {A} W w B P e = wac
where
C : Set l
C = set (x , y) ∶ (∑ A B), P x y
p' : C → A
p' ((x , _) ∣ _) = x
surjectionp' : surjection p'
surjectionp' x with e x
... | ∃i y u = ∃i ((x , y) ∣ u) refl
q' : (z : C) → B (p' z)
q' ((_ , y) ∣ _) = y
r : ∀ z → P (p' z) (q' z)
r ((_ , _) ∣ p) = p
wac : ∃ c ∶ base W ,
∃ p ∶ (fiber W c → A),
∃ q ∶ ((z : fiber W c) → B (p z)),
(surjection p ∧ ∀ z → P (p z) (q z))
wac with w C p' surjectionp'
... | ∃i c (∃i k u) =
∃i c (
∃i (p' ∘ k) (
∃i (q' ∘ k) (
∧i u λ z → r (k z))))
oldsklWISC :
{l : Level}
{A : Set l}
(W : Fam l)
(_ : wisc A W)
{B E : Set l}
(f : A → B)
(q : E → B)
(_ : surjection q)
→
∃ c ∶ base W ,
∃ p ∶ (fiber W c → A),
∃ f' ∶ (fiber W c → E),
(surjection p ∧ q ∘ f' == f ∘ p)
oldsklWISC {l} {A} W Wwisc {B} {E} f q surjq = match wac (λ {
(∃i c (∃i g (∃i g' (∧i gsurj eq)))) →
∃i c (∃i g (∃i g' (∧i gsurj (funext eq)))
)
})
where
P : A → E → Prop l
P pz f'z = q f'z == f pz
Ptotal : (x : A) → ∃ E (P x)
Ptotal x = surjq (f x)
wac = wAC W Wwisc (λ _ → E) P Ptotal
postulate
IWISC :
{l : Level}
(F : Fam l)
→
∃ W ∶ Fam l , ∀ c → wisc (fiber F c) W