module ProductsofSizedFunctors where

open import AlgebraicSignature public
open import Colimit public
open import InitialAlgebra public
open import Prelude public
open import Sets public
open import Size public
open import SizedFunctor public
open import WISC public

----------------------------------------------------------------------
-- A family of sized functors is Σ-sized for a single Σ
----------------------------------------------------------------------
SizedFamily :
  {𝓒 𝓓 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  {{_ : CAT 𝓓}}
  {{_ : Cocomplete 𝓓}}
  (X : Set)
  (F : X → 𝓒 → 𝓓)
  {{_ : ∀{x} → Functor (F x)}}
  (_ : ∀ x → Sized (F x))
  → -------------------------------
  ∃ Σ ∶ Sig , ∀ x → (F x) hasSize Σ
SizedFamily X F SizedF with WISC X ℓ₁
... | ∃i (C , D) w = match (w S p surjp) \ where
    (∃i c (∃i g surjgp)) → lemma c g surjgp
  where
  S : Set₁
  S = ∑ x ∶ X , set Σ ∶ Sig , (F x hasSize Σ)
  p : S → X
  p = π₁
  surjp : surjection p
  surjp x with SizedF x
  ... | ∃i Σ p = ∃i (x , (Σ ∣ p)) refl

  lemma :
    (c : C)
    (g : D c → S)
    (sgp : surjection (p ∘ g))
    → -------------------------------
    ∃ Σ ∶ Sig , ∀ x → (F x) hasSize Σ
  lemma c g surjgp = ∃i Σ h
    where
    Σ : Sig
    Σ = ⨁ (D c) (el ∘ π₂ ∘ g)

    h : ∀ x → F x hasSize Σ
    h x with surjgp x
    ... | ∃i x' refl =
      Sized⨁ (F x) (D c) (el ∘ π₂ ∘ g) x' (pf (π₂ (g x')))

----------------------------------------------------------------------
-- Indexed product of endofunctors on Set
----------------------------------------------------------------------
∏₁ :
  (X : Set)
  (F : X → Set → Set)
  → -----------------
  Set → Set
∏₁ X F A = ∏ x ∶ X , F x A

instance
  Functor∏₁ :
    {X : Set}
    {F : X → Set → Set}
    {{_ : ∀{x} → Functor (F x)}}
    → --------------------------
    Functor (∏₁ X F)
  act    {{Functor∏₁ {F = F}}} f g x = (F x ′ f) (g x)
  actide {{Functor∏₁ {F = F}}}       = funext \ g → funext \ x →
    ap (case (g x)) (actide {F = F x})
  act∙   {{Functor∏₁ {F = F}}}       = funext \ g → funext \ x →
    ap (case (g x)) (act∙ {F = F x})

