{-# OPTIONS --cubical --safe #-}

module DepthComonads.Algebra where

open import DepthComonads.Level
open import DepthComonads.Path
open import DepthComonads.Function using (id; _∘_; _$_; _∘′_; flip)

module _ {a} {A : Type a} (_∙_ : A → A → A) where
  Associative : Type a
  Associative = ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)

  Commutative : Type _
  Commutative = ∀ x y → x ∙ y ≡ y ∙ x

  Idempotent : Type _
  Idempotent = ∀ x → x ∙ x ≡ x

Identityˡ : (A → B → B) → A → Type _
Identityˡ _∙_ x = ∀ y → x ∙ y ≡ y

Zeroˡ : (A → B → A) → A → Type _
Zeroˡ _∙_ x = ∀ y → x ∙ y ≡ x

Zeroʳ : (A → B → B) → B → Type _
Zeroʳ _∙_ x = ∀ y → y ∙ x ≡ x

Identityʳ : (A → B → A) → B → Type _
Identityʳ _∙_ x = ∀ y → y ∙ x ≡ y

_Distributesʳ_ : (A → B → B) → (B → B → B) → Type _
_⊗_ Distributesʳ _⊕_ = ∀ x y z → x ⊗ (y ⊕ z) ≡ (x ⊗ y) ⊕ (x ⊗ z)

_Distributesˡ_ : (B → A → B) → (B → B → B) → Type _
_⊗_ Distributesˡ _⊕_ = ∀ x y z → (x ⊕ y) ⊗ z ≡ (x ⊗ z) ⊕ (y ⊗ z)

Cancellableˡ : (A → B → C) → A → Type _
Cancellableˡ _⊗_ c = ∀ x y → c ⊗ x ≡ c ⊗ y → x ≡ y

Cancellableʳ : (A → B → C) → B → Type _
Cancellableʳ _⊗_ c = ∀ x y → x ⊗ c ≡ y ⊗ c → x ≡ y

Cancellativeˡ : (A → B → C) → Type _
Cancellativeˡ _⊗_ = ∀ c → Cancellableˡ _⊗_ c

Cancellativeʳ : (A → B → C) → Type _
Cancellativeʳ _⊗_ = ∀ c → Cancellableʳ _⊗_ c

