{-# OPTIONS --type-in-type #-}

module Category.AGRP where

open import Algebra.Bundles using (AbelianGroup)
open import Categories
open import Relation.Binary.Bundles

open import Relation.Binary.Structures

import Relation.Binary.Reasoning.Setoid as SetoidR

record AGrpArr (S T : AbelianGroup _ _) : Set where
  open AbelianGroup S using (_≈_; _∙_; ε; _⁻¹)

  open AbelianGroup T using () renaming (_≈_ to _≋_; _∙_ to _×_; ε to εT; _⁻¹ to _-inv)
  field
    map : AbelianGroup.Carrier S → AbelianGroup.Carrier T
    preserves-∙
      : (a b : AbelianGroup.Carrier S)
      → map (a ∙ b) ≋ map a × map b
    preserves-ε
      : map ε ≋ εT
    preserves-inv
      : (a : AbelianGroup.Carrier S)
      → map (a ⁻¹) ≋ (map a) -inv
    preserves-≈
      : (a a' : AbelianGroup.Carrier S)
      → a ≈ a'
      → map a ≋ map a'

open Category hiding (setoid)
open AGrpArr
open AbelianGroup hiding (_∙_)

AGRP : Category
AGRP .Obj = AbelianGroup _ _
AGRP ._~>_ = AGrpArr
AGRP ._≈_ {A} {B} f g = forall a → B ._≈_ (map f a) (map g a)
AGRP .≈-equiv {B = B} .IsEquivalence.refl _ = B .refl
AGRP .≈-equiv {B = B} .IsEquivalence.sym f a = B .sym (f a)
AGRP .≈-equiv {B = B} .IsEquivalence.trans f g a = B .trans (f a) (g a)
AGRP .id .map x = x
AGRP .id {A} .preserves-∙ _ _ = A .refl
AGRP .id {A} .preserves-ε = A .refl
AGRP .id {A} .preserves-inv _ = A .refl
AGRP .id .preserves-≈ a a' x = x
(AGRP ∘ g) f .map ca = g .map (f .map ca)
AGRP ._∘_ {C = C} g f .preserves-∙ a b =
  C .trans (g .preserves-≈ _ _ (preserves-∙ f _ _)) (preserves-∙ g _ _)
AGRP ._∘_ {C = C} g f .preserves-ε =
  C .trans (g .preserves-≈ _ _ (preserves-ε f )) (preserves-ε g)
AGRP ._∘_ {C = C} g f .preserves-inv a =
  C .trans (g .preserves-≈ _ _ (preserves-inv f _)) (preserves-inv g _)
AGRP ._∘_ g f .preserves-≈ a a' x = g .preserves-≈ _ _ (f .preserves-≈ _ _ x)
AGRP .∘-cong {A} {B} {C} {g} {g'} {f} {f'} geq feq a =
  begin
    g .map (f .map a)
  ≈⟨ preserves-≈ g _ _ (feq _) ⟩
    map g (f' .map a)
  ≈⟨ geq _ ⟩
    g' .map (f' .map a)
  ∎
  where open SetoidR (setoid C) public
AGRP .id-r {B = B} f a = B .refl
AGRP .id-l {B = B} f a = B .refl
AGRP .∘-assoc {D = D} h g f a = D .refl