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

open import Level using (Level; suc; _⊔_)

module Data.System.Category {c ℓ : Level} where

import Relation.Binary.Reasoning.Setoid as ≈-Reasoning

open import Algebra using (CommutativeMonoid)
open import Categories.Category using (Category)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Morphism using () renaming (_≅_ to _[_≅_])
open import Data.Setoid using (_⇒ₛ_)
open import Data.Setoid using (∣_∣)
open import Data.System.Core using (System; _≤_; ≤-trans; ≤-refl)
open import Function using (Func; _⟨$⟩_; flip)
open import Relation.Binary as Rel using (Setoid; Rel)

open Func
open System
open _≤_

private module ≈ {I : Setoid c ℓ} {O : CommutativeMonoid c ℓ} where

  private
    variable
      A B C : System I O

  _≈_ : Rel (A ≤ B) ℓ
  _≈_ {A} {B} ≤₁ ≤₂ = ⇒S ≤₁ A⇒B.≈ ⇒S ≤₂
    where
      module A⇒B = Setoid (S A ⇒ₛ S B)

  open Rel.IsEquivalence

  ≈-isEquiv : Rel.IsEquivalence (_≈_ {A} {B})
  ≈-isEquiv {B = B} .refl = S.refl B
  ≈-isEquiv {B = B} .sym a = S.sym B a
  ≈-isEquiv {B = B} .trans a b = S.trans B a b

  ≤-resp-≈ : {f h : B ≤ C} {g i : A ≤ B} → f ≈ h → g ≈ i → ≤-trans g f ≈ ≤-trans i h
  ≤-resp-≈ {_} {C} {_} {f} {h} {g} {i} f≈h g≈i {x} = begin
      ⇒S f ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ f≈h ⟩
      ⇒S h ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ cong (⇒S h) g≈i ⟩
      ⇒S h ⟨$⟩ (⇒S i ⟨$⟩ x) ∎
    where
      open ≈-Reasoning (System.S C)

open ≈ using (_≈_) public
open ≈ using (≈-isEquiv; ≤-resp-≈)

Systems[_,_] : Setoid c ℓ → CommutativeMonoid c ℓ → Category (c ⊔ suc ℓ) (c ⊔ ℓ) ℓ
Systems[ I , O ] = record
    { Obj = System I O
    ; _⇒_ = _≤_
    ; _≈_ = _≈_
    ; id = ≤-refl
    ; _∘_ = flip ≤-trans
    ; assoc = λ {D = D} → S.refl D
    ; sym-assoc = λ {D = D} → S.refl D
    ; identityˡ = λ {B = B} → S.refl B
    ; identityʳ = λ {B = B} → S.refl B
    ; identity² = λ {A = A} → S.refl A
    ; equiv = ≈-isEquiv
    ; ∘-resp-≈ = λ {f = f} {h} {g} {i} → ≤-resp-≈ {f = f} {h} {g} {i}
    }

module _
    {I : Setoid c ℓ}
    {O : CommutativeMonoid c ℓ}
    {A B : System I O}
    (let private module A = System A)
    (let private module B = System B)
    (≅S : Setoids ℓ ℓ [ A.S ≅ B.S ])
    (let private module O = CommutativeMonoid O)
    (let private module ≅S = _[_≅_] ≅S)
    (≗-fₛ : (i : ∣ I ∣) (s : ∣ A.S ∣) → ≅S.from ⟨$⟩ (A.fₛ′ i s) B.S.≈ B.fₛ′ i (≅S.from ⟨$⟩ s))
    (≗-fₒ : (s : ∣ A.S ∣) → (A.fₒ′ s) O.≈ B.fₒ′ (≅S.from ⟨$⟩ s))
  where

  private

    ≗-fₛ-≥ : ((i : ∣ I ∣) (s : ∣ B.S ∣) → ≅S.to ⟨$⟩ (B.fₛ′ i s) A.S.≈ A.fₛ′ i (≅S.to ⟨$⟩ s))
    ≗-fₛ-≥  i s = begin
        ≅S.to ⟨$⟩ (B.fₛ′ i s)                           ≈⟨ cong ≅S.to (cong (B.fₛ ⟨$⟩ i) ≅S.isoʳ) ⟨
        ≅S.to ⟨$⟩ (B.fₛ′ i (≅S.from ⟨$⟩ (≅S.to ⟨$⟩ s))) ≈⟨ cong ≅S.to (≗-fₛ i (≅S.to ⟨$⟩ s)) ⟨
        ≅S.to ⟨$⟩ (≅S.from ⟨$⟩ (A.fₛ′ i (≅S.to ⟨$⟩ s))) ≈⟨ ≅S.isoˡ ⟩
        A.fₛ′ i (≅S.to ⟨$⟩ s)                           ∎
      where
        open ≈-Reasoning A.S

    ≗-fₒ-≥ : (s : ∣ B.S ∣) → B.fₒ′ s O.≈ A.fₒ′ (≅S.to ⟨$⟩ s)
    ≗-fₒ-≥ s = begin
        B.fₒ′ s                           ≈⟨ cong B.fₒ ≅S.isoʳ ⟨
        B.fₒ′ (≅S.from ⟨$⟩ (≅S.to ⟨$⟩ s)) ≈⟨ ≗-fₒ (≅S.to ⟨$⟩ s) ⟨
        A.fₒ′ (≅S.to ⟨$⟩ s)               ∎
      where
        open ≈-Reasoning O.setoid

    A≤B : A ≤ B
    A≤B = record
        { ⇒S = ≅S.from
        ; ≗-fₛ = ≗-fₛ
        ; ≗-fₒ = ≗-fₒ
        }

    B≤A : B ≤ A
    B≤A = record
        { ⇒S = ≅S.to
        ; ≗-fₛ = ≗-fₛ-≥
        ; ≗-fₒ = ≗-fₒ-≥
        }

  mk-≅ : Systems[ I , O ] [ A ≅ B ]
  mk-≅ = record
      { from = A≤B
      ; to = B≤A
      ; iso = record { ≅S }
      }