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

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 6 _∙_
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 6 _∙_

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

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 6 _+_
infixl 7 _∗_
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 5 _<*>_
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 1 _>>=_
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 9 _<=<_

_<=<_ : (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 10 _=<=_
_=<=_ : (𝐹 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)
```