module Colimit where
open import Axioms public
open import InitialAlgebra public
open import Prelude public
open import ThinSemiCategory public
record Diag (κ : Set){{_ : Thin κ}}(𝓒 : Set₁){{_ : CAT 𝓒}} : Set₁ where
field
V : κ → 𝓒
E : ∀ i → ∏ᵇ j < i , (V j ⟶ V i)
E∙E : ∀ i → ∀ᵇ j < i , ∀ᵇ k < j , (E i j ∙ E j k ≡ E i k)
open Diag public
record Cocomplete (𝓒 : Set₁){{_ : CAT 𝓒}} : Set₁ where
field
colim : {κ : Set}{{_ : Thin κ}} → Diag κ 𝓒 → 𝓒
inc :
{κ : Set}
{{_ : Thin κ}}
(D : Diag κ 𝓒)
(i : κ)
→
V D i ⟶ colim D
cocone :
{κ : Set}
{{_ : Thin κ}}
(D : Diag κ 𝓒)
{i : κ}
→
∀ᵇ j < i , (inc D j ≡ inc D i ∙ E D i j)
lift :
{κ : Set}
{{_ : Thin κ}}
(D : Diag κ 𝓒)
{C : 𝓒}
(f : ∀ i → V D i ⟶ C)
(_ : {i : κ} → ∀ᵇ j < i , (f j ≡ f i ∙ E D i j))
→
colim D ⟶ C
liftinc :
{κ : Set}
{{_ : Thin κ}}
(D : Diag κ 𝓒)
{C : 𝓒}
(f : ∀ i → V D i ⟶ C)
(φ : ∀{i} → ∀ᵇ j < i , (f j ≡ f i ∙ E D i j))
(i : κ)
→
f i ≡ lift D f φ ∙ inc D i
liftuniq :
{κ : Set}
{{_ : Thin κ}}
(D : Diag κ 𝓒)
{C : 𝓒}
(f : ∀ i → V D i ⟶ C)
(φ : ∀{i} → ∀ᵇ j < i , (f j ≡ f i ∙ E D i j))
{g : colim D ⟶ C}
(_ : ∀ i → f i ≡ g ∙ inc D i)
→
lift D f φ ≡ g
colimext :
{κ : Set}
{{_ : Thin κ}}
(D : Diag κ 𝓒)
{C : 𝓒}
{f g : colim D ⟶ C}
(_ : ∀ i → f ∙ inc D i ≡ g ∙ inc D i)
→
f ≡ g
colimext D {C} {f} {g} finc=ginc =
proof
f
=[ symm (liftuniq D _ φ' (λ _ → refl)) ]
lift D f' φ'
=[ liftuniq D _ φ' finc=ginc ]
g
qed
where
f' : ∀ i → V D i ⟶ C
f' i = f ∙ inc D i
φ' : ∀{i} → ∀ᵇ j < i , (f' j ≡ f' i ∙ E D i j)
φ' {i} j =
proof
f ∙ inc D j
=[ ap (f ∙_) (cocone _ _) ]
f ∙ (inc D i ∙ E D i j)
=[ symm ∙assoc ]
(f ∙ inc D i) ∙ E D i j
qed
open Cocomplete {{...}} public
infix 6 _⊙_
_⊙_ :
{𝓒 𝓓 : Set₁}
{{_ : CAT 𝓒}}
{{_ : CAT 𝓓}}
(F : 𝓒 → 𝓓)
{{_ : Functor F}}
{κ : Set}
{{_ : Thin κ}}
(D : Diag κ 𝓒)
→
Diag κ 𝓓
V (F ⊙ D) i = F (V D i)
E (F ⊙ D) i j = F ′ (E D i j)
E∙E (_⊙_ F {{func}} D) i j k =
proof
F ′ (E D i j) ∙ F ′ (E D j k)
=[ symm (act∙ {{r = func}}) ]
F ′ (E D i j ∙ E D j k)
=[ ap (F ′_) (E∙E D i j k) ]
F ′ (E D i k)
qed
can :
{𝓒 𝓓 : Set₁}
{{_ : CAT 𝓒}}
{{_ : Cocomplete 𝓒}}
{{_ : CAT 𝓓}}
{{_ : Cocomplete 𝓓}}
(F : 𝓒 → 𝓓)
{{_ : Functor F}}
{κ : Set}
{{_ : Thin κ}}
(D : Diag κ 𝓒)
→
colim (F ⊙ D) ⟶ F (colim D)
can F {{func}} D = lift (F ⊙ D) caninc caninc'
module _ where
caninc : ∀ i → F (V D i) ⟶ F (colim D)
caninc i = F ′ inc D i
caninc' : ∀{i} → ∀ᵇ j < i , (caninc j ≡ caninc i ∙ F ′ (E D i j))
caninc' {i} j =
proof
F ′ (inc D j)
=[ ap (F ′_) (cocone D j) ]
F ′ (inc D i ∙ E D i j)
=[ act∙ {{r = func}} ]
F ′ (inc D i) ∙ F ′ (E D i j)
qed
Cocontinuous :
(κ : Set)
{{_ : Thin κ}}
{𝓒 𝓓 : Set₁}
{{_ : CAT 𝓒}}
{{_ : CAT 𝓓}}
{{_ : Cocomplete 𝓒}}
{{_ : Cocomplete 𝓓}}
(F : 𝓒 → 𝓓)
{{_ : Functor F}}
→
Prop₁
Cocontinuous κ {𝓒} F = (D : Diag κ 𝓒) → Iso (can F D)
record Diagᵇ
{κ : Set}
{{_ : Thin κ}}
(i : κ)
(𝓒 : Set₁)
{{_ : CAT 𝓒}}
:
Set₁
where
field
Vᵇ : ∏ᵇ j < i , 𝓒
Eᵇ : ∏ᵇ j < i , ∏ᵇ k < j , (Vᵇ k ⟶ Vᵇ j)
Eᵇ∙Eᵇ : ∀ᵇ j < i , ∀ᵇ k < j , ∀ᵇ l < k ,
(Eᵇ j k ∙ Eᵇ k l ≡ Eᵇ j l)
open Diagᵇ public
Diagᵇext :
{κ : Set}
{{_ : Thin κ}}
{𝓒 : Set₁}
{{_ : CAT 𝓒}}
{i : κ}
{D D' : Diagᵇ i 𝓒}
(_ : ∀ᵇ j < i , (Vᵇ D j ≡ Vᵇ D' j))
(_ : ∀ᵇ j < i , ∀ᵇ k < j , (Eᵇ D j k ≣ Eᵇ D' j k))
→
D ≡ D'
Diagᵇext {i = i} {D} {D'} v e =
match VᵇD=VᵇD' \ where
refl → match EᵇD=EᵇD' \ where
refl → refl
where
VᵇD=VᵇD' : Vᵇ D ≡ Vᵇ D'
VᵇD=VᵇD' = funext \
j → instance-funexp \
p → v j {{p}}
EᵇD=EᵇD' : Eᵇ D ≣ Eᵇ D'
EᵇD=EᵇD' = match VᵇD=VᵇD' \ where
refl → funext \
j → instance-funexp \
p → funext \
k → instance-funexp \
q → e j {{p}} k {{q}}
infixl 6 _⇂_
_⇂_ :
{κ : Set}
{{_ : Thin κ}}
{𝓒 : Set₁}
{{_ : CAT 𝓒}}
(D : Diag κ 𝓒)
(i : κ)
→
Diagᵇ i 𝓒
Vᵇ (D ⇂ _) j = V D j
Eᵇ (D ⇂ _) j k = E D j k
Eᵇ∙Eᵇ (D ⇂ _) j k l = E∙E D j k l
infixl 6 _⇂ᵇ_
_⇂ᵇ_ :
{κ : Set}
{{_ : Thin κ}}
{𝓒 : Set₁}
{{_ : CAT 𝓒}}
{i : κ}
(D : Diagᵇ i 𝓒)
(j : κ)
{{_ : j <ᵇ i}}
→
Diagᵇ j 𝓒
Vᵇ (D ⇂ᵇ j) = (Vᵇ D) ↓ᵇ j
Eᵇ (D ⇂ᵇ j) = (Eᵇ D) ↓ᵇ j
Eᵇ∙Eᵇ (D ⇂ᵇ j) k l m = Eᵇ∙Eᵇ D k l m
⇂ᵇ∙⇂ᵇ :
{κ : Set}
{{_ : Thin κ}}
{𝓒 : Set₁}
{{_ : CAT 𝓒}}
{i : κ}
(D : Diagᵇ i 𝓒)
(j k : κ)
{{_ : j <ᵇ i}}
{{_ : k <ᵇ j}}
→
(D ⇂ᵇ j) ⇂ᵇ k ≡ D ⇂ᵇ k
⇂ᵇ∙⇂ᵇ D j k = Diagᵇext (λ _ → refl) (λ _ _ → refl)
infix 6 _⊙ᵇ_
_⊙ᵇ_ :
{𝓒 𝓓 : Set₁}
{{_ : CAT 𝓒}}
{{_ : CAT 𝓓}}
(F : 𝓒 → 𝓓)
{{_ : Functor F}}
{κ : Set}
{{_ : Thin κ}}
{i : κ}
→
Diagᵇ i 𝓒 → Diagᵇ i 𝓓
Vᵇ (F ⊙ᵇ D) j = F (Vᵇ D j)
Eᵇ (F ⊙ᵇ D) j k = F ′ (Eᵇ D j k)
Eᵇ∙Eᵇ (_⊙ᵇ_ F {{func}} D) j k l =
proof
F ′ (Eᵇ D j k) ∙ F ′ (Eᵇ D k l)
=[ symm (act∙ {{r = func}}) ]
F ′ (Eᵇ D j k ∙ Eᵇ D k l)
=[ ap (F ′_) (Eᵇ∙Eᵇ D j k l) ]
F ′ (Eᵇ D j l)
qed
Dwn : (κ : Set){{_ : Thin κ}} → κ → Set
Dwn κ i = set j ∶ κ , (j < i)
dwn : {κ : Set}{{_ : Thin κ}}{i : κ} → ∏ᵇ j < i , Dwn κ i
dwn j {{p}} = j ∣ <prf p
instance
ThinDwn :
{κ : Set}
{{_ : Thin κ}}
{i : κ}
→
Thin (Dwn κ i)
_<_ {{ThinDwn}} k j = el k < el j
<< {{ThinDwn}} q p = << q p
diagᵇ :
{κ : Set}
{{_ : Thin κ}}
{i : κ}
{𝓒 : Set₁}
{{_ : CAT 𝓒}}
(D : Diagᵇ i 𝓒)
→
Diag (Dwn κ i) 𝓒
V (diagᵇ D) j =
Vᵇ D (el j) {{<inst (pf j)}}
E (diagᵇ D) j k {{<inst p}} =
Eᵇ D (el j) {{<inst (pf j)}} (el k) {{<inst p}}
E∙E (diagᵇ D) j k {{<inst p}} l {{<inst q}} =
Eᵇ∙Eᵇ D (el j) {{<inst (pf j)}} (el k) {{<inst p}} (el l) {{<inst q}}
colimᵇ :
{κ : Set}
{{_ : Thin κ}}
(i : κ)
{𝓒 : Set₁}
{{_ : CAT 𝓒}}
{{_ : Cocomplete 𝓒}}
→
Diagᵇ i 𝓒 → 𝓒
colimᵇ i D = colim (diagᵇ D)
incᵇ :
{κ : Set}
{{_ : Thin κ}}
{i : κ}
{𝓒 : Set₁}
{{_ : CAT 𝓒}}
{{_ : Cocomplete 𝓒}}
(D : Diagᵇ i 𝓒)
→
∏ᵇ j < i , (Vᵇ D j ⟶ colimᵇ i D)
incᵇ D j = inc (diagᵇ D) (dwn j)
coconeincᵇ :
{κ : Set}
{{_ : Thin κ}}
{i : κ}
{𝓒 : Set₁}
{{_ : CAT 𝓒}}
{{_ : Cocomplete 𝓒}}
(D : Diagᵇ i 𝓒)
→
∀ᵇ j < i , ∀ᵇ k < j , (incᵇ D k ≡ incᵇ D j ∙ Eᵇ D j k)
coconeincᵇ D j k {{p}} = cocone (diagᵇ D) (dwn k) {{<inst (<prf p)}}
module _
{κ : Set}
{{_ : Thin κ}}
{i : κ}
{𝓒 : Set₁}
{{_ : CAT 𝓒}}
{{_ : Cocomplete 𝓒}}
(D : Diagᵇ i 𝓒)
{C : 𝓒}
(f : ∏ᵇ j < i , (Vᵇ D j ⟶ C))
(φ : ∀ᵇ j < i , ∀ᵇ k < j , (f k ≡ f j ∙ Eᵇ D j k))
where
private
f' : ((j ∣ p) : Dwn κ i) → (Vᵇ D j {{<inst p}} ⟶ C)
f' (j ∣ p) = f j {{<inst p}}
φ' : {j : Dwn κ i} → ∀ᵇ k < j , (f' k ≡ f' j ∙ E (diagᵇ D) j k )
φ' {j ∣ p} (k ∣ _) {{<inst r}} = φ j {{<inst p}} k {{<inst r}}
liftᵇ : colimᵇ i D ⟶ C
liftᵇ = lift (diagᵇ D) f' φ'
liftincᵇ : ∀ᵇ j < i , (f j ≡ liftᵇ ∙ incᵇ D j)
liftincᵇ j = liftinc (diagᵇ D) f' φ' (dwn j)
liftuniqᵇ :
(g : colimᵇ i D ⟶ C)
(ψ : ∀ᵇ j < i , (f j ≡ g ∙ incᵇ D j))
→
liftᵇ ≡ g
liftuniqᵇ g ψ =
liftuniq (diagᵇ D) f' φ' {g} λ{(j ∣ p) → ψ j {{<inst p}}}
colimextᵇ :
{κ : Set}
{{_ : Thin κ}}
{i : κ}
{𝓒 : Set₁}
{{_ : CAT 𝓒}}
{{_ : Cocomplete 𝓒}}
(D : Diagᵇ i 𝓒)
{C : 𝓒}
{f g : colimᵇ i D ⟶ C}
(_ : ∀ᵇ j < i , (f ∙ incᵇ D j ≡ g ∙ incᵇ D j))
→
f ≡ g
colimextᵇ {κ} {i} D e = colimext (diagᵇ D) λ{(j ∣ p) → e j {{<inst p}}}
colimᵇ⇂ :
{κ : Set}
{{_ : Thin κ}}
(i j : κ)
{{_ : j <ᵇ i}}
{𝓒 : Set₁}
{{_ : CAT 𝓒}}
{{_ : Cocomplete 𝓒}}
(D : Diagᵇ i 𝓒)
→
colimᵇ j (D ⇂ᵇ j) ⟶ colimᵇ i D
colimᵇ⇂ i j D = liftᵇ (D ⇂ᵇ j)
(λ k → incᵇ D k)
(λ k l → coconeincᵇ D k l)
colimᵇ⇂incᵇ :
{κ : Set}
{{_ : Thin κ}}
(i j k : κ)
{{_ : j <ᵇ i}}
{{_ : k <ᵇ j}}
{𝓒 : Set₁}
{{_ : CAT 𝓒}}
{{_ : Cocomplete 𝓒}}
(D : Diagᵇ i 𝓒)
→
incᵇ D k ≡ colimᵇ⇂ i j D ∙ incᵇ (D ⇂ᵇ j) k
colimᵇ⇂incᵇ i j k D = liftincᵇ (D ⇂ᵇ j)
(λ k → incᵇ D k)
(λ k l → coconeincᵇ D k l) k