----------------------------------------------------------------------
-- Theorem 4.13: Sized endofunctors on Set are closed under
-- indexed products
----------------------------------------------------------------------
module _
  (X : Set)
  (F : X → Set → Set)
  {{_ : ∀{x} → Functor (F x)}}
  where
  hasSize∏ :
    (Σ : Sig)
    (_ : ∀ x → (F x) hasSize Σ)
    → -------------------------
    Sized (∏₁ X F)
  hasSize∏ Σ FhasSizeΣ with WISC X ℓ₀
  ... | ∃i (A  , B ) w with IWISC (Ker (A , B) X) ℓ₀
  ... | ∃i (A' , B') w' = ∃i Σ' hasSizeΣ'
    where
    Σ' : Sig
    Σ' = Σ ⊕ sig (A , B) ⊕ sig (A' , B')

    hasSizeΣ' : (∏₁ X F) hasSize Σ'
    hasSizeΣ' κ D =
      BijisIso (can (∏₁ X F) D) (∧i injectioncan surjectioncan)
      where
      instance
        isocan : ∀{x} → Iso (can (F x) D)
        isocan {x} = Sized⊕l (F x) Σ _ (FhasSizeΣ x) κ D

      -- Proof that can (∏₁ X F) D is surjective ---------------------
      surjectioncan : surjection (can (∏₁ X F) D)
      surjectioncan f =
        match (wAC (A , B) w ∑FD (P f) (Ptotal f)) \ where
          (∃i a (∃i h (∃i sg (∧i surjh cansg)))) →
            lemma a h (π₁ ∘ sg) (π₂ ∘ sg) surjh cansg
        where
        ∑FD : X → Set
        ∑FD x = ∑ i ∶ κ , F x (V D i)

        P : ∏₁ X F (setcolim D) → ∀ x → ∑FD x → Prop
        P f x (i , z) = can (F x) D ([ i , z ]/ _) ≡ f x

        Ptotal :
          (f : ∏₁ X F (setcolim D))
          (x : X)
          → -----------------------
          ∃ y ∶ ∑FD x , P f x y
        Ptotal f x with quot.surjectionmk _ ((can (F x) D ⁻¹) (f x))
        ... | ∃i (i , z) e = ∃i (i , z)
          (proof
             can (F x) D ([ i , z ]/ _)
           =[ ap (can (F x) D ) e ]
             can (F x) D ((can (F x) D ⁻¹) (f x))
           =[ ap (case (f x)) (rinv _) ]
             f x
           qed)

        lemma :
          (a : A)
          (h : B a → X)
          (s : B a → κ)
          (g : (z : B a) → F (h z) (V D (s z)))
          (_ : surjection h)
          (_ : ∀ z → P f (h z) (s z , g z))
          → ------------------------------------------------
          ∃ y ∶ setcolim (∏₁ X F ⊙ D) , can (∏₁ X F) D y ≡ f
        lemma a h s g surjh cansg =
          match (wAC (A' , B') (w' (a , h)) (λ _ → κ) Q Qtotal) \ where
            (∃i a' (∃i h' (∃i s' (∧i surjh' e)))) →
              lemma' a' h' s' surjh' e
          where
          Q : ker h → κ → Prop
          Q ((z₁ , z₂) ∣ _) i =
            ⋀ p₁ ∶ (s z₁ <ᵇ i), ⋀ p₂ ∶ (s z₂ <ᵇ i),
            (F (h z₁) ′ E D i (s z₁) {{p₁}}) (g z₁ ) ≣
            (F (h z₂) ′ E D i (s z₂) {{p₂}}) (g z₂)

          Qtotal : ∀ x' → ∃ i ∶ κ , Q x' i
          Qtotal ((z₁ , z₂) ∣ hz₁=hz₂) =
            colimsize (F (h z₁) ⊙ D) (F (h z₂) ⊙ D)
            (ap (λ x → F x ⊙ D) hz₁=hz₂)
            (s z₁) (s z₂) (g z₁) (g z₂) p
            where
            p : [ s z₁ , g z₁ ]/ setrel (F (h z₁) ⊙ D) ≣
                [ s z₂ , g z₂ ]/ setrel (F (h z₂) ⊙ D)
            p =
              let
                y₁ = [ s z₁ , g z₁ ]/ setrel (F (h z₁) ⊙ D)
                y₂ = [ s z₂ , g z₂ ]/ setrel (F (h z₂) ⊙ D)
              in
              proof
                y₁
              =[ ap (case y₁) (symm (linv _)) ]
                ((can (F (h z₁)) D)⁻¹) (can (F (h z₁)) D y₁)
              =[ ap (can (F (h z₁)) D ⁻¹) (cansg z₁) ]
                ((can (F (h z₁)) D)⁻¹) (f (h z₁))
              =[ invCong (λ x → can (F x) D) f hz₁=hz₂ ]
                ((can (F (h z₂)) D)⁻¹) (f (h z₂))
              =[ ap (can (F (h z₂)) D ⁻¹) (symm (cansg z₂)) ]
                ((can (F (h z₂)) D)⁻¹) (can (F (h z₂)) D y₂)
              =[ ap (case y₂) (linv _) ]
                y₂
              qed

          lemma' :
            (a' : A')
            (h' : B' a' → ker h)
            (s' : B' a' → κ)
            (_ : surjection h')
            (_ : ∀ z' → Q (h' z') (s' z'))
            → ------------------------------------------------
            ∃ y ∶ setcolim (∏₁ X F ⊙ D) , can (∏₁ X F) D y ≡ f
          lemma' a' h' s' surjh' e =
            ∃i ([ i , fi ]/ setrel _) can[i,fi]
            where
            h₁ : B' a' → B a
            h₁ = π₁ ∘ el ∘ h'

            h₂ : B' a' → B a
            h₂ = π₂ ∘ el ∘ h'

            hh₁=hh₂ : ∀ z' → h (h₁ z') ≡ h (h₂ z')
            hh₁=hh₂ z' = pf (h' z')

            surjh₁h₂ : ∀ z₁ z₂ → h z₁ ≡ h z₂ →
              ∃ z' ∶ B' a' , (h₁ z' ≡ z₁ ∧ h₂ z' ≡ z₂)
            surjh₁h₂ z₁ z₂ hz₁=hz₂ with surjh' ((z₁ , z₂) ∣ hz₁=hz₂)
            ... | ∃i z' refl = ∃i z' (∧i refl refl)

            congev :
              {l : Level}
              {A A' B B' : Set l}
              {f : A → B}
              {f' : A' → B'}
              {x : A}
              {x' : A'}
              → ---------------------------------------------
              A ≡ A' → B ≡ B' → f ≣ f' → x ≣ x' → f x ≣ f' x'
            congev refl refl refl refl = refl

            i : κ
            i = ⨆ˢ (ι₂ (ι₂ a')) s'


            s'<ᵇi : ∀ z' → s' z' <ᵇ i
            s'<ᵇi z' = <ᵇ⨆ˢ s' z'

            s<ᵇi : ∀ z → s z <ᵇ i
            s<ᵇi z with surjh₁h₂ z z refl
            ... | ∃i z' (∧i refl _) = <ᵇ<ᵇ {{q = s'<ᵇi _}} {{⋀e₁ (e z')}}

            Fi : (x : X) → F x (V D i) → Prop
            Fi x y = ∃ z ∶ B a ,
              h z ≡ x ∧ (F (h z) ′ E D i (s z) {{s<ᵇi z}}) (g z) ≣ y

            ∃!XFi : ∀ x → ∃! y ∶ F x (V D i) , Fi x y
            ∃!XFi x with surjh x
            ... | ∃i z₂ refl =
              ∃i y (∧i (∃i z₂ (∧i refl refl)) λ{y' (∃i z₁ (∧i hz₁=hz₂ u)) →
              match (surjh₁h₂ z₁ z₂ hz₁=hz₂) (\ where
                (∃i z' (∧i refl refl)) →
                  let
                    x₁ = h (h₁ z')
                    x₂ = h (h₂ z')
                    j₁ = s (h₁ z')
                    j₂ = s (h₂ z')
                    k  = s' z'
                    instance
                      _ : j₁ <ᵇ k
                      _ = ⋀e₁ (e z')
                      _ : j₂ <ᵇ k
                      _ = ⋀e₁ (⋀e₂ (e z'))
                      _ : k <ᵇ i
                      _ = s'<ᵇi  z'
                  in
                  proof
                    (F x₂ ′ E D i j₂) (g (h₂ z'))
                  =[ ap (case (g (h₂ z'))) (symm (E∙E (F x₂ ⊙ D) i k j₂)) ]
                    (F x₂ ′ E D i k) ((F x₂ ′ E D k j₂) (g (h₂ z')))
                  =[ congev
                        (ap (λ x → F x (V D (s' z'))) (symm hz₁=hz₂))
                        (ap (λ x → F x (V D i)) (symm hz₁=hz₂))
                        (ap (λ x → F x ′ E D i k) (symm hz₁=hz₂))
                        (symm (⋀e₂ (⋀e₂ (e z')))) ]
                    (F x₁ ′ E D i k) ((F x₁ ′ E D k j₁) (g (h₁ z')))
                  =[ ap (case (g (h₁ z'))) (E∙E (F x₁ ⊙ D) i k j₁) ]
                  (F x₁ ′ E D i j₁) (g (h₁ z'))
                  =[ u ]
                  y'
                  qed)})
              where
              y : F x (V D i)
              y = (F (h z₂) ′ E D i (s z₂) {{s<ᵇi _}}) (g z₂)

            fi : ∏₁ X F (V D i)
            fi x = the (F x (V D i)) (Fi x) {{∃!XFi x}}

            can[i,fi] : can (∏₁ X F) D ([ i , fi ]/ setrel _) ≡ f
            can[i,fi] = funext λ x →
              match (the-pf (F x (V D i)) (Fi x) {{∃!XFi x}}) \ where
                (∃i z (∧i refl u)) →
                  let
                    instance
                      _ : s z <ᵇ i
                      _ = s<ᵇi z
                  in
                  proof
                    can (F (h z)) D ([ i , fi (h z) ]/ _)
                  =[ ap (λ y → can (F (h z)) D ([ i , y ]/ _)) (symm u) ]
                    can (F (h z)) D ([ i , (F (h z) ′ E D i (s z)) (g z) ]/ _)
                  =[ ap (can (F (h z)) D)
                     (symm (quot.eq _ (mksetrel i (s z) (g z)))) ]
                       can (F (h z)) D ([ s z , g z ]/ _)
                  =[ cansg z ]
                    f (h z) qed
      -- end of proof that can (∏₁ X F) D is surjective --------------

      -- Proof that can (∏₁ X F) D is injective ----------------------
      injectioncan : injection (can (∏₁ X F) D)
      injectioncan {z} {z'} = quot.ind₂ _ _
        (λ z z' → can (∏₁ X F) D z ≡ can (∏₁ X F) D z' → z ≡ z')
        (λ{(i , f) (j , g) e → match (injcan i j f g e) \ where
          (∃i k (⋀i p (⋀i q e'))) →
            proof
              [ i , f ]/ _
            =[ quot.eq _ (mksetrel k i {{p}} f) ]
              [ k , (λ a → (F a ′ E D k i {{p}})(f a)) ]/ setrel (∏₁ X F ⊙ D)
            =[ ap (λ h → [ k , h ]/ setrel (∏₁ X F ⊙ D)) (funext e') ]
              [ k , (λ a → (F a ′ E D k j {{q}})(g a)) ]/ setrel (∏₁ X F ⊙ D)
            =[ symm (quot.eq _ (mksetrel k j {{q}} g)) ]
              [ j , g ]/ _
            qed}) z z'
        where
        injcan :
          (i j : κ)
          (f : ∏₁ X F (V D i))
          (g : ∏₁ X F (V D j))
          (_ : can (∏₁ X F) D ([ i , f ]/ setrel _)  ≡
               can (∏₁ X F) D ([ j , g ]/ setrel _)    )
          → --------------------------------------------------------
          ∃ k ∶ κ , ⋀ p ∶ i <ᵇ k , ⋀ q ∶ j <ᵇ k , (∀ x →
            (F x ′ E D k i {{p}})(f x) ≡ (F x ′ E D k j {{q}})(g x))
        injcan i j f g e = match (wAC (A , B) w (λ _ → κ) P Ptotal) \ where
            (∃i a (∃i h (∃i u (∧i surjh v)))) → lemma a h u surjh v
          where
          P : X → κ → Prop
          P x k = ⋀ p ∶ i <ᵇ k , ⋀ q ∶ j <ᵇ k ,
            ((F x ′ E D k i {{p}})(f x) ≡ (F x ′ E D k j {{q}})(g x))

          Ptotal : ∀ x → ∃ k ∶ κ , P x k
          Ptotal x = colimsize (F x ⊙ D) _ refl i j (f x) (g x)
            (let
              instance
                _ : Iso (can (F x) D)
                _ = Sized⊕l (F x) Σ _ (FhasSizeΣ x) κ D
            in
            proof
              [ i , f x ]/ setrel (F x ⊙ D)
            =[ ap (case ([ i , f x ]/ setrel _)) (symm (linv _)) ]
              ((can (F x ) D)⁻¹) (((F x) ′ inc D i) (f x))
            =[ ap (λ h → (can (F x) D ⁻¹) (h x)) e ]
              ((can (F x ) D)⁻¹) (((F x) ′ inc D j) (g x))
            =[ ap (case ([ j , g x ]/ setrel _)) (linv _) ]
              [ j , g x ]/ _
            qed)

          lemma :
            (a : A)
            (h : B a → X)
            (u : B a → κ)
            (_ : surjection h)
            (_ : ∀ z → P (h z) (u z))
            → -------------------------------------
            ∃ k ∶ κ , ⋀ p ∶ i <ᵇ k , ⋀ q ∶ j <ᵇ k ,
              (∀ x →
                (F x ′ E D k i {{p}})(f x) ≡
                (F x ′ E D k j {{q}})(g x))
          lemma a h u surjh v =
            let
              instance
                p : i <ᵇ k
                p = <ᵇ⊔ˢl

                q : j <ᵇ k
                q = <ᵇ<ᵇ {{q = <ᵇ⊔ˢr}} {{<ᵇ⊔ˢl}}

                i<ᵇu : ∀{z} → i <ᵇ u z
                i<ᵇu {z} = ⋀e₁ (v z)

                j<ᵇu : ∀{z} → j <ᵇ u z
                j<ᵇu {z} = ⋀e₁ (⋀e₂ (v z))

                u<ᵇk : ∀{z} → u z <ᵇ k
                u<ᵇk {z} =
                  <ᵇ<ᵇ {{q = <ᵇ⊔ˢr}}
                  {{<ᵇ<ᵇ {{q = <ᵇ⊔ˢr}} {{<ᵇ⨆ˢ u z}}}}
            in
            ∃i k (⋀i p (⋀i q λ x → match (surjh x) \ where
              (∃i z refl) →
                (proof
                   (F x ′ E D k i)(f x)
                 =[ ap (case (f x)) (symm (E∙E (F x ⊙ D) k (u z) i)) ]
                   (F x ′ E D k (u z)) ((F x ′ E D (u z) i)(f x))
                 =[ ap (F x ′ E D k (u z)) (⋀e₂ (⋀e₂ (v z))) ]
                   (F x ′ E D k (u z)) ((F x ′ E D (u z) j)(g x))
                 =[ ap (case (g x)) (E∙E (F x ⊙ D) k (u z) j) ]
                   (F x ′ E D k j)(g x)
                 qed)))
            where
            k : κ
            k = i ⊔ˢ j ⊔ˢ ⨆ˢ (ι₂ (ι₁ a)) u
      -- end of proof that can (∏₁ X F) D is injective ---------------
  -- end of proof of hasSize∏ ----------------------------------------

  Sized∏ : (∀ x → Sized (F x)) → Sized (∏₁ X F)
  Sized∏ s with SizedFamily X F s
  ... | ∃i Σ hs = hasSize∏ Σ hs