module QW.FixedPointsAreQWTypes where
open import QW.SizeIndexedStructure public
module _
{l : Level}
(Σ : Sig {l})
(ε : Syseq Σ)
where
private
Γ = fst ε
lhs = fst (snd ε)
rhs = snd (snd ε)
Ξ = Σ ⊕ Γ
FxSzAlg→QWType :
∃ Size ∶ Set l ,
∃ ssz ∶ SizeStructure Size ,
(let open Colim Size {{ssz}} in
Inhabited (SizeIdxStruct.FixSizeStruct Σ ε Size {{ssz}} → QWtype Σ ε)
)
FxSzAlg→QWType
with IWISC (mkFam (Op Ξ) (Ar Ξ))
... | ∃i (mkFam C F) w
with IWISC (mkFam (∑ (c , a) ∶ C × (Op Ξ) , (F c → Ar Ξ a)) λ{(_ , f) → ker f})
... | ∃i (mkFam C' F') w' =
∃i Size (∃i ssz
(inhab getQWType)
)
module _ where
Size = CocontinuityOfTakingPowers.Size Ξ C F w C' F' w'
instance
ssz = CocontinuityOfTakingPowers.ssz Ξ C F w C' F' w'
upperbounds : UpperBounds {l} _ _
upperbounds = CocontinuityOfTakingPowers.upperbounds Ξ C F w C' F' w'
open SizeIdxStruct Σ ε Size {{ssz}} renaming (D to ∣D_∣)
open Colim Size
getQWType : SizeIdxStruct.FixSizeStruct {l} Σ ε Size {{ssz}} → QWtype Σ ε
getQWType (A ∣ δ) =
mkQWtype QW {{AlgQW}} satQW recQW homrecQW uniqQW
where
W : Size → Set l
W i = Wᵇ (A ↓ i)
R : ∀ i → W i → W i → Prop l
R i = Rᵇ (A ↓ i)
Q : Size → Set l
Q i = W i / R i
DA=Q : ∀{i} → ∣D A ∣ i == Q i
DA=Q {i} = ∧e₁ (δ i)
τ=[pairᵇ]/R : ∀{i} → ∀ᵇ j < i ,
(∀ t → τ A i j t === [ pairᵇ j t ]/ R i)
τ=[pairᵇ]/R {i} j = ∧e₂ (δ i) j
W′ : ∀ i → ∏ᵇ j < i , (W j → W i)
W′ i j (pairᵇ k t) = pairᵇ k t
Q′ : ∀ i → ∏ᵇ j < i , (Q j → Q i)
Q′ i j = quot.lift {R = R j}
(λ z → [ W′ i j z ]/ R i)
λ{ (τεᵇ k e ρ) → quot.eq (R i) (τεᵇ k e ρ)
; (τηᵇ k l t) → quot.eq (R i) (τηᵇ k l t)
; (τσᵇ k l a f) → quot.eq (R i) (τσᵇ k l a f)
}
D′ : ∀ i → ∏ᵇ j < i , (∣D A ∣ j → ∣D A ∣ i)
D′ i j = τ A i j ∘ η
τ-surj :
(i : Size)
(x : ∣D A ∣ i)
→
∃ᵇ j < i , (∃ t ∶ T (∣D A ∣ j) , τ A i j t == x)
τ-surj i x =
match (quot.surjectionmk (R i) (coe DA=Q x))
λ{(∃i (pairᵇ j t) p) → ∃ᵇi j (∃i t
(proof
τ A i j t
=[ τ=[pairᵇ]/R j t ]
[ pairᵇ j t ]/ R i
=[ p ]
coe DA=Q x
=[ coe=== DA=Q x ]
x
qed))}
D′=Q′ : ∀ i → ∀ᵇ j < i , (∀ x →
coe DA=Q (D′ i j x) == Q′ i j (coe DA=Q x))
D′=Q′ i j x = match (τ-surj j x) (λ {
(∃ᵇi k (∃i t refl)) →
proof
coe DA=Q (τ A i j (η (τ A j k t)))
=[ coe=== DA=Q _ ]
τ A i j (η (τ A j k t))
=[ τ=[pairᵇ]/R j _ ]
[ pairᵇ j (η (τ A j k t)) ]/ R i
=[ quot.eq (R i) (τηᵇ j k t) ]
[ pairᵇ k t ]/ R i
=[ ap (Q′ i j)
(symm (trans (τ=[pairᵇ]/R k t) (coe=== DA=Q _))) ]
Q′ i j (coe DA=Q (τ A j k t))
qed
})
Dact : ∀ i → ∀ᵇ j < i , ∀ᵇ k < j , (∀ z →
D′ i k z == D′ i j (D′ j k z))
Dact i j k z =
proof
τ A i k (η z)
=[ τ=[pairᵇ]/R k _ ]
[ pairᵇ k (η z) ]/ R i
=[ symm (quot.eq (R i) (τηᵇ j k (η z))) ]
[ pairᵇ j (η (τ A j k (η z))) ]/ R i
=[ symm (τ=[pairᵇ]/R j _) ]
τ A i j (η (τ A j k (η z)))
qed
τε : ∀ i → ∀ᵇ j < i ,
((e : Op Γ)
(ρ : Ar Γ e → ∣D A ∣ j)
→
τ A i j (T' ρ (lhs e)) == τ A i j (T' ρ (rhs e)))
τε i j e ρ =
proof
τ A i j (T' ρ (lhs e))
=[ τ=[pairᵇ]/R j _ ]
[ pairᵇ j (T' ρ (lhs e)) ]/ R i
=[ quot.eq (R i) (τεᵇ j e ρ) ]
[ pairᵇ j (T' ρ (rhs e)) ]/ R i
=[ symm (τ=[pairᵇ]/R j _) ]
τ A i j (T' ρ (rhs e))
qed
τη : ∀ i → ∀ᵇ j < i ,
((z : ∣D A ∣ j)
→
τ A i j (η z) == D′ i j z)
τη _ _ _ = refl
τσ : ∀ i → ∀ᵇ j < i , ∀ᵇ k < j ,
((a : Op Σ)
(f : Ar Σ a → T (∣D A ∣ k))
→
τ A i k (σ (a , f)) ==
τ A i j (σ (a , λ b → η (τ A j k (f b)))))
τσ i j k a f =
proof
τ A i k (σ (a , f))
=[ τ=[pairᵇ]/R k _ ]
[ pairᵇ k (σ (a , f)) ]/ R i
=[ quot.eq (R i) (τσᵇ j k a f) ]
[ pairᵇ j (σ (a , λ b → η (τ A j k (f b)))) ]/ R i
=[ symm (τ=[pairᵇ]/R j _) ]
τ A i j (σ (a , λ b → η (τ A j k (f b))))
qed
D′τ : ∀ i → ∀ᵇ j < i , ∀ᵇ k < j , (∀ t →
D′ i j (τ A j k t) == τ A i k t)
D′τ i j k t =
proof
τ A i j (η (τ A j k t))
=[ τ=[pairᵇ]/R j _ ]
[ pairᵇ j (η (τ A j k t)) ]/ R i
=[ quot.eq (R i) (τηᵇ j k t) ]
[ pairᵇ k t ]/ R i
=[ symm (τ=[pairᵇ]/R k _ ) ]
τ A i k t
qed
τD′ :
(i j : Size)
{{p : j <ᵇ i}}
(t : T (∣D A ∣ j))
→
set k ∶ Size , (⋀ q ∶ i <ᵇ k ,
τ A k j {{<ᵇ<ᵇ{{q = q}}}} t ==
τ A k i {{q}} (T' (D′ i j) t))
τD′ i j {{p}} (η x) =
let
k : Size
k = ↑ˢ i
instance
_ : j <ᵇ i
_ = p
q : i <ᵇ k
q = <ᵇ↑ˢ
_ : j <ᵇ k
_ = <ᵇ<ᵇ
in k ∣ ⋀i q
(proof
τ A k j (η x)
=[ τη k j _ ]
D′ k j x
=[ Dact k i j x ]
D′ k i (D′ i j x)
=[ symm (τη k i _) ]
τ A k i (η (D′ i j x))
qed)
τD′ i j {{p}} (σ (a , f)) =
let
g : Ar Σ a → Size
g b = el (τD′ i j (f b))
i<ᵇg : ∀ b → i <ᵇ g b
i<ᵇg b = ⋀e₁ (pf (τD′ i j (f b)))
j<ᵇg : ∀ b → j <ᵇ g b
j<ᵇg b = <ᵇ<ᵇ {{q = i<ᵇg b}}
e :
(b : Ar Σ a)
→
τ A (g b) j {{j<ᵇg b}} (f b) ==
τ A (g b) i {{i<ᵇg b}} (T' (D′ i j) (f b))
e b = ⋀e₂ (pf (τD′ i j (f b)))
k : Size
k = i ∨ˢ ⋁ˢ (ι₁ a) g
g<ᵇk : ∀ b → g b <ᵇ k
g<ᵇk b = <ᵇ<ᵇ {{q = <ᵇ∨ˢr _}} {{<ᵇ⋁ˢ g b}}
ℓ : Level
ℓ = l
l : Size
l = ↑ˢ k
instance
_ : i <ᵇ k
_ = <ᵇ∨ˢl _
_ : k <ᵇ l
_ = <ᵇ↑ˢ
q : i <ᵇ l
q = <ᵇ<ᵇ
in l ∣ (⋀i q
(proof
τ A l j (σ (a , f))
=[ τσ l k j _ _ ]
τ A l k (σ (a , λ b → η (τ A k j (f b))))
=[ ap (λ f' → τ A l k (σ (a , f'))) (funext λ b →
ap η (symm (D′τ k (g b) {{g<ᵇk b}} j {{j<ᵇg b}} _))) ]
τ A l k (σ (a , λ b → η (D′ k (g b) {{g<ᵇk b}}
(τ A (g b) j {{j<ᵇg b}} (f b)))))
=[ ap (λ h → τ A l k (σ (a , h))) (funext λ b →
ap (η {ℓ} {Σ} ∘ D′ k (g b) {{g<ᵇk b}}) (e b)) ]
τ A l k (σ (a , λ b → η (D′ k (g b) {{g<ᵇk b}}
(τ A (g b) i {{i<ᵇg b}} (T' (D′ i j) (f b))))))
=[ ap (λ h → τ A l k (σ (a , h))) (funext λ b →
ap (η {ℓ} {Σ}) (D′τ k (g b) {{g<ᵇk b}} i {{i<ᵇg b}} _ )) ]
τ A l k (σ (a , λ b → η (τ A k i (T' (D′ i j) (f b)))))
=[ symm (τσ l k i _ _) ]
τ A l i (σ (a , λ b → T' (D′ i j) (f b)))
qed)
)
D : Diag
vtx D = ∣D A ∣
edg D = D′
act D = Dact
QW : Set l
QW = colim D
instance
canSΣDiso : isIso (canS {Σ} D)
canSΣDiso = CocontinuityOfPolynomialEndofunctors.Scont Σ Γ Size ssz
(CocontinuityOfTakingPowers.isIsocan Ξ C F w C' F' w') D
AlgQW : Alg {l} {Σ} (QW)
sup {{AlgQW}} = (∫ (S∘ D) φ Coconeφ) ∘ (canS {Σ} D)⁻¹
module _ where
φ : (i : Size) → S{l}{Σ}(∣D A ∣ i) → QW
φ i s = ν D (↑ˢ i) (τ A (↑ˢ i) i {{<ᵇ↑ˢ}} (ι s))
Coconeφ : Cocone (S∘ D) φ
Coconeφ i j s =
let
k : Size
k = el (τD′ i j (ι s))
k' : Size
k' = ↑ˢ i ∨ˢ ↑ˢ j ∨ˢ k
instance
i<ᵇk : i <ᵇ k
i<ᵇk = ⋀e₁ (pf (τD′ i j (ι s)))
j<ᵇk : j <ᵇ k
j<ᵇk = <ᵇ<ᵇ
↑ˢj<ᵇk' : ↑ˢ j <ᵇ k'
↑ˢj<ᵇk' = <ᵇ<ᵇ {{q = <ᵇ∨ˢr _}} {{<ᵇ∨ˢl _}}
i<ᵇk' : i <ᵇ k'
i<ᵇk' = <ᵇ<ᵇ {{q = <ᵇ∨ˢl _}} {{<ᵇ↑ˢ}}
j<ᵇk' : j <ᵇ k'
j<ᵇk' = <ᵇ<ᵇ {{q = ↑ˢj<ᵇk'}}{{<ᵇ↑ˢ}}
k<ᵇk' : k <ᵇ k'
k<ᵇk' = <ᵇ<ᵇ {{q = <ᵇ∨ˢr _}} {{<ᵇ∨ˢr _}}
↑ˢi<ᵇk' : ↑ˢ i <ᵇ k'
↑ˢi<ᵇk' = <ᵇ∨ˢl _
e : τ A k j (ι s) == τ A k i (T' (D′ i j) (ι s))
e = ⋀e₂ (pf (τD′ i j (ι s)))
in
proof
ν D (↑ˢ j) (τ A (↑ˢ j) j {{<ᵇ↑ˢ}} (ι s))
=[ Coconeν D k' (↑ˢ j) _ ]
ν D k' (D′ k' (↑ˢ j) ((τ A (↑ˢ j) j {{<ᵇ↑ˢ}} (ι s))))
=[ ap (ν D k') (D′τ k' (↑ˢ j) j {{<ᵇ↑ˢ}} _) ]
ν D k' (τ A k' j (ι s))
=[ ap (ν D k') (symm (D′τ k' k j _)) ]
ν D k' (D′ k' k (τ A k j (ι s)))
=[ ap (ν D k' ∘ D′ k' k) e ]
ν D k' (D′ k' k (τ A k i (T' (D′ i j) (ι s))))
=[ ap (ν D k') (D′τ k' k i _) ]
ν D k' (τ A k' i (T' (D′ i j) (ι s)))
=[ ap (ν D k') (symm (D′τ k' (↑ˢ i) {{↑ˢi<ᵇk'}} i {{<ᵇ↑ˢ}} _)) ]
ν D k' (D′ k' (↑ˢ i) {{↑ˢi<ᵇk'}}
(τ A (↑ˢ i) i {{<ᵇ↑ˢ}} (T' (D′ i j) (ι s))))
=[ symm (Coconeν D k' (↑ˢ i) {{↑ˢi<ᵇk'}} _ ) ]
ν D (↑ˢ i) (τ A (↑ˢ i) i {{<ᵇ↑ˢ}} (T' (D′ i j) (ι s)))
qed
⟦⟧ν : ∀ i → ∀ᵇ j < i ,
((t : T{l}{Σ} (∣D A ∣ j))
→
⟦ t ⟧ (ν D j) == ν D i (τ A i j t))
⟦⟧ν i j (η x) =
proof
ν D j x
=[ Coconeν D i j x ]
ν D i (D′ i j x)
=[ ap (ν D i) (symm (τη _ _ _)) ]
ν D i (τ A i j (η x))
qed
⟦⟧ν i j (σ (a , f)) =
proof
∫ (S∘ D) φ Coconeφ (((canS D)⁻¹)
(a , λ b → ⟦ f b ⟧ (ν D j)))
=[ ap (λ g → ∫ (S∘ D) φ Coconeφ (((canS D)⁻¹) (a , g)))
(funext λ b → ⟦⟧ν i j (f b))
]
∫ (S∘ {Σ} D) {QW} φ Coconeφ (((canS D)⁻¹) (S' (ν D i) (a , λ b → τ A i j (f b))))
=[ ap (∫ (S∘ D) φ Coconeφ) canS⁻¹Sν ]
∫ (S∘ {Σ} D) {QW} φ Coconeφ (ν (S∘ {Σ} D) i ((a , λ b → τ A i j (f b))))
=[ refl ]
ν D (↑ˢ i) (τ A (↑ˢ i) i {{<ᵇ↑ˢ}} (T' (τ A i j) (σ (a , η ∘ f))))
=[ ap (ν D (↑ˢ i)) (symm (τσ (↑ˢ i) i {{<ᵇ↑ˢ}} j _ _)) ]
ν D (↑ˢ i) (τ A (↑ˢ i) j {{<ᵇ<ᵇ {{q = <ᵇ↑ˢ}}}} (σ (a , f)))
=[ ap (ν D (↑ˢ i)) (symm (D′τ (↑ˢ i) i {{<ᵇ↑ˢ}} j _)) ]
ν D (↑ˢ i) (D′ (↑ˢ i) i {{<ᵇ↑ˢ}} (τ A i j (σ (a , f))))
=[ symm (Coconeν D (↑ˢ i) i {{<ᵇ↑ˢ}} _) ]
ν D i (τ A i j (σ (a , f)))
qed
where
open CocontinuityOfPolynomialEndofunctors Ξ
canS⁻¹Sν :
((canS D)⁻¹) (S' (ν D i) (a , λ b → τ A i j (f b)))
===
ν (S∘ {Σ} D) i ((a , λ b → τ A i j (f b)))
canS⁻¹Sν = linv (canS D) _
satQW : Sat {l} {Σ} {ε} QW
satQW e ρ with CocontinuityOfTakingPowers.surjcan Ξ C F w C' F' w' (ι₂ e) D ρ
... | ∃i i (∃i ρi refl) =
proof
⟦ lhs e ⟧ (ν D i ∘ ρi)
=[ symm (⟦T⟧ (lhs e)) ]
⟦ T' ρi (lhs e) ⟧ (ν D i)
=[ ⟦⟧ν (↑ˢ i) i {{<ᵇ↑ˢ}} _ ]
ν D (↑ˢ i) (τ A (↑ˢ i) i {{<ᵇ↑ˢ}} (T' ρi (lhs e)))
=[ ap (ν D (↑ˢ i)) (τε (↑ˢ i) i {{<ᵇ↑ˢ}} _ _) ]
ν D (↑ˢ i) (τ A (↑ˢ i) i {{<ᵇ↑ˢ}} (T' ρi (rhs e)))
=[ symm (⟦⟧ν (↑ˢ i) i {{<ᵇ↑ˢ}} _ ) ]
⟦ T' ρi (rhs e) ⟧ (ν D i)
=[ ⟦T⟧ (rhs e) ]
⟦ rhs e ⟧ (ν D i ∘ ρi)
qed
module _
{C : Set l}
{{AlgC : Alg C}}
(satC : Sat {l} {Σ} {ε} C)
where
rec : ∀ i → ∣D A ∣ i → C
rec = λ i → fun (rec' i) ∘ coe DA=Q
module _ where
record Fun (i : Size) : Set l where
field
fun : W i / R i → C
funτ : ∀ᵇ j < i ,
((t : T (∣D A ∣ j))
→
fun ([ pairᵇ j t ]/ R i) ==
⟦ t ⟧ (fun ∘ coe DA=Q ∘ D′ i j))
open Fun public
fun∘Q′ :
(i : Size)
(hi : ∏ᵇ j < i , Fun j)
(k j : Size)
{{_ : j <ᵇ i}}
{{_ : k <ᵇ j}}
→
fun (hi k) == fun (hi j) ∘ Q′ j k
fun∘Q′ i hi = wf.ind _<_ <iswf P
λ k hk → hyp k (λ l {{l<ᵇk}} → hk l (<prf l<ᵇk))
where
P : Size → Prop l
P k =
(j : Size)
{{_ : j <ᵇ i}}
{{_ : k <ᵇ j}}
→
fun (hi k) == fun (hi j) ∘ Q′ j k
hyp : ∀ k → (∀ᵇ l < k , P l) → P k
hyp k hk j = funext (quot.ind (R k)
(λ z → fun (hi k) z == fun (hi j) (Q′ j k z))
(λ{(pairᵇ l t) →
proof
fun (hi k) ([ pairᵇ l t ]/ R k)
=[ funτ (hi k) l t ]
⟦ t ⟧ (fun (hi k) ∘ coe DA=Q ∘ D′ k l)
=[ ap (λ f → ⟦ t ⟧ (fun (hi k) ∘ f))
(funext (D′=Q′ k l)) ]
⟦ t ⟧ (fun (hi k) ∘ Q′ k l ∘ coe DA=Q)
=[ ap (λ f → ⟦ t ⟧ (f ∘ coe DA=Q))
(symm (hk l k)) ]
⟦ t ⟧ (fun (hi l) ∘ coe DA=Q)
=[ ap (λ f → ⟦ t ⟧ (f ∘ coe DA=Q)) (hk l j) ]
⟦ t ⟧ (fun (hi j) ∘ Q′ j l ∘ coe DA=Q)
=[ ap (λ f → ⟦ t ⟧ (fun (hi j) ∘ f))
(symm (funext (D′=Q′ j l))) ]
⟦ t ⟧ (fun (hi j) ∘ coe DA=Q ∘ D′ j l)
=[ symm (funτ (hi j) l t) ]
fun (hi j) ([ pairᵇ l t ]/ R j)
qed}))
rec' : ∀ i → Fun i
rec' = <rec Fun hyp
where
hyp : ∀ i → (∏ᵇ j < i , Fun j) → Fun i
hyp i hi = record { fun = funhyp ; funτ = funτhyp }
where
funhyp : W i / R i → C
funhyp = quot.lift {R = R i}
(λ{(pairᵇ j t) → ⟦ t ⟧ (fun (hi j) ∘ coe DA=Q)})
(λ{(τεᵇ j e ρ) →
proof
⟦ T' ρ (lhs e) ⟧ (fun (hi j) ∘ coe DA=Q)
=[ ⟦T⟧ (lhs e) ]
⟦ lhs e ⟧ (fun (hi j) ∘ coe DA=Q ∘ ρ)
=[ satC e (fun (hi j) ∘ coe DA=Q ∘ ρ) ]
⟦ rhs e ⟧ (fun (hi j) ∘ coe DA=Q ∘ ρ)
=[ symm ( ⟦T⟧ (rhs e)) ]
⟦ T' ρ (rhs e) ⟧ (fun (hi j) ∘ coe DA=Q)
qed
;(τηᵇ j k t) →
proof
fun (hi j) (coe DA=Q (τ A j k t))
=[ ap (fun (hi j))
(trans (τ=[pairᵇ]/R k t) (coe=== DA=Q _)) ]
fun (hi j) ([ pairᵇ k t ]/ R j)
=[ funτ (hi j) k t ]
⟦ t ⟧ (fun (hi j) ∘ coe DA=Q ∘ D′ j k)
=[ ap (λ f → ⟦ t ⟧ (fun (hi j) ∘ f))
(funext (D′=Q′ j k)) ]
⟦ t ⟧ (fun (hi j) ∘ Q′ j k ∘ coe DA=Q)
=[ ap (λ f → ⟦ t ⟧ (f ∘ coe DA=Q))
(symm (fun∘Q′ i hi k j)) ]
⟦ t ⟧ (fun (hi k) ∘ coe DA=Q)
qed
;(τσᵇ j k a f) → ap (λ f → sup (a , f)) (funext λ b →
proof
⟦ f b ⟧ (fun (hi k) ∘ coe DA=Q)
=[ ap (λ g → ⟦ f b ⟧ (g ∘ coe DA=Q))
(fun∘Q′ i hi k j) ]
⟦ f b ⟧ (fun (hi j) ∘ Q′ j k ∘ coe DA=Q)
=[ ap (λ g → ⟦ f b ⟧ (fun (hi j) ∘ g))
(symm (funext (D′=Q′ j k))) ]
⟦ f b ⟧ (fun (hi j) ∘ coe DA=Q ∘ D′ j k)
=[ symm (funτ (hi j) k _) ]
fun (hi j) ([ pairᵇ k (f b) ]/ R j)
=[ ap (fun (hi j))
(symm (trans (τ=[pairᵇ]/R k _) (coe=== DA=Q _))) ]
fun (hi j) (coe DA=Q (τ A j k (f b)))
qed)
})
funτhyp : ∀ᵇ j < i ,
((t : T (∣D A ∣ j))
→
funhyp ([ pairᵇ j t ]/ R i) ==
⟦ t ⟧ (funhyp ∘ coe DA=Q ∘ D′ i j))
funτhyp j t = ap ⟦ t ⟧ (funext λ x →
match (τ-surj j x) (λ{(∃ᵇi k (∃i t refl)) →
proof
fun (hi j) (coe DA=Q (τ A j k t))
=[ ap (fun (hi j))
(trans (τ=[pairᵇ]/R k t) (coe=== DA=Q _)) ]
fun (hi j) ([ pairᵇ k t ]/ R j)
=[ funτ (hi j) k t ]
⟦ t ⟧ (fun (hi j) ∘ coe DA=Q ∘ D′ j k)
=[ ap (λ f → ⟦ t ⟧ (fun (hi j) ∘ f))
(funext (D′=Q′ j k)) ]
⟦ t ⟧ (fun (hi j) ∘ Q′ j k ∘ coe DA=Q)
=[ ap (λ f → ⟦ t ⟧ (f ∘ coe DA=Q))
(symm (fun∘Q′ i hi k j)) ]
⟦ t ⟧ (fun (hi k) ∘ coe DA=Q)
=[ refl ]
funhyp ([ pairᵇ k t ]/ R i)
=[ ap funhyp (symm (quot.eq (R i) (τηᵇ j k _))) ]
funhyp ([ pairᵇ j (η (τ A j k t)) ]/ R i)
=[ ap funhyp (symm (trans (τ=[pairᵇ]/R j _) (coe=== DA=Q _))) ]
funhyp (coe DA=Q (τ A i j (η (τ A j k t))))
qed}))
recτ : ∀ i → ∀ᵇ j < i ,
((t : T (∣D A ∣ j))
→
rec i (τ A i j t) == ⟦ t ⟧ (rec i ∘ D′ i j))
recτ i j t =
proof
fun (rec' i) (coe DA=Q (τ A i j t))
=[ ap (fun (rec' i)) (trans (τ=[pairᵇ]/R j _) (coe=== DA=Q _)) ]
fun (rec' i) ([ pairᵇ j t ]/ R i)
=[ funτ (rec' i) j t ]
⟦ t ⟧ (rec i ∘ D′ i j)
qed
Coconerec : Cocone D rec
Coconerec = λ i j → wf.ind _<_ <iswf P hyp j i
where
P : Size → Prop l
P j =
(i : Size)
{{_ : j <ᵇ i}}
(x : ∣D A ∣ j)
→
rec j x == rec i (D′ i j x)
hyp : ∀ j → (∀ k → (k < j) → P k) → P j
hyp j h i {{j<ᵇi}} x = match (τ-surj j x)
(λ {(∃ᵇi k {{k<ᵇj}} (∃i t refl)) →
proof
rec j (τ A j k t)
=[ recτ j k t ]
⟦ t ⟧ (rec j ∘ D′ j k)
=[ ap ⟦ t ⟧ (symm (funext (h k (<prf k<ᵇj) j))) ]
⟦ t ⟧ (rec k)
=[ ap ⟦ t ⟧ (funext (h k (<prf k<ᵇj) i)) ]
⟦ t ⟧ (rec i ∘ D′ i k)
=[ symm (recτ i k t) ]
rec i (τ A i k t)
=[ ap (rec i) (symm (D′τ i j k t)) ]
rec i (D′ i j (τ A j k t))
qed
})
recQW : QW → C
recQW = ∫ D rec Coconerec
homrecQW : isHom recQW
homrecQW (a , f) =
proof
recQW ((∫ (S∘ D) φ Coconeφ) (((canS D)⁻¹) (a , f)))
=[ ap (case (((canS D)⁻¹) (a , f)))
(colimext (S∘ D)
{f = recQW ∘ ∫ (S∘ D) φ Coconeφ}
{g = sup ∘ S' recQW ∘ canS D} lemma) ]
sup (S' recQW (canS D (((canS D)⁻¹) (a , f))))
=[ ap (sup ∘ S' recQW) (rinv (canS D) (a , f)) ]
sup (S' recQW (a , f))
qed
where
lemma :
{i : Size}
(s : S{l}{Σ} (∣D A ∣ i))
→
rec (↑ˢ i) (τ A (↑ˢ i) i {{<ᵇ↑ˢ}} (ι s)) == sup (S' (recQW ∘ ν D i) s)
lemma {i} (a , f) =
proof
rec (↑ˢ i) (τ A (↑ˢ i) i {{<ᵇ↑ˢ}} (σ (a , η ∘ f)))
=[ recτ (↑ˢ i) i {{<ᵇ↑ˢ}} _ ]
sup (a , rec (↑ˢ i) ∘ D′ (↑ˢ i) i {{<ᵇ↑ˢ}} ∘ f)
=[ ap (λ g → sup (a , g ∘ f)) (funext λ z →
symm (Coconerec (↑ˢ i) i {{<ᵇ↑ˢ}} z)) ]
sup (a , rec i ∘ f)
qed
uniq< :
(h : QW → C)
(isHomh : isHom h)
(i : Size)
→
rec i == h ∘ ν D i
uniq< h isHomh = <ind P hyp
where
P : Size → Prop l
P i = rec i == h ∘ ν D i
hyp : ∀ i → (∀ᵇ j < i , P j) → P i
hyp i hi =
funext λ x →
match (τ-surj i x) (λ{(∃ᵇi j (∃i t refl)) →
proof
rec i (τ A i j t)
=[ recτ i j t ]
⟦ t ⟧ (rec i ∘ D′ i j)
=[ ap ⟦ t ⟧ (funext λ z → symm (Coconerec i j z)) ]
⟦ t ⟧ (rec j)
=[ ap ⟦ t ⟧ (hi j) ]
⟦ t ⟧ (h ∘ ν D j)
=[ symm (⟦⟧∘ (ν D j) h isHomh t) ]
h (⟦ t ⟧ (ν D j))
=[ ap h (⟦⟧ν _ _ _) ]
h (ν D i (τ A i j t))
qed})
uniqQW :
(h : QW → C)
(isHomh : isHom h)
→
recQW == h
uniqQW h isHomh =
colimext D λ x → ap (case x) (uniq< h isHomh _)