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

open import Categories.Category
open import Categories.Comonad

-- verbatim dual of Categories.Category.Construction.EilenbergMoore
module Categories.Category.Construction.CoEilenbergMoore {o  e} {C : Category o  e} (M : Comonad C) where

open import Level

open import Categories.Morphism.Reasoning C

private
  module C = Category C
  module M = Comonad M
  open C
  open M.F
  open HomReasoning
  open Equiv

record Comodule : Set (o    e) where
  field
    A        : Obj
    coaction   : A  F₀ A
    commute  : F₁ coaction  coaction  M.δ.η A  coaction
    identity : M.ε.η A  coaction  C.id

record Comodule⇒ (X Y : Comodule) : Set (  e) where
  private
    module X = Comodule X
    module Y = Comodule Y
  field
    arr     : X.A  Y.A
    commute : Y.coaction  arr  F₁ arr  X.coaction

CoEilenbergMoore : Category (o    e) (  e) e
CoEilenbergMoore =
 record
  { Obj = Comodule
  ; _⇒_ = Comodule⇒
  ; _≈_ = λ f g  Comodule⇒.arr f  Comodule⇒.arr g
  ; id = record { arr = C.id ; commute = identityʳ  introˡ identity }
  ; _∘_ = compose
  ; assoc = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
  ; ∘-resp-≈ = ∘-resp-≈
  }
  where
   open Equiv
   compose :  {X Y Z}  Comodule⇒ Y Z  Comodule⇒ X Y  Comodule⇒ X Z
   compose {X} {Y} {Z} f g = record
    { arr     = f.arr  g.arr
    ; commute = begin
       Comodule.coaction Z  f.arr  g.arr       ≈⟨ pullˡ f.commute 
       (F₁ f.arr  Comodule.coaction Y)  g.arr  ≈⟨ pullʳ g.commute 
       F₁ f.arr  F₁ g.arr  Comodule.coaction X ≈⟨ pullˡ (sym homomorphism) 
       F₁ (f.arr  g.arr)  Comodule.coaction X  
    }
    where module f = Comodule⇒ f
          module g = Comodule⇒ g