{-# OPTIONS --without-K --safe #-}

open import Level using (Level)
module Category.Instance.Properties.FinitelyCocompletes {o ℓ e : Level} where

import Categories.Morphism.Reasoning as ⇒-Reasoning

open import Categories.Category.BinaryProducts using (BinaryProducts)
open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
open import Categories.Category.Product using (Product) renaming (_⁂_ to _⁂′_)
open import Categories.Diagram.Coequalizer using (IsCoequalizer)
open import Categories.Functor.Core using (Functor)
open import Categories.Functor using (_∘F_) renaming (id to idF)
open import Categories.Object.Coproduct using (IsCoproduct; IsCoproduct⇒Coproduct; Coproduct)
open import Categories.Object.Initial using (IsInitial)
open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes; FinitelyCocompletes-Cartesian; _×₁_)
open import Data.Product.Base using (_,_) renaming (_×_ to _×′_)
open import Functor.Exact using (IsRightExact; RightExactFunctor)
open import Level using (_⊔_; suc)

FinitelyCocompletes-CC : CartesianCategory (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
FinitelyCocompletes-CC = record
    { U = FinitelyCocompletes
    ; cartesian = FinitelyCocompletes-Cartesian
    }

module FinCoCom = CartesianCategory FinitelyCocompletes-CC
open BinaryProducts (FinCoCom.products) using (_×_; π₁; π₂; _⁂_; assocˡ) --  hiding (unique)

module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where

  private
    module 𝒞 = FinitelyCocompleteCategory 𝒞
    module 𝒞×𝒞 = FinitelyCocompleteCategory (𝒞 × 𝒞)

  open 𝒞 using ([_,_]; +-unique; i₁; i₂; _∘_; _+_; module Equiv; _⇒_; _+₁_; -+-)
  open Equiv
  module -+- = Functor -+-

  +-resp-⊥
      : {(A , B) : 𝒞×𝒞.Obj}
      → IsInitial 𝒞×𝒞.U (A , B)
      → IsInitial 𝒞.U (A + B)
  +-resp-⊥ {A , B} A,B-isInitial = record
      { ! = [ A-isInitial.! , B-isInitial.! ]
      ; !-unique = λ { f → +-unique (sym (A-isInitial.!-unique (f ∘ i₁))) (sym (B-isInitial.!-unique (f ∘ i₂))) }
      }
    where
      open IsRightExact
      open RightExactFunctor
      module A-isInitial = IsInitial (F-resp-⊥ (isRightExact (π₁ {𝒞} {𝒞})) A,B-isInitial)
      module B-isInitial = IsInitial (F-resp-⊥ (isRightExact (π₂ {𝒞} {𝒞})) A,B-isInitial)

  +-resp-+
      : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj}
        {(i₁-₁ , i₁-₂) : (A₁ ⇒ C₁) ×′ (A₂ ⇒ C₂)}
        {(i₂-₁ , i₂-₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)}
      → IsCoproduct 𝒞×𝒞.U (i₁-₁ , i₁-₂) (i₂-₁ , i₂-₂)
      → IsCoproduct 𝒞.U (i₁-₁ +₁ i₁-₂) (i₂-₁ +₁ i₂-₂)
  +-resp-+ {A₁ , A₂} {B₁ , B₂} {C₁ , C₂} {i₁-₁ , i₁-₂} {i₂-₁ , i₂-₂} isCoproduct = record
      { [_,_] = λ { h₁ h₂ → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂  , h₂ ∘ i₂ ] ] }
      ; inject₁ = inject₁
      ; inject₂ = inject₂
      ; unique = unique
      }
    where
      open IsRightExact
      open RightExactFunctor
      module Coprod₁ = Coproduct (IsCoproduct⇒Coproduct 𝒞.U (F-resp-+ (isRightExact (π₁ {𝒞} {𝒞})) isCoproduct))
      module Coprod₂ = Coproduct (IsCoproduct⇒Coproduct 𝒞.U (F-resp-+ (isRightExact (π₂ {𝒞} {𝒞})) isCoproduct))
      open 𝒞 using ([]-cong₂; []∘+₁; +-g-η; +₁∘i₁; +₁∘i₂)
      open 𝒞 using (Obj; _≈_; module HomReasoning; assoc)
      open HomReasoning
      open ⇒-Reasoning 𝒞.U
      inject₁
          : {X : Obj}
            {h₁ : A₁ + A₂ ⇒ X}
            {h₂ : B₁ + B₂ ⇒ X}
          → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₁-₁ +₁ i₁-₂) ≈ h₁
      inject₁ {_} {h₁} {h₂} = begin
          [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₁-₁ +₁ i₁-₂)  ≈⟨ []∘+₁ ⟩
          [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] ∘ i₁-₁ , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ∘ i₁-₂ ]     ≈⟨ []-cong₂ Coprod₁.inject₁ Coprod₂.inject₁ ⟩
          [ h₁ ∘ i₁ , h₁ ∘ i₂ ]                                                               ≈⟨ +-g-η ⟩
          h₁                                                                                  ∎
      inject₂
          : {X : Obj}
            {h₁ : A₁ + A₂ ⇒ X}
            {h₂ : B₁ + B₂ ⇒ X}
          → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₂-₁ +₁ i₂-₂) ≈ h₂
      inject₂ {_} {h₁} {h₂} = begin
          [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₂-₁ +₁ i₂-₂)  ≈⟨ []∘+₁ ⟩
          [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] ∘ i₂-₁ , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ∘ i₂-₂ ]     ≈⟨ []-cong₂ Coprod₁.inject₂ Coprod₂.inject₂ ⟩
          [ h₂ ∘ i₁ , h₂ ∘ i₂ ]                                                               ≈⟨ +-g-η ⟩
          h₂                                                                                  ∎
      unique
          : {X : Obj}
            {i : C₁ + C₂ ⇒ X}
            {h₁ : A₁ + A₂ ⇒ X}
            {h₂ : B₁ + B₂ ⇒ X}
            (eq₁ : i ∘ (i₁-₁ +₁ i₁-₂) ≈ h₁)
            (eq₂ : i ∘ (i₂-₁ +₁ i₂-₂) ≈ h₂)
          → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ≈ i
      unique {X} {i} {h₁} {h₂} eq₁ eq₂ = begin
          [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ≈⟨ []-cong₂ (Coprod₁.unique eq₁-₁ eq₂-₁) (Coprod₂.unique eq₁-₂ eq₂-₂) ⟩
          [ i ∘ i₁ , i ∘ i₂ ]                                               ≈⟨ +-g-η ⟩
          i                                                                 ∎
        where
          eq₁-₁ : (i ∘ i₁) ∘ i₁-₁ ≈ h₁ ∘ i₁
          eq₁-₁ = begin
              (i ∘ i₁) ∘ i₁-₁         ≈⟨ pushʳ +₁∘i₁ ⟨
              i ∘ (i₁-₁ +₁ i₁-₂) ∘ i₁ ≈⟨ pullˡ eq₁ ⟩
              h₁ ∘ i₁                 ∎
          eq₂-₁ : (i ∘ i₁) ∘ i₂-₁ ≈ h₂ ∘ i₁
          eq₂-₁ = begin
              (i ∘ i₁) ∘ i₂-₁         ≈⟨ pushʳ +₁∘i₁ ⟨
              i ∘ (i₂-₁ +₁ i₂-₂) ∘ i₁ ≈⟨ pullˡ eq₂ ⟩
              h₂ ∘ i₁                 ∎
          eq₁-₂ : (i ∘ i₂) ∘ i₁-₂ ≈ h₁ ∘ i₂
          eq₁-₂ = begin
              (i ∘ i₂) ∘ i₁-₂         ≈⟨ pushʳ +₁∘i₂ ⟨
              i ∘ (i₁-₁ +₁ i₁-₂) ∘ i₂ ≈⟨ pullˡ eq₁ ⟩
              h₁ ∘ i₂                 ∎
          eq₂-₂ : (i ∘ i₂) ∘ i₂-₂ ≈ h₂ ∘ i₂
          eq₂-₂ = begin
              (i ∘ i₂) ∘ i₂-₂         ≈⟨ pushʳ +₁∘i₂ ⟨
              i ∘ (i₂-₁ +₁ i₂-₂) ∘ i₂ ≈⟨ pullˡ eq₂ ⟩
              h₂ ∘ i₂                 ∎

  +-resp-coeq
      : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj}
        {(f₁ , f₂) (g₁ , g₂) : (A₁ ⇒ B₁) ×′ (A₂ ⇒ B₂)}
        {(h₁ , h₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)}
      → IsCoequalizer 𝒞×𝒞.U (f₁ , f₂) (g₁ , g₂) (h₁ , h₂)
      → IsCoequalizer 𝒞.U (f₁ +₁ f₂) (g₁ +₁ g₂) (h₁ +₁ h₂)
  +-resp-coeq {A₁ , A₂} {B₁ , B₂} {C₁ , C₂} {f₁ , f₂} {g₁ , g₂} {h₁ , h₂} isCoeq = record
      { equality = sym -+-.homomorphism ○ []-cong₂ (refl⟩∘⟨ Coeq₁.equality) (refl⟩∘⟨ Coeq₂.equality) ○ -+-.homomorphism
      ; coequalize = coequalize
      ; universal = universal _
      ; unique = uniq _
      }
    where
      open IsRightExact
      open RightExactFunctor
      module Coeq₁ = IsCoequalizer (F-resp-coeq (isRightExact (π₁ {𝒞} {𝒞})) isCoeq)
      module Coeq₂ = IsCoequalizer (F-resp-coeq (isRightExact (π₂ {𝒞} {𝒞})) isCoeq)
      open 𝒞 using ([]-cong₂; +₁∘i₁; +₁∘i₂; []∘+₁; +-g-η)
      open 𝒞 using (Obj; _≈_; module HomReasoning; assoc; sym-assoc)
      open 𝒞.HomReasoning
      open ⇒-Reasoning 𝒞.U

      module _ {X : Obj} {k : B₁ + B₂ ⇒ X} (eq : k ∘ (f₁ +₁ f₂) ≈ k ∘ (g₁ +₁ g₂)) where

        eq₁ : (k ∘ i₁) ∘ f₁ ≈ (k ∘ i₁) ∘ g₁
        eq₁ = begin
            (k ∘ i₁) ∘ f₁       ≈⟨ pushʳ +₁∘i₁ ⟨
            k ∘ (f₁ +₁ f₂) ∘ i₁ ≈⟨ extendʳ eq ⟩
            k ∘ (g₁ +₁ g₂) ∘ i₁ ≈⟨ pushʳ +₁∘i₁ ⟩
            (k ∘ i₁) ∘ g₁       ∎

        eq₂ : (k ∘ i₂) ∘ f₂ ≈ (k ∘ i₂) ∘ g₂
        eq₂ = begin
            (k ∘ i₂) ∘ f₂       ≈⟨ pushʳ +₁∘i₂ ⟨
            k ∘ (f₁ +₁ f₂) ∘ i₂ ≈⟨ extendʳ eq ⟩
            k ∘ (g₁ +₁ g₂) ∘ i₂ ≈⟨ pushʳ +₁∘i₂ ⟩
            (k ∘ i₂) ∘ g₂       ∎

        coequalize : C₁ + C₂ ⇒ X
        coequalize = [ Coeq₁.coequalize eq₁ , Coeq₂.coequalize eq₂ ]

        universal : k ≈ coequalize ∘ (h₁ +₁ h₂)
        universal = begin
            k                                                         ≈⟨ +-g-η ⟨
            [ k ∘ i₁ , k ∘ i₂ ]                                       ≈⟨ []-cong₂ Coeq₁.universal Coeq₂.universal ⟩
            [ Coeq₁.coequalize eq₁ ∘ h₁ , Coeq₂.coequalize eq₂ ∘ h₂ ] ≈⟨ []∘+₁ ⟨
            coequalize ∘ (h₁ +₁ h₂)                                   ∎

        uniq : {i : C₁ + C₂ ⇒ X} → k ≈ i ∘ (h₁ +₁ h₂) → i ≈ coequalize
        uniq {i} eq′ = begin
            i                   ≈⟨ +-g-η ⟨
            [ i ∘ i₁ , i ∘ i₂ ] ≈⟨ []-cong₂ (Coeq₁.unique eq₁′) (Coeq₂.unique eq₂′) ⟩
            [ Coeq₁.coequalize eq₁ , Coeq₂.coequalize eq₂ ] ∎
          where
            eq₁′ : k ∘ i₁ ≈ (i ∘ i₁) ∘ h₁
            eq₁′ = eq′ ⟩∘⟨refl ○ extendˡ +₁∘i₁
            eq₂′ : k ∘ i₂ ≈ (i ∘ i₂) ∘ h₂
            eq₂′ = eq′ ⟩∘⟨refl ○ extendˡ +₁∘i₂

module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where

  open FinCoCom using (_⇒_; _∘_; id)
  module 𝒞 = FinitelyCocompleteCategory 𝒞

  -+- : 𝒞 × 𝒞 ⇒ 𝒞
  -+- = record
      { F = 𝒞.-+-
      ; isRightExact = record
          { F-resp-⊥ = +-resp-⊥ 𝒞
          ; F-resp-+ = +-resp-+ 𝒞
          ; F-resp-coeq = +-resp-coeq 𝒞
          }
      }

  [x+y]+z : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞
  [x+y]+z = -+- ∘ (-+- ×₁ id)

  x+[y+z] : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞
  x+[y+z] = -+- ∘ (id ×₁ -+-) ∘ assocˡ