{-# OPTIONS --without-K --safe #-}
open import Categories.Category
open import Categories.Functor hiding (id)
open import Categories.Functor.DistributiveLaw using (DistributiveLaw)
module Categories.Functor.Construction.LiftAlgebras {o  e} {C : Category o  e} (T F : Endofunctor C) (μ : DistributiveLaw T F) where

open import Level
open import Function using (_$_)

open import Categories.Functor.Algebra using (F-Algebra;F-Algebra-Morphism)
open import Categories.Functor.Coalgebra using (F-Coalgebra;F-Coalgebra-Morphism)
open import Categories.NaturalTransformation using (NaturalTransformation)
open import Categories.Category.Construction.F-Algebras using (F-Algebras)
open import Categories.Category.Construction.F-Coalgebras using (F-Coalgebras)
open import Categories.Functor.Properties using ([_]-resp-square)

open import Categories.Object.Initial

import Categories.Morphism.Reasoning as MR

{-
For theoretical background, see header comment in
`Categories.Category.Construction.mu-Bialgebras`
-}

LiftAlgebras : Endofunctor (F-Algebras T)
LiftAlgebras = record
  { F₀           = λ X  record { A = (F .F₀) (X .A);  α = (F₁ F) (X .α)  (μ .η) (X .A) }
  ; F₁           = λ α₁  record { f = (F .F₁) (α₁ .f) ; commutes = commut α₁ }
  ; identity     = identity F
  ; homomorphism = homomorphism F
  ; F-resp-≈     = F-resp-≈ F
  }
  where
    open Category C
    open Definitions C
    open MR C
    open HomReasoning
    open Equiv
    open Functor
    open NaturalTransformation
    open F-Algebra
    open F-Algebra-Morphism
    commut : { X Y : F-Algebra T }  (a : F-Algebra-Morphism X Y) 
      (F .F₁) (a .f)  ((F .F₁) (X .α)  (μ .η) (X .A)) 
      ((F .F₁) (Y .α)  (μ .η) (Y .A))  (T .F₁) ((F .F₁) (a .f))
    commut {X} {Y} a =  (glue ( ([ F ]-resp-square (commutes a))) (commute μ (f a)))

liftInitial : Initial (F-Algebras T)  Initial (F-Coalgebras LiftAlgebras)
liftInitial μT = record
  {  = record
    { A = 
    ; α =  F₀  
    }
  ; ⊥-is-initial = record
    { ! = λ {A = X} 
      let
        a = F-Coalgebra.A X
        c = F-Coalgebra.α X
      in record
      { f =  a 
      ; commutes = !-unique₂ (c   a ) (F₁  a    F₀  )
      }
    ; !-unique = λ {A = X} g  !-unique (F-Coalgebra-Morphism.f g)
    }
  }
  where
    open Initial μT
    open Category (F-Algebras T)
    open Definitions (F-Algebras T)
    open MR (F-Algebras T)
    open HomReasoning
    open Equiv
    private
      ⦅_⦆ = λ X  ! {A = X} -- "banana brackets" (Meijer 1991)
    open Functor LiftAlgebras