module SizedFunctor where
open import AlgebraicSignature public
open import Colimit public
open import InflationaryIteration public
open import InitialAlgebra public
open import InitialAlgebraViaInflationaryIteration public
open import Prelude public
open import Size
module _
{𝓒 𝓓 : Set₁}
{{_ : CAT 𝓒}}
{{_ : Cocomplete 𝓒}}
{{_ : CAT 𝓓}}
{{_ : Cocomplete 𝓓}}
(F : 𝓒 → 𝓓)
{{_ : Functor F}}
where
infix 4 _hasSize_
_hasSize_ : Sig → Prop₁
_hasSize_ Σ =
(κ : Set)
{{sz : Size κ}}
{{fi : Filtered Σ κ}}
→
Cocontinuous κ F
Sized : Prop₁
Sized = ∃ Sig _hasSize_
Sized⨁ :
(A : Set)
(Σ : A → Sig)
(x : A)
→
_hasSize_ (Σ x) → _hasSize_ (⨁ A Σ)
Sized⨁ A Σ x hsx κ = hsx κ {{fi = Filtered⨁ κ A Σ x}}
Sized⊕l :
(Σ Σ' : Sig)
→
_hasSize_ Σ → _hasSize_ (Σ ⊕ Σ')
Sized⊕l Σ Σ' hs κ = hs κ {{fi = Filtered⊕l κ Σ Σ'}}
Sized⊕r :
(Σ Σ' : Sig)
→
_hasSize_ Σ' → _hasSize_ (Σ ⊕ Σ')
Sized⊕r Σ Σ' hs κ = hs κ {{fi = Filtered⊕r κ Σ Σ'}}
SizedInitialAlg :
{𝓒 : Set₁}
{{_ : CAT 𝓒}}
{{_ : Cocomplete 𝓒}}
(F : 𝓒 → 𝓒)
{{_ : Functor F}}
(Σ : Sig)
→
F hasSize Σ → InitialAlg F
SizedInitialAlg F Σ sizedΣF = InitialAlgebraTheorem κ F (sizedΣF κ)
where
κ : Set
κ = plump Σ
instance
_ : Size (plump Σ)
_ = SizePlump
_ : Filtered Σ κ
_ = FilteredPlump
CocontinuousSized :
{𝓒 𝓓 : Set₁}
{{_ : CAT 𝓒}}
{{_ : Cocomplete 𝓒}}
{{_ : CAT 𝓓}}
{{_ : Cocomplete 𝓓}}
(F : 𝓒 → 𝓓)
{{_ : Functor F}}
(_ : (κ : Set){{_ : Thin κ}} → Cocontinuous κ F)
→
Sized F
CocontinuousSized F c = ∃i emp λ κ → c κ