module _ {ℓ : Level} (𝑆 : Type ℓ) where
  record  Semigroup : Type ℓ where
    infixl  _∙_
    field
      _∙_    : 𝑆 → 𝑆 → 𝑆
      assoc  : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)

  record  Monoid : Type ℓ where
    field
      _∙_    : 𝑆 → 𝑆 → 𝑆
      ε      : 𝑆
      assoc  : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)
      ε∙ : ∀ x → ε ∙ x ≡ x
      ∙ε : ∀ x → x ∙ ε ≡ x

    semigroup : Semigroup
    semigroup = record
      { _∙_ = _∙_; assoc = assoc }

    infixl  _∙_

  record Group : Type ℓ where
    field
      monoid : Monoid
    open Monoid monoid public
    field
      -_ : 𝑆 → 𝑆
      ∙⁻ : ∀ x → x ∙ - x ≡ ε
      ⁻∙ : ∀ x → - x ∙ x ≡ ε

    open import DepthComonads.Path.Reasoning

    cancelˡ : Cancellativeˡ _∙_
    cancelˡ x y z p =
      y ≡˘⟨ ε∙ y ⟩
      ε ∙ y ≡˘⟨ cong (_∙ y) (⁻∙ x) ⟩
      (- x ∙ x) ∙ y ≡⟨ assoc (- x) x y ⟩
      - x ∙ (x ∙ y) ≡⟨ cong (- x ∙_) p ⟩
      - x ∙ (x ∙ z) ≡˘⟨ assoc (- x) x z ⟩
      (- x ∙ x) ∙ z ≡⟨ cong (_∙ z) (⁻∙ x) ⟩
      ε ∙ z ≡⟨ ε∙ z ⟩
      z ∎

    cancelʳ : Cancellativeʳ _∙_
    cancelʳ x y z p =
      y ≡˘⟨ ∙ε y ⟩
      y ∙ ε ≡˘⟨ cong (y ∙_) (∙⁻ x) ⟩
      y ∙ (x ∙ - x) ≡˘⟨ assoc y x (- x) ⟩
      (y ∙ x) ∙ - x ≡⟨ cong (_∙ - x) p ⟩
      (z ∙ x) ∙ - x ≡⟨ assoc z x (- x) ⟩
      z ∙ (x ∙ - x) ≡⟨ cong (z ∙_) (∙⁻ x) ⟩
      z ∙ ε ≡⟨ ∙ε z ⟩
      z ∎

  record CommutativeMonoid : Type ℓ where
    field ⦃ monoid ⦄ : Monoid
    open Monoid monoid public
    field comm : ∀ x y → x ∙ y ≡ y ∙ x

  record Semilattice : Type ℓ where
    field commutativeMonoid : CommutativeMonoid
    open CommutativeMonoid commutativeMonoid public
    field idem : Idempotent _∙_

  record NearSemiring : Type ℓ where
    infixl  _+_
    infixl  _∗_
    field
      _+_ : 𝑆 → 𝑆 → 𝑆
      _∗_ : 𝑆 → 𝑆 → 𝑆
      𝟙 : 𝑆
      𝟘 : 𝑆
      +-assoc : Associative _+_
      ∗-assoc : Associative _∗_
      0+ : Identityˡ _+_ 𝟘
      +0 : Identityʳ _+_ 𝟘
      1∗ : Identityˡ _∗_ 𝟙
      ∗1 : Identityʳ _∗_ 𝟙
      0∗ : Zeroˡ _∗_ 𝟘
      ⟨+⟩∗ : _∗_ Distributesˡ _+_

  record Semiring : Type ℓ where
    field nearSemiring : NearSemiring
    open NearSemiring nearSemiring public
    field
      +-comm : Commutative _+_
      ∗0 : Zeroʳ _∗_ 𝟘
      ∗⟨+⟩ : _∗_ Distributesʳ _+_

  record IdempotentSemiring : Type ℓ where
    field semiring : Semiring
    open Semiring semiring public
    field +-idem : Idempotent _+_

  record CommutativeSemiring : Type ℓ where
    field semiring : Semiring
    open Semiring semiring public
    field ∗-comm : Commutative _∗_

  record StarSemiring : Type ℓ where
    field semiring : Semiring
    open Semiring semiring public
    field
      _⋆ : 𝑆 → 𝑆
      star-iterʳ : ∀ x → x ⋆ ≡ 𝟙 + x ∗ x ⋆
      star-iterˡ : ∀ x → x ⋆ ≡ 𝟙 + x ⋆ ∗ x
    _⁺ : 𝑆 → 𝑆
    x ⁺ = x ∗ x ⋆

