-- Quotients of additive categories
{-# OPTIONS --safe #-}

module Cubical.Categories.Additive.Quotient where

open import Cubical.Algebra.AbGroup.Base
open import Cubical.Categories.Additive.Base
open import Cubical.Categories.Additive.Properties
open import Cubical.Categories.Category.Base
open import Cubical.Categories.Constructions.Quotient
open import Cubical.Categories.Limits.Terminal
open import Cubical.Foundations.Prelude
open import Cubical.HITs.SetQuotients renaming ([_] to ⟦_⟧)

private
  variable
    ℓ ℓ' ℓq : Level

-- Quotients of preadditive categories
module _ (C : PreaddCategory ℓ ℓ') where
  open PreaddCategory C
  open PreaddCategoryTheory C

  module _ (_~_ : {x y : ob} (f g : Hom[ x , y ] ) → Type ℓq)
           (~refl : {x y : ob} (f : Hom[ x , y ] ) → f ~ f)
           (~cong⋆ : {x y z : ob}
                     (f f' : Hom[ x , y ]) → f ~ f'
                   → (g g' : Hom[ y , z ]) → g ~ g'
                   → (f ⋆ g) ~ (f' ⋆ g'))
           (~cong+ : {x y : ob} (f f' g g' : Hom[ x , y ])
                   → f ~ f' → g ~ g' → (f + g) ~ (f' + g'))
           (~cong- : {x y : ob} (f f' : Hom[ x , y ])
                   → f ~ f' → (- f) ~ (- f'))           where

    private
      C/~ = QuotientCategory cat _~_ ~refl ~cong⋆
      Hom[_,_]/~ = λ (x y : ob) → (Hom[ x , y ]) / _~_
      _⋆/~_ = C/~ .Category._⋆_

      _+/~_ : {x y : ob} (f g : Hom[ x , y ]/~) → Hom[ x , y ]/~
      _+/~_ = setQuotBinOp ~refl ~refl _+_ ~cong+

    -- Quotient group structure on homsets
    private
      open AbGroupStr renaming (_+_ to add; -_ to inv)
      homAbStr/~ : (x y : ob) → AbGroupStr Hom[ x , y ]/~
      homAbStr/~ x y .0g        = ⟦ 0h ⟧
      homAbStr/~ x y .add       = _+/~_
      homAbStr/~ x y .inv       = (setQuotUnaryOp -_ ~cong-)
      homAbStr/~ x y .isAbGroup = makeIsAbGroup squash/
          (elimProp3 (λ _ _ _ → squash/ _ _)  λ _ _ _ → cong ⟦_⟧ (+assoc _ _ _))
          (elimProp  (λ _     → squash/ _ _)  λ _     → cong ⟦_⟧ (+idr _))
          (elimProp  (λ _     → squash/ _ _)  λ _     → cong ⟦_⟧ (+invr _))
          (elimProp2 (λ _ _   → squash/ _ _)  λ _ _   → cong ⟦_⟧ (+comm _ _))

    -- Distributivity
    ⋆distl+/~ : {x y z : ob} → (f : Hom[ x , y ]/~) → (g g' : Hom[ y , z ]/~) →
        f  ⋆/~  (g  +/~  g')  ≡  (f  ⋆/~  g)  +/~  (f  ⋆/~  g')
    ⋆distl+/~ = elimProp3 (λ _ _ _ → squash/ _ _) λ _ _ _ → cong ⟦_⟧ (⋆distl+ _ _ _)

    ⋆distr+/~ : {x y z : ob} → (f f' : Hom[ x , y ]/~) → (g : Hom[ y , z ]/~) →
        (f  +/~  f')  ⋆/~  g  ≡  (f  ⋆/~  g)  +/~  (f'  ⋆/~  g)
    ⋆distr+/~ = elimProp3 (λ _ _ _ → squash/ _ _) λ _ _ _ → cong ⟦_⟧ (⋆distr+ _ _ _)


    -- Quotient of preadditive category
    open PreaddCategory
    open PreaddCategoryStr
    PreaddQuotient : PreaddCategory ℓ (ℓ-max ℓ' ℓq)
    PreaddQuotient .cat = QuotientCategory (cat C) _~_ ~refl ~cong⋆
    PreaddQuotient .preadd .homAbStr = homAbStr/~
    PreaddQuotient .preadd .⋆distl+ = ⋆distl+/~
    PreaddQuotient .preadd .⋆distr+ = ⋆distr+/~


-- Quotients of additive categories
module _ (A : AdditiveCategory ℓ ℓ') where
  open AdditiveCategory A

  module _ (_~_ : {x y : ob} (f g : Hom[ x , y ] ) → Type ℓq)
           (~refl : {x y : ob} (f : Hom[ x , y ] ) → f ~ f)
           (~cong⋆ : {x y z : ob}
                     (f f' : Hom[ x , y ]) → f ~ f'
                   → (g g' : Hom[ y , z ]) → g ~ g'
                   → (f ⋆ g) ~ (f' ⋆ g'))
           (~cong+ : {x y : ob} (f f' g g' : Hom[ x , y ])
                   → f ~ f' → g ~ g' → (f + g) ~ (f' + g'))
           (~cong- : {x y : ob} (f f' : Hom[ x , y ])
                   → f ~ f' → (- f) ~ (- f'))           where

    private
      A/~ = PreaddQuotient preaddcat _~_ ~refl ~cong⋆ ~cong+ ~cong-

    -- Zero object
    open ZeroObject
    zero/~ : ZeroObject A/~
    zero/~ .z = zero .z
    zero/~ .zInit = isInitial/~ cat _~_ ~refl ~cong⋆ (zInit zero)
    zero/~ .zTerm = isTerminal/~ cat _~_ ~refl ~cong⋆ (zTerm zero)

    -- Biproducts
    module _ (x y : ob) where
      open Biproduct
      open IsBiproduct

      biprod/~ : Biproduct A/~ x y
      biprod/~ .x⊕y = x ⊕ y
      biprod/~ .i₁ = ⟦ i₁ (biprod x y) ⟧
      biprod/~ .i₂ = ⟦ i₂ (biprod x y) ⟧
      biprod/~ .π₁ = ⟦ π₁ (biprod x y) ⟧
      biprod/~ .π₂ = ⟦ π₂ (biprod x y) ⟧
      biprod/~ .isBipr .i₁⋆π₁ = cong ⟦_⟧ (i₁⋆π₁ (biprod x y))
      biprod/~ .isBipr .i₁⋆π₂ = cong ⟦_⟧ (i₁⋆π₂ (biprod x y))
      biprod/~ .isBipr .i₂⋆π₁ = cong ⟦_⟧ (i₂⋆π₁ (biprod x y))
      biprod/~ .isBipr .i₂⋆π₂ = cong ⟦_⟧ (i₂⋆π₂ (biprod x y))
      biprod/~ .isBipr .∑π⋆i  = cong ⟦_⟧ (∑π⋆i  (biprod x y))


    open AdditiveCategoryStr
    AdditiveQuotient : AdditiveCategory ℓ (ℓ-max ℓ' ℓq)
    AdditiveQuotient .preaddcat = A/~
    AdditiveQuotient .addit .zero = zero/~
    AdditiveQuotient .addit .biprod = biprod/~