Weighted colimits - #652
Conversation
dd865d5 to
a74210d
Compare
|
|
||
| is-pointwise-weighted-colimit→is-lan | ||
| : is-pointwise-weighted-colimit C'[P[-],-] F L (λ c c' f → L.₁ f D.∘ ε .η c) | ||
| → is-lan P F L ε |
There was a problem hiding this comment.
Proving that this is pointwise is really tedious: I think that we might actually want to take is-pointwise-weighted-colimit as the definition of pointwise Kan extensions.
| module W = Functor W | ||
| module F = Functor F | ||
|
|
||
| record Weighted-cocone |
There was a problem hiding this comment.
I've got this here to be able to use it for some future comparison map equivalences, but I'm not sure if it is worth it.
| → (∀ j → (w : W ʻ j) → ψ j w ≡ ι-∐ j C.∘ ι-⊗ j w) | ||
| → (∀ j → is-indexed-coproduct C (λ _ → F.₀ j) (ι-⊗ j)) | ||
| → is-indexed-coproduct C copow ι-∐ | ||
| → is-weighted-colimit W F colim ψ |
There was a problem hiding this comment.
In hindsight, this could probably use the bundled forms of indexed coproducts.
| hiding (ΣF) | ||
| public | ||
|
|
||
| Tensor : Bifunctor (J ^op) J C |
There was a problem hiding this comment.
This is basically https://1lab.dev/Cat.Diagram.Coproduct.Copower.html#2729, but we can't use that here because (a) it imposes a universe level constraint on the copowering set and (b) requires us to have copowers of all sets and objects in
it makes sense to factor this out as some sort of Copowers-along?
1 participant
Description
This PR defines weighted colimits, and proves some basic facts about them.
Notes
This depends on #651 for some results about colimits over discrete diagrams. The prose is also still WIP, as is the stuff on pointwise weighted colimits, though some eyes would be appreciated!