module _ {ℓ} (𝐹 : Type ℓ → Type ℓ) where
  record Functor : Type (ℓsuc ℓ) where
    field
      map : (A → B) → 𝐹 A → 𝐹 B
      map-id : ∀ x → map (id {ℓ} {A}) x ≡ x
      map-comp : ∀ (f : B → C) (g : A → B) x → map (f ∘ g) x ≡ map f (map g x)

  record Applicative : Type (ℓsuc ℓ) where
    infixl  _<*>_
    field
      pure : A → 𝐹 A
      _<*>_ : 𝐹 (A → B) → 𝐹 A → 𝐹 B

    -- map : (A → B) → 𝐹 A → 𝐹 B
    -- map f x = ⦇ f x ⦈

    field
      identity : (v : 𝐹 A) → ⦇ id v ⦈ ≡ v
      composition : (u : 𝐹 (B → C)) (v : 𝐹 (A → B)) (w : 𝐹 A) → pure _∘′_ <*> u <*> v <*> w ≡ u <*> (v <*> w)
      homomorphism : (f : A → B) (x : A) → pure f <*> pure x ≡ pure (f x)
      interchange : (u : 𝐹 (A → B)) (y : A) → u <*> pure y ≡ pure (_$ y) <*> u

  record Monad : Type (ℓsuc ℓ) where
    infixl  _>>=_
    field
      _>>=_ : 𝐹 A → (A → 𝐹 B) → 𝐹 B
      return : A → 𝐹 A
      >>=-idˡ : (f : A → 𝐹 B) → (x : A) → (return x >>= f) ≡ f x
      >>=-idʳ : (x : 𝐹 A) → (x >>= return) ≡ x
      >>=-assoc : (xs : 𝐹 A) (f : A → 𝐹 B) (g : B → 𝐹 C) → ((xs >>= f) >>= g) ≡ (xs >>= (λ x → f x >>= g))

    _>=>_ : (A → 𝐹 B) → (B → 𝐹 C) → A → 𝐹 C
    (f >=> g) x = f x >>= g
    infixl  _<=<_

    _<=<_ : (B → 𝐹 C) → (A → 𝐹 B) → A → 𝐹 C
    _<=<_ = flip _>=>_

  record Comonad : Type (ℓsuc ℓ) where
    field
      _=>>_ : 𝐹 A → (𝐹 A → B) → 𝐹 B
      extract : 𝐹 A → A

    _<<=_ : (𝐹 A → B) → 𝐹 A → 𝐹 B
    _<<=_ = flip _=>>_

    _=>=_ : (𝐹 A → B) → (𝐹 B → C) → 𝐹 A → C
    (f =>= g) x = g (x =>> f)

    infixl  _=<=_
    _=<=_ : (𝐹 B → C) → (𝐹 A → B) → 𝐹 A → C
    _=<=_ = flip _=>=_ 

    duplicate : 𝐹 A → 𝐹 (𝐹 A)
    duplicate xs = xs =>> id

    extend : (𝐹 A → B) → 𝐹 A → 𝐹 B
    extend = _<<=_

    map : (A → B) → 𝐹 A → 𝐹 B
    map f xs = xs =>> (f ∘ extract)

    field
      =>>-idʳ : (f : 𝐹 A → B) → (f =>= extract) ≡ f
      =>>-idˡ : {B : Type ℓ} (f : 𝐹 A → B) → (extract =>= f) ≡ f
      =>>-assoc :
        ∀ {D : Type ℓ}
        (f : 𝐹 A → B)
        (g : 𝐹 B → C)
        (h : 𝐹 C → D) →
        (f =>= (g =>= h)) ≡ ((f =>= g) =>= h)

-- module _ {ℓ₁} {𝑆 : Type ℓ₁} (mon : Monoid 𝑆) where
--   open Monoid mon
--   module _ {ℓ₂ ℓ₃} (𝐹 : 𝑆 → Type ℓ₂ → Type ℓ₃) where

--     record GradedMonad : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂ ℓ⊔ ℓ₃) where
--       field
--         return  : A → 𝐹 ε A
--         _>>=_ : ∀ {x y} → 𝐹 x A → (A → 𝐹 y B) → 𝐹 (x ∙ y) B

--         >>=-idˡ : ∀ {s} (f : A → 𝐹 s B) → (x : A) → (return x >>= f) ≡[ i ≔ 𝐹 (ε∙ s i) B ]≡ (f x)
--         >>=-idʳ : ∀ {s} (x : 𝐹 s A) → (x >>= return) ≡[ i ≔ 𝐹 (∙ε s i) A ]≡ x
--         >>=-assoc : ∀ {x y z} (xs : 𝐹 x A) (f : A → 𝐹 y B) (g : B → 𝐹 z C) → ((xs >>= f) >>= g) ≡[ i ≔ 𝐹 (assoc x y z i) C ]≡ (xs >>= (λ x → f x >>= g))

--       infixr 0 proven-bind

--       proven-bind : ∀ {x y z} → 𝐹 x A → (A → 𝐹 y B) → (x ∙ y) ≡ z → 𝐹 z B
--       proven-bind xs f proof = subst (flip 𝐹 _) proof (xs >>= f)

