module QWI.ConstructionOfQWITypes where
open import QWI.FixedPointsAreQWITypes public
module Main
{l : Level}
{I : Set l}
(Σ : Slice.Sig I)
(ε : Slice.Syseq I Σ)
where
open Slice I
theorem : Inhabited (QWItype Σ ε)
theorem with FxSzAlg→QWIType Σ ε
... | ∃i Size (∃i ssz (inhab fixSizeStruct→QWtype)) =
inhab (fixSizeStruct→QWtype init)
where
instance
_ : SizeStructure Size
_ = ssz
open SizeIdxStruct I Σ ε Size renaming (D to dom; Dᵇ to domᵇ)
IdxStructᵇ-ext :
{i : Size}
{A A' : IdxStructᵇ i}
(_ : ∀ᵇ j < i , (domᵇ A j == domᵇ A' j))
(_ : ∀ᵇ j < i , ∀ᵇ k < j , (
(m : I)
{t : T (domᵇ A k) m}
{t' : T (domᵇ A' k) m}
(_ : t === t')
→
τᵇ A j k m t === τᵇ A' j k m t')
)
→
A == A'
IdxStructᵇ-ext e e' =
match (funᵇ-ext e) λ{refl →
match
(funᵇ-ext λ j →
funᵇ-ext λ k →
funext λ m → heq-funext refl λ p → e' j k m p
)
λ{refl → refl}}
FixSizeStructᵇ↓ᵇ :
{i : Size}
→
FixSizeStructᵇ i → ∏ᵇ j < i , FixSizeStructᵇ j
FixSizeStructᵇ↓ᵇ (D ∣ δ) j = D ↓ᵇ j ∣ (λ k → δ k)
FixSizeStructᵇ-uniq :
(i : Size)
(I I' : FixSizeStructᵇ i)
→
I == I'
FixSizeStructᵇ-uniq = <ind P hyp
where
P : Size → Prop (lsuc l)
P i = (I I' : FixSizeStructᵇ i) → I == I'
hyp : ∀ i → (∀ᵇ j < i , P j) → P i
hyp i hi I@(D ∣ δ) I'@(D' ∣ δ') =
setext (IdxStructᵇ-ext domD=domD' ΤD=τD')
where
D↓ᵇ=D'↓ᵇ : ∀ᵇ j < i , (D ↓ᵇ j == D' ↓ᵇ j)
D↓ᵇ=D'↓ᵇ j = ap el (hi j (FixSizeStructᵇ↓ᵇ I j) (FixSizeStructᵇ↓ᵇ I' j))
domD=domD' : ∀ᵇ j < i , (domᵇ D j == domᵇ D' j)
domD=domD' j =
proof
domᵇ D j
=[ funext (∧e₁ (δ j)) ]
◇ (D ↓ᵇ j)
=[ ap ◇ (D↓ᵇ=D'↓ᵇ j) ]
◇ (D' ↓ᵇ j)
=[ symm (funext (∧e₁ (δ' j))) ]
domᵇ D' j
qed
ΤD=τD' : ∀ᵇ j < i , ∀ᵇ k < j , (
(m : _)
{t : T (SizeIdxStruct.Dᵇ D k) m}
{t' : T (SizeIdxStruct.Dᵇ D' k) m}
→
t === t' → SizeIdxStruct.τᵇ D j k m t === SizeIdxStruct.τᵇ D' j k m t')
ΤD=τD' j k m {t}{t'} t=t' =
proof
τᵇ D j k m t
=[ ∧e₂ (δ j) k m t ]
[ pairᵇ k t ]/ Rᵇ (D ↓ᵇ j) m
=[ ap₂ (λ X x → [ pairᵇ k x ]/ Rᵇ X m) (D↓ᵇ=D'↓ᵇ j) t=t' ]
[ pairᵇ k t' ]/ Rᵇ (D' ↓ᵇ j) m
=[ symm (∧e₂ (δ' j) k m t') ]
τᵇ D' j k m t'
qed
initᵇ : ∀ i → FixSizeStructᵇ i
initᵇ = <rec FixSizeStructᵇ hyp
where
hyp : ∀ i → (∏ᵇ j < i , FixSizeStructᵇ j) → FixSizeStructᵇ i
hyp i hi = Di ∣ δ
where
domi : ∏ᵇ j < i , Setᴵ l
domi j m = Wᵇ (el (hi j)) m / Rᵇ (el (hi j)) m
domi< : ∀ᵇ j < i , ∀ᵇ k < j , ((m : I) → domi k m == domᵇ (el (hi j)) k m)
domi< j k m =
proof
◇ (el (hi k)) m
=[ ap (λ f → (◇ ∘ el) f m) (FixSizeStructᵇ-uniq k (hi k) (FixSizeStructᵇ↓ᵇ (hi j) k)) ]
◇ (el (hi j) ↓ᵇ k) m
=[ symm (∧e₁ (pf (hi j) k) m) ]
domᵇ (el (hi j)) k m
qed
τi : ∏ᵇ j < i , ∏ᵇ k < j , (T{Σ}(domi k) ⇁ domi j)
τi j k m t = [ pairᵇ k (T' (λ n → coe (domi< j k n)) m t) ]/ Rᵇ (el (hi j)) m
τi< :
∀ᵇ j < i , ∀ᵇ k < j , ∀ᵇ l < k ,
((m : I)
{t : T{Σ = Σ}(domi l) m}
{t' : T (domᵇ (el (hi j)) l) m}
(_ : t === t')
→
τi k l m t === τᵇ (el (hi j)) k l m t')
τi< j k l m {t} {t'} t=t' =
proof
[ pairᵇ l (T' (λ n → coe (domi< k l n)) m t) ]/ Rᵇ (el (hi k)) m
=[ ap₂ (λ X x → [ pairᵇ l x ]/ Rᵇ (el X) m)
(FixSizeStructᵇ-uniq k (hi k) (FixSizeStructᵇ↓ᵇ (hi j) k))
(lemma e (funext λ n → domi< k l n) m t=t')
]
[ pairᵇ l t' ]/ Rᵇ ((el (hi j)) ↓ᵇ k) m
=[ symm (∧e₂ (pf (hi j) k) l m t') ]
τᵇ (el (hi j)) k l m t'
qed
where
e : domᵇ (el (FixSizeStructᵇ↓ᵇ (hi j) k)) l == domᵇ (el (hi k)) l
e = ap (λ X → domᵇ (el X) l)
(symm (FixSizeStructᵇ-uniq k (hi k) (FixSizeStructᵇ↓ᵇ (hi j) k)))
lemma :
{X X' X'' : Setᴵ _}
(_ : X' == X'')
(e : X == X'')
(m : I)
{u : T{Σ = Σ} X m}
{u' : T{Σ = Σ} X' m}
(_ : u === u')
→
T' (λ n → coe (ap (λ f → f n) e)) m u === u'
lemma {X} refl refl m {u} refl =
proof
T' (λ n → coe (ap (λ f → f n) {X} refl)) m u
=[ ap (λ f → T' (λ n → f n) m u) (funext λ n → funext coerefl) ]
T' idᴵ m u
=[ symm (T'id m u) ]
u
qed
Di : IdxStructᵇ i
Di = mkIdxStructᵇ domi τi
Di↓ᵇ : ∀ᵇ j < i , (Di ↓ᵇ j == el (hi j))
Di↓ᵇ j = IdxStructᵇ-ext
(λ i → funext λ m → domi< j i m)
(τi< j)
domi↓ᵇ : ∀ᵇ j < i , (domi j == ◇ (Di ↓ᵇ j))
domi↓ᵇ j = ap ◇ (symm (Di↓ᵇ j))
δ : isFixSizeStructᵇ i Di
δ j = ∧i
(λ n → ap (λ f → f n) (domi↓ᵇ j))
(λ k m t →
(proof
[ pairᵇ k (T' (λ n → coe (domi< j k n)) m t) ]/ Rᵇ (el (hi j)) m
=[ ap₂ (λ X x → [ pairᵇ k x ]/ Rᵇ X m)
(symm (Di↓ᵇ j))
(lemma (funext λ n → domi< j k n) m)
]
[ pairᵇ k t ]/ Rᵇ (Di ↓ᵇ j) m
qed)
)
where
lemma :
{X X' : Setᴵ _}
(e : X == X')
(m : I)
{u : T{Σ = Σ} X m}
→
T' (λ n → coe (ap (λ f → f n) e)) m u === u
lemma {X} refl m {u} =
proof
T' (λ n → coe (ap (λ f → f n) {X} refl)) m u
=[ ap (λ f → T' f m u) (funext λ n → funext coerefl) ]
T' idᴵ m u
=[ symm (T'id m u) ]
u
qed
FixSizeStructᵇ↓ᵇ-uniq : ∀ i → ∀ᵇ j < i ,
(initᵇ j == FixSizeStructᵇ↓ᵇ (initᵇ i) j)
FixSizeStructᵇ↓ᵇ-uniq i j =
FixSizeStructᵇ-uniq j (initᵇ j) (FixSizeStructᵇ↓ᵇ (initᵇ i) j)
init : FixSizeStruct
init = D ∣ δ
where
Q : Size → Setᴵ l
Q i = ◇ (el (initᵇ i))
Q< : ∀ i → ∀ᵇ j < i , (Q j == domᵇ (el (initᵇ i)) j)
Q< i j =
proof
◇ (el (initᵇ j))
=[ ap (◇ ∘ el) (FixSizeStructᵇ↓ᵇ-uniq i j) ]
◇ (el (initᵇ i) ↓ᵇ j)
=[ symm (funext λ n → ∧e₁ (pf (initᵇ i) j) n) ]
domᵇ (el (initᵇ i)) j
qed
D : IdxStruct
dom D = Q
τ D i j m t =
[ pairᵇ j (T' (λ n → coe (ap (λ f → f n)
(Q< i j))) m t) ]/ Rᵇ(el (initᵇ i)) m
D↓ : ∀ i → D ↓ i == el (initᵇ i)
D↓ i = IdxStructᵇ-ext (Q< i) λ j k m {t}{t'} t=t' →
proof
[ pairᵇ k (T' (λ n → coe (ap (λ f → f n)
(Q< j k))) m t) ]/ Rᵇ (el (initᵇ j)) m
=[ ap₂ (λ X x → [ pairᵇ k x ]/ Rᵇ (el X) m)
(FixSizeStructᵇ↓ᵇ-uniq i j)
(lemma
(ap (λ X → domᵇ (el X) k) (symm (FixSizeStructᵇ↓ᵇ-uniq i j)))
(Q< j k) m t=t'
)
]
[ pairᵇ k t' ]/ Rᵇ (el (initᵇ i) ↓ᵇ j) m
=[ symm (∧e₂ (pf (initᵇ i) j) k m t') ]
τᵇ (el (initᵇ i)) j k m t'
qed
where
lemma :
{X X' X'' : Setᴵ _}
(_ : X' == X'')
(e : X == X'')
(m : I)
{u : T{Σ = Σ} X m}
{u' : T{Σ = Σ} X' m}
(_ : u === u')
→
T' (λ n → coe (ap (λ f → f n) e)) m u === u'
lemma {X} refl refl m {u} refl =
proof
T' (λ n → coe (ap (λ f → f n) {X} refl)) m u
=[ ap (λ f → T' f m u) (funext λ n → funext coerefl) ]
T' idᴵ m u
=[ symm (T'id m u) ]
u
qed
δ : ◇fix D
δ i = ∧i
(λ n → ap (λ f → f n) (Q=Qᵇ↓ i))
(λ j n t →
proof
[ pairᵇ j (T' (λ n → coe (ap (λ f → f n) (Q< i j))) n t) ]/ Rᵇ (el (initᵇ i)) n
=[ ap₂ (λ X x → [ pairᵇ j x ]/ Rᵇ X n)
(symm (D↓ i))
(lemma (Q< i j) n)
]
[ pairᵇ j t ]/ Rᵇ (D ↓ i) n
qed
)
where
Q=Qᵇ↓ : ∀ i → Q i == ◇ (D ↓ i)
Q=Qᵇ↓ i = ap ◇ (symm (D↓ i))
lemma :
{X X' : Setᴵ _}
(e : X == X')
(m : I)
{u : T{Σ = Σ} X m}
→
T' (λ n → coe (ap (λ f → f n) e)) m u === u
lemma {X} refl m {u} =
proof
T' (λ n → coe (ap (λ f → f n) {X} refl)) m u
=[ ap (λ f → T' f m u) (funext λ n → funext coerefl) ]
T' idᴵ m u
=[ symm (T'id _ _) ]
u
qed