{-# OPTIONS --without-K --safe #-}
open import Level
open import Categories.Category
open import Categories.Functor using (Functor; _∘F_; Endofunctor)
open import Categories.Functor.Hom
open import Categories.Diagram.Colimit

open import Data.Product

open import Colimit-Lemmas
open import Filtered

module Presentable {o β„“ fil-level}
  (π’ž : Category o β„“ β„“)
  (o' β„“' e' : Level) -- The level for the diagram schemes of interest
  (Fil : Category o' β„“' e' β†’ Set fil-level) -- some variant of 'filtered'
  where

private
  module π’ž = Category π’ž

open import Hom-Colimit-Choice π’ž
open LiftHom o' β„“' e'
open import Categories.Object.Coproduct (π’ž)
open import Categories.Morphism (π’ž)
open import Categories.Morphism.Reasoning.Core π’ž

finitary : {o'' β„“'' e'' : Level} {β„° : Category o'' β„“'' e''} (F : Functor π’ž β„°) β†’ Set _
finitary F =
  βˆ€ (π’Ÿ : Category o' β„“' e') β†’ -- forall diagram schemes
  Fil π’Ÿ β†’                     -- satisfying some notion of filteredness
  (J : Functor π’Ÿ π’ž) β†’         -- and all their diagrams
  preserves-colimit J F       -- the functor preserves all (existing) colimits

presentable : π’ž.Obj β†’ Set _
presentable X = finitary LiftHom[ X ,-] -- the hom-functor is finitary

-- presentable objects are closed under coproducts
presentable-coproduct : {A B : π’ž.Obj} β†’ (coprod : Coproduct A B) β†’
  (βˆ€ {π’Ÿ} β†’ Fil π’Ÿ β†’ filtered π’Ÿ) β†’ -- 'Fil' implies filtered
  presentable A β†’ presentable B β†’ presentable (Coproduct.A+B coprod)
presentable-coproduct {A} {B} coprod Pβ‡’filtered A-pres B-pres π’Ÿ π’Ÿ-has-P J J-colim =
  hom-colim-construct
    J-colim
    (filtered.bounds (Pβ‡’filtered π’Ÿ-has-P))
    A+B
    -- Part 1: every morphism A+B -> colim J needs to factor through the diagram:
    (Ξ» [f,g] β†’ Part1.goal [f,g])
    -- Part 2: if we have two factorizations, then they
    -- are identified within the diagram:
    Ξ» {i} [f,g] [f',g'] pr∘fgβ‰ˆpr∘fg' β†’
      let
        open Part2 i [f,g] [f',g'] pr∘fgβ‰ˆpr∘fg'
      in
      i' , (m , (m , (
          coproduct-jointly-epic coprod
            (record { case-precompose-i₁ = case1 ; case-precompose-iβ‚‚ = case2 }))))
  where
    open Coproduct coprod
    open Category π’ž
    module π’Ÿ = Category π’Ÿ
    module J = Functor J
    module J-colim = Colimit J-colim
    open has-upper-bounds (filtered.bounds (Pβ‡’filtered π’Ÿ-has-P))
    A-preserves-J = A-pres π’Ÿ π’Ÿ-has-P J J-colim
    B-preserves-J = B-pres π’Ÿ π’Ÿ-has-P J J-colim
    Hom-A-colim = Colimit-from-prop A-preserves-J
    Hom-B-colim = Colimit-from-prop B-preserves-J

    module Part1 ([f,g] : A+B β‡’ J-colim.coapex) where
        f = [f,g] ∘ i₁
        g = [f,g] ∘ iβ‚‚
        T-f : Triangle _ f
        T-f = hom-colim-choice J-colim A (A-pres π’Ÿ π’Ÿ-has-P J) f
        module T-f = Triangle T-f
        T-g : Triangle _ g
        T-g = hom-colim-choice J-colim B (B-pres π’Ÿ π’Ÿ-has-P J) g
        module T-g = Triangle T-g

        Bo = upper-bound T-f.x T-g.x
        p' = [ (J.₁ (is-above₁ _ _) ∘ T-f.p') , (J.₁ (is-aboveβ‚‚ _ _) ∘ T-g.p')  ]

        open HomReasoning
        case1 = begin
          [f,g] ∘ i₁                             β‰‘βŸ¨βŸ©
          f                                               β‰ˆβŸ¨ T-f.commutes ⟩
          J-colim.proj T-f.x ∘ T-f.p' β‰ˆΛ˜βŸ¨ J-colim.colimit-commute _ ⟩∘⟨refl ⟩
          (J-colim.proj Bo ∘ J.₁ (is-above₁ _ _)) ∘ T-f.p' β‰ˆβŸ¨ assoc ⟩
          J-colim.proj Bo ∘ (J.₁ (is-above₁ _ _) ∘ T-f.p') β‰ˆΛ˜βŸ¨ refl⟩∘⟨ inject₁ ⟩
          J-colim.proj Bo ∘ p' ∘ i₁ β‰ˆβŸ¨ sym-assoc ⟩
          (J-colim.proj Bo ∘ p') ∘ i₁
          ∎
        case2 = begin
          [f,g] ∘ iβ‚‚                            β‰ˆβŸ¨ T-g.commutes ⟩
          J-colim.proj T-g.x ∘ T-g.p' β‰ˆΛ˜βŸ¨ J-colim.colimit-commute _ ⟩∘⟨refl ⟩
          (J-colim.proj Bo ∘ J.₁ (is-aboveβ‚‚ _ _)) ∘ T-g.p' β‰ˆβŸ¨ assoc ⟩
          J-colim.proj Bo ∘ (J.₁ (is-aboveβ‚‚ _ _) ∘ T-g.p') β‰ˆΛ˜βŸ¨ refl⟩∘⟨ injectβ‚‚ ⟩
          J-colim.proj Bo ∘ p' ∘ iβ‚‚ β‰ˆβŸ¨ sym-assoc ⟩
          (J-colim.proj Bo ∘ p') ∘ iβ‚‚
          ∎
        goal : Triangle J-colim [f,g]
        goal = record {
          x = Bo ;
          p' = p' ;
          commutes = coproduct-jointly-epic coprod (record {
            case-precompose-i₁ = case1 ;
            case-precompose-iβ‚‚ = case2 })
          }
    module Part2 (i : π’Ÿ.Obj) ([f,g] [f',g'] : A+B β‡’ J.Fβ‚€ i)
                  (pr∘fgβ‰ˆpr∘fg' : J-colim.proj i ∘ [f,g] β‰ˆ J-colim.proj i ∘ [f',g']) where
      module fil = filtered (Pβ‡’filtered π’Ÿ-has-P)
      open HomReasoning

      f = [f,g] ∘ i₁
      g = [f,g] ∘ iβ‚‚
      f' = [f',g'] ∘ i₁
      g' = [f',g'] ∘ iβ‚‚
      pr∘fβ‰ˆpr∘f' : J-colim.proj i ∘ ([f,g] ∘ i₁) β‰ˆ J-colim.proj i ∘ ([f',g'] ∘ i₁)
      pr∘fβ‰ˆpr∘f' = extendΚ³ pr∘fgβ‰ˆpr∘fg'
      i-u-f-f'-prop =
        hom-colim-unique-factor J-colim (Pβ‡’filtered π’Ÿ-has-P)
              A A-preserves-J _ _ pr∘fβ‰ˆpr∘f'
      i-f = proj₁ i-u-f-f'-prop
      u-f = proj₁ (projβ‚‚ i-u-f-f'-prop)
      u-f' = proj₁ (projβ‚‚(projβ‚‚ i-u-f-f'-prop))
      u-f∘fβ‰ˆu-f'∘f' = (projβ‚‚(projβ‚‚(projβ‚‚ i-u-f-f'-prop)))

      Mf = fil.merge-all u-f u-f'
      module Mf = MergedMorphisms Mf
      v-f = Mf.merge π’Ÿ.∘ u-f
      v-f-prop : J.₁ v-f ∘ f β‰ˆ J.₁ v-f ∘ f'
      v-f-prop =
        begin
        J.₁ v-f ∘ f         β‰ˆβŸ¨ J.homomorphism ⟩∘⟨refl ⟩
        (J.₁ Mf.merge ∘ J.₁ u-f) ∘ f    β‰ˆβŸ¨ extendΛ‘ u-f∘fβ‰ˆu-f'∘f' ⟩
        (J.₁ Mf.merge ∘ J.₁ u-f') ∘ f'  β‰ˆΛ˜βŸ¨ J.homomorphism ⟩∘⟨refl ⟩
        J.₁ (Mf.merge π’Ÿ.∘ u-f') ∘ f'      β‰ˆΛ˜βŸ¨ J.F-resp-β‰ˆ Mf.prop ⟩∘⟨refl ⟩
        J.₁ v-f ∘ f'
        ∎

      -- same for g:
      g-unique-factor =
        hom-colim-unique-factor J-colim (Pβ‡’filtered π’Ÿ-has-P)
              B B-preserves-J g g' (extendΚ³ pr∘fgβ‰ˆpr∘fg')
      i-g = proj₁ g-unique-factor
      u-g = proj₁ (projβ‚‚ g-unique-factor)
      u-g' = proj₁ (projβ‚‚(projβ‚‚ g-unique-factor))
      u-g∘gβ‰ˆu-g'∘g' = (projβ‚‚(projβ‚‚(projβ‚‚ g-unique-factor)))
      Mg = fil.merge-all u-g u-g'
      module Mg = MergedMorphisms Mg
      v-g = Mg.merge π’Ÿ.∘ u-g
      v-g-prop : J.₁ v-g ∘ g β‰ˆ J.₁ v-g ∘ g'
      v-g-prop =
        begin
        J.₁ v-g ∘ g         β‰ˆβŸ¨ J.homomorphism ⟩∘⟨refl ⟩
        (J.₁ Mg.merge ∘ J.₁ u-g) ∘ g    β‰ˆβŸ¨ extendΛ‘ u-g∘gβ‰ˆu-g'∘g' ⟩
        (J.₁ Mg.merge ∘ J.₁ u-g') ∘ g'  β‰ˆΛ˜βŸ¨ J.homomorphism ⟩∘⟨refl ⟩
        J.₁ (Mg.merge π’Ÿ.∘ u-g') ∘ g'      β‰ˆΛ˜βŸ¨ J.F-resp-β‰ˆ Mg.prop ⟩∘⟨refl ⟩
        J.₁ v-g ∘ g'
        ∎

      -- we then merge the span v-f and v-g to one commuting square
      closed = fil.close-span v-f v-g
      module closed = ClosedSpan closed
      i' = closed.tip
      e-f = closed.close-fst
      e-g = closed.close-snd
      m = e-f π’Ÿ.∘ v-f
      case1 =
        begin
        (J.₁ m ∘ [f,g]) ∘ i₁        β‰ˆβŸ¨ assoc ⟩
        J.₁ m ∘ f          β‰ˆβŸ¨ J.homomorphism ⟩∘⟨refl ⟩
        (J.₁ e-f ∘ J.₁ v-f) ∘ f        β‰ˆβŸ¨ assoc ⟩
        J.₁ e-f ∘ (J.₁ v-f ∘ f)        β‰ˆβŸ¨ refl⟩∘⟨ v-f-prop ⟩
        J.₁ e-f ∘ (J.₁ v-f ∘ f')        β‰ˆβŸ¨ sym-assoc ⟩
        (J.₁ e-f ∘ J.₁ v-f) ∘ f'        β‰ˆΛ˜βŸ¨ J.homomorphism ⟩∘⟨refl ⟩
        J.₁ m ∘ [f',g'] ∘ i₁        β‰ˆβŸ¨ sym-assoc ⟩
        (J.₁ m ∘ [f',g']) ∘ i₁
        ∎
      case2 =
        begin
        (J.₁ m ∘ [f,g]) ∘ iβ‚‚        β‰ˆβŸ¨ assoc ⟩
        J.₁ m ∘ g          β‰ˆβŸ¨ J.F-resp-β‰ˆ closed.commutes ⟩∘⟨refl ⟩
        J.₁ (e-g π’Ÿ.∘ v-g) ∘ g          β‰ˆβŸ¨ J.homomorphism ⟩∘⟨refl ⟩
        (J.₁ e-g ∘ J.₁ v-g) ∘ g        β‰ˆβŸ¨ assoc ⟩
        J.₁ e-g ∘ (J.₁ v-g ∘ g)        β‰ˆβŸ¨ refl⟩∘⟨ v-g-prop ⟩ -- refl⟩∘⟨ v-g-prop ⟩
        J.₁ e-g ∘ (J.₁ v-g ∘ g')        β‰ˆβŸ¨ sym-assoc ⟩
        (J.₁ e-g ∘ J.₁ v-g) ∘ g'        β‰ˆΛ˜βŸ¨ J.homomorphism ⟩∘⟨refl ⟩
        J.₁ (e-g π’Ÿ.∘ v-g) ∘ [f',g'] ∘ iβ‚‚        β‰ˆΛ˜βŸ¨ J.F-resp-β‰ˆ closed.commutes ⟩∘⟨refl ⟩
        J.₁ m ∘ [f',g'] ∘ iβ‚‚        β‰ˆβŸ¨ sym-assoc ⟩
        (J.₁ m ∘ [f',g']) ∘ iβ‚‚
        ∎