--       syntax proven-bind xs f proof = xs >>=[ proof ] f

--       infixr 0 proven-do
--       proven-do : ∀ {x y z} → 𝐹 x A → (A → 𝐹 y B) → (x ∙ y) ≡ z → 𝐹 z B
--       proven-do = proven-bind

--       syntax proven-do xs (λ x → e) proof = x ← xs [ proof ]; e

--       map : ∀ {x} → (A → B) → 𝐹 x A → 𝐹 x B
--       map f xs = xs >>=[ ∙ε _ ] (return ∘ f)

--       _<∗>_ : ∀ {x y} → 𝐹 x (A → B) → 𝐹 y A → 𝐹 (x ∙ y) B
--       fs <∗> xs = fs >>= flip map xs

--       _>>=ε_ : ∀ {x} → 𝐹 x A → (A → 𝐹 ε B) → 𝐹 x B
--       xs >>=ε f = xs >>=[ ∙ε _ ] f

--     record GradedComonad : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂ ℓ⊔ ℓ₃) where
--       field
--         extract : 𝐹 ε A → A
--         _=>>_ : ∀ {x y} → 𝐹 (x ∙ y) A → (𝐹 y A → B) → 𝐹 x B

--       infixr 5 proven-cobind
--       proven-cobind : ∀ {x y z} → 𝐹 z A → (𝐹 y A → B) → x ∙ y ≡ z → 𝐹 x B
--       proven-cobind xs k prf = subst (flip 𝐹 _) (sym prf) xs =>> k

--       syntax proven-cobind xs f prf = xs =>> [ prf ] f

--       infixl 5 proven-cobindˡ
--       proven-cobindˡ : ∀ {x y z} → (𝐹 y A → B) → 𝐹 z A → z ≡ x ∙ y → 𝐹 x B
--       proven-cobindˡ k xs prf = subst (flip 𝐹 _) prf xs =>> k

--       syntax proven-cobindˡ f xs prf = f <<= [ prf ] xs

--       _=<=_ : ∀ {x y} → (𝐹 x B → C) → (𝐹 y A → B) → 𝐹 (x ∙ y) A → C
--       (g =<= f) x = g (x =>> f)

--       _=>=_ : ∀ {x y} → (𝐹 y A → B) → (𝐹 x B → C) → 𝐹 (x ∙ y) A → C
--       f =>= g = g =<= f

--       field
--         =>>-idʳ : ∀ {s} (f : 𝐹 s A → B) → (f =>= extract) ≡[ i ≔ (𝐹 (ε∙ s i) A → B) ]≡ f
--         =>>-idˡ : ∀ {s} {B : Type ℓ₂} (f : 𝐹 s A → B) → (extract =>= f) ≡[ i ≔ (𝐹 (∙ε s i) A → B) ]≡ f
--         =>>-assoc :
--           ∀ {D : Type ℓ₂}
--           {x y z} →
--           (f : 𝐹 x A → B)
--           (g : 𝐹 y B → C)
--           (h : 𝐹 z C → D) →
--           (f =>= (g =>= h)) ≡[ i ≔ (𝐹 (assoc z y x i) A → D) ]≡ ((f =>= g) =>= h)

--       infixr 1 codo-syntax
--       codo-syntax : ∀ {x y} → 𝐹 (x ∙ y) A → (𝐹 y A → B) → 𝐹 x B
--       codo-syntax = _=>>_

--       syntax codo-syntax xs (λ x → r) = x ↢ xs ; r

--       infixr 1 proven-codo-syntax
--       proven-codo-syntax : ∀ {x y z} → 𝐹 z A → (𝐹 y A → B) → x ∙ y ≡ z → 𝐹 x B
--       proven-codo-syntax = proven-cobind

--       syntax proven-codo-syntax xs (λ x → r) prf = x ↢ xs [ prf ]; r

--       map : ∀ {x} → (A → B) → 𝐹 x A → 𝐹 x B
--       map f xs =
--         x ↢ xs [ ∙ε _ ];
--         f (extract x)