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

----------------------------------------------------------------------
-- Sized functors between cocomplete categories
----------------------------------------------------------------------
module _
  {𝓒 𝓓 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  {{_ : CAT 𝓓}}
  {{_ : Cocomplete 𝓓}}
  (F : 𝓒 → 𝓓)
  {{_ : Functor F}}
  where
  infix  _hasSize_
  _hasSize_ : Sig → Prop₁
  -- F hasSize Σ if it preserves colimits indexed by any Σ-filtered size
  _hasSize_ Σ =
    (κ : Set)
    {{sz : Size κ}}
    {{fi : Filtered Σ κ}}
    → ------------------
    Cocontinuous κ F

  -- F is sized if it hasSize Σ for some Σ
  Sized : Prop₁
  Sized = ∃ Sig _hasSize_

  -- Behaviour of sizing on signature sums
  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 κ Σ Σ'}}

----------------------------------------------------------------------
-- Theorem 4.4: Sized endofunctors have initial algebras
----------------------------------------------------------------------
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

----------------------------------------------------------------------
-- Any cocontinuous functor is sized
----------------------------------------------------------------------
CocontinuousSized :
  {𝓒 𝓓 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  {{_ : CAT 𝓓}}
  {{_ : Cocomplete 𝓓}}
  (F : 𝓒 → 𝓓)
  {{_ : Functor F}}
  (_ : (κ : Set){{_ : Thin κ}} → Cocontinuous κ F)
  → ----------------------------------------------
  Sized F
CocontinuousSized F c = ∃i emp λ κ → c κ

----------------------------------------------------------------------
-- Identity functors are sized
----------------------------------------------------------------------
-- IdSized :
--   {𝓒 : Set₁}
--   {{_ : CAT 𝓒}}
--   {{_ : Cocomplete 𝓒}}
--   → -------------------------------
--   Sized (λ(X : 𝓒) → X){{FunctorId}}
-- IdSized = {!!}