\begin{code}

{-# OPTIONS --safe #-}

open import Signatures
open import Prelude hiding (Iso)

module FreeMonad.Syntax (𝔽 : Signature) where

open Signature 𝔽

--------------------------------------------------------------------------------
-- Unquotiented Free Monad
--------------------------------------------------------------------------------

data Syntax (A : Type a) : Type a
data Syntax Ξ½ where
  var  : Ξ½                 β†’ Syntax Ξ½
  op   : ⟦ 𝔽 ⟧ (Syntax Ξ½)  β†’ Syntax Ξ½
\end{code}
%<*op-con>
\begin{code}
Op⟦_⟧ : βˆ€ o β†’ Syntax (Arity o)
Op⟦ o ⟧ = op (o , var)
\end{code}
%</op-con>
\begin{code}

private variable Ξ½ : Type a

\end{code}
%<*syntax-alg>
\begin{code}
syntax-alg : 𝔽 -Alg[ Syntax Ξ½ ]
syntax-alg = op
\end{code}
%</syntax-alg>
\begin{code}
syntax-alg' : (v : Type) β†’ 𝔽 -Alg
syntax-alg' Ξ½ = Syntax Ξ½ , op

--------------------------------------------------------------------------------
-- Fold
--------------------------------------------------------------------------------

private variable π’ž : Type c
\end{code}
%<*interp>
\begin{code}[number=syn:interp]
interp : 𝔽 -Alg[ π’ž ] β†’ (Ξ½ β†’ π’ž) β†’ Syntax Ξ½ β†’ π’ž
interp Ο• ρ (var x)        = ρ x
interp Ο• ρ (op (Oα΅’ , k))  = Ο• (Oα΅’ , Ξ» i β†’ interp Ο• ρ (k i))
\end{code}
%</interp>
\begin{code}

--------------------------------------------------------------------------------
-- The base *dependent* functor for this type:
--------------------------------------------------------------------------------

data π”–π”Άπ”«π”±π”žπ”΅ (A : Type a) (B : Type b) (P : B β†’ Type c) : Type (a β„“βŠ” b β„“βŠ” c) where
  var  :  A                              β†’ π”–π”Άπ”«π”±π”žπ”΅ A B P
  op   :  (xs : ⟦ 𝔽 ⟧ B)
          (P⟨xs⟩ : βˆ€ i β†’ P (xs .snd i))  β†’ π”–π”Άπ”«π”±π”žπ”΅ A B P

--------------------------------------------------------------------------------
-- Dependent eliminators for the syntax type
--------------------------------------------------------------------------------

βŸͺ_⟫ : π”–π”Άπ”«π”±π”žπ”΅ A (Syntax A) P β†’ Syntax A
βŸͺ var x    ⟫ = var x
βŸͺ op xs _  ⟫ = op xs

DepAlg : (A : Type a) β†’ (Syntax A β†’ Type b) β†’ Type (a β„“βŠ” b)
DepAlg A P = (xs : π”–π”Άπ”«π”±π”žπ”΅ A (Syntax A) P) β†’ P βŸͺ xs ⟫

syntax DepAlg A (Ξ» xs β†’ P) = Ξ¨[ xs ⦂ Syntax A ] P

elim-s : (P : Syntax A β†’ Type b) β†’ DepAlg A P β†’ (xs : Syntax A) β†’ P xs
elim-s _ alg (var x)         = alg (var x)
elim-s P alg (op (Op , xs))  = alg (op (Op , xs) (Ξ» i β†’ elim-s P alg (xs i)))

--------------------------------------------------------------------------------
-- Bind
--------------------------------------------------------------------------------

module SyntaxBind where
  return : A β†’ Syntax A
  return = var

  private variable
    Ξ½β€² : Type b

  infixl 4.5 _=<<_
  _=<<_ : (Ξ½ β†’ Syntax Ξ½β€²) β†’ Syntax Ξ½ β†’ Syntax Ξ½β€²
  _=<<_ = interp op

  infixr 4.5 _>>=_
\end{code}
%<*bind>
\begin{code}
  _>>=_ : Syntax A β†’ (A β†’ Syntax B) β†’ Syntax B
  xs >>= ρ = interp op ρ xs
\end{code}
%</bind>
\begin{code}

  infixr 4.5 _>>_
  _>>_ : Syntax A β†’ Syntax B β†’ Syntax B
  xs >> ys = xs >>= Ξ» _ β†’ ys

  infixr 9 _<=<_
  _<=<_ : (B β†’ Syntax C) β†’ (A β†’ Syntax B) β†’ A β†’ Syntax C
  (f <=< g) x = f =<< g x

  infixl 9 _>=>_
  _>=>_ : (A β†’ Syntax B) β†’ (B β†’ Syntax C) β†’ A β†’ Syntax C
  _>=>_ = flip _<=<_

  infixr 4.5 _<$>_
  _<$>_ : (A β†’ B) β†’ Syntax A β†’ Syntax B
  f <$> xs = xs >>= var ∘ f

  infixl 4.5 _<&>_
  _<&>_ : Syntax A β†’ (A β†’ B) β†’ Syntax B
  xs <&> f = f <$> xs

  <$>-comp : (xs : Syntax A) β†’ (f : A β†’ B) β†’ (g : B β†’ C) β†’ ((g ∘ f) <$> xs) ≑ (g <$> (f <$> xs))
  <$>-comp (var x)      f g   = refl
  <$>-comp (op (o , k)) f g i = op (o , Ξ» a β†’ <$>-comp (k a) f g i)

open SyntaxBind

--------------------------------------------------------------------------------
-- Properties about interps on syntax
--------------------------------------------------------------------------------

interp-id : 
\end{code}
%<*interp-id>
\begin{code}
  (xs : Syntax Ξ½) β†’ interp op var xs ≑ xs
\end{code}
%</interp-id>
\begin{code}
interp-id (var x)        = refl
interp-id (op (Oα΅’ , k))  = cong (op ∘ _,_ Oα΅’) (funExt Ξ» i β†’ interp-id (k i))

interp-fusion  :  (f : C β†’ A) {g₁ : ⟦ 𝔽 ⟧ C β†’ C} {gβ‚‚ : ⟦ 𝔽 ⟧ A β†’ A} (c : B β†’ C) β†’
                  (βˆ€ xs β†’ f (g₁ xs) ≑ gβ‚‚ (cmap f xs)) β†’ 
               βˆ€  xs β†’ f (interp g₁ c xs) ≑ interp gβ‚‚ (f ∘ c) xs
interp-fusion f            c p (var x)          = refl
interp-fusion f {gβ‚‚ = gβ‚‚}  c p (op (Oα΅’ , xs) )  =
  p _ ΝΎ cong gβ‚‚ (cong (Oα΅’ ,_) (funExt Ξ» x β†’ interp-fusion f c p (xs x)))

private module DisplayComp where
  private variable Ξ½β€² : Type b
  interp-comp : βˆ€ (Ο• : 𝔽 -Alg[ π’ž ]) (ρ : Ξ½β€² β†’ π’ž) (k : Ξ½ β†’ Syntax Ξ½β€²) xs β†’
\end{code}
%<*interp-comp>
\begin{code}[number=interp-comp]
                interp Ο• ρ (xs >>= k) ≑ interp Ο• (interp Ο• ρ ∘ k) xs
\end{code}
%</interp-comp>
\begin{code}
  interp-comp Ο• ρ k (var x)         = refl
  interp-comp Ο• ρ k (op (Oα΅’ , ks))  = cong (Ο• ∘ _,_ Oα΅’) (funExt Ξ» i β†’ interp-comp Ο• ρ k (ks i))

interp-comp : βˆ€ (f : ⟦ 𝔽 ⟧ A β†’ A) (k : B β†’ A) (c : C β†’ Syntax B) xs β†’
              interp f k (xs >>= c) ≑ interp f (interp f k ∘ c) xs
interp-comp f k c = interp-fusion (interp f k) c Ξ» _ β†’ refl

-- interp is a homomorphism
interp-homo : βˆ€ {Ξ½ C : Type} β†’ (alg : 𝔽 -Alg[ C ]) β†’ (Ξ½ β†’ C)
            β†’ ((Syntax Ξ½ , syntax-alg) ⟢ (C , alg))
interp-homo {Ξ½ = Ξ½} alg k = interp alg k , funExt comm
  where
    comm :  (x : ⟦ 𝔽 ⟧ (Syntax Ξ½)) β†’ interp alg k (op x) ≑ alg (cmap (interp alg k) x)
    comm (o , xs) = refl

--------------------------------------------------------------------------------
-- Freeness of Syntax
--------------------------------------------------------------------------------

var-alg : (Ξ½ : Type) β†’ (C : Type) β†’ (alg : 𝔽 -Alg[ C ])
        β†’ ((Syntax Ξ½ , syntax-alg {Ξ½ = Ξ½}) ⟢ (C , alg)) β†’ Ξ½ β†’ C
var-alg Ξ½ C alg (h , _) x = h (var x)

open import Cubical.Foundations.Isomorphism using (isoToIsEquiv; Iso)

-- The homotopy freeness is essentially Theorem 5.4.7 in the HoTT book and studied
-- in detail in the following paper:
--
--   Steve Awodey, Nicola Gambino, and Kristina Sojakova. 2017. Homotopy-Initial
--   Algebras in Type Theory. J. ACM 63, 6, Article 51 (February 2017), 45 pages.
--   https://doi.org/10.1145/3006383
--
-- The following proof is generalised from the proof of homotopy initiality of natural
-- numbers in the cubical library (https://agda.github.io/cubical/Cubical.Data.Nat.Algebra.html).

syntax-is-free : βˆ€ {Ξ½ : Type} β†’ (C : Type) β†’ (alg : 𝔽 -Alg[ C ])
               β†’ isEquiv (var-alg Ξ½ C alg)
syntax-is-free {Ξ½} C alg = isoToIsEquiv i where
  i : Iso ((Syntax Ξ½ , syntax-alg {Ξ½ = Ξ½}) ⟢ (C , alg)) (Ξ½ β†’ C)
  i .fun = var-alg Ξ½ C alg
  i .inv k = interp-homo alg k
  i .rightInv k = refl
  i .leftInv (h , comm) = Ξ£PathP (h-path , comm-path) where
     h-var-fusion-ty : Syntax Ξ½ β†’ Type
     h-var-fusion-ty x = interp alg (h ∘ var) x ≑ h x

     open import Cubical.Foundations.Prelude using (_βˆ™βˆ™_βˆ™βˆ™_)
     open import Cubical.Foundations.Path using (PathP≑doubleCompPathΚ³)

     h-var-fusion-alg : DepAlg Ξ½ h-var-fusion-ty
     h-var-fusion-alg (var x) = refl
     h-var-fusion-alg (op oxs P⟨xs⟩) = refl βˆ™βˆ™ p-IH βˆ™βˆ™ sym (Ξ» i β†’ comm i oxs)  where
       p-IH : alg (oxs .fst , (Ξ» a β†’ interp alg (Ξ» x β†’ h (var x)) (oxs .snd a))) ≑ alg (cmap h oxs)
       p-IH = cong (Ξ» xs' β†’ alg (oxs .fst , xs')) (funExt (Ξ» a β†’ P⟨xs⟩ a))

     h-var-fusion : βˆ€ x β†’ interp alg (h ∘ var) x ≑ h x
     h-var-fusion = elim-s h-var-fusion-ty h-var-fusion-alg

     h-path : interp alg (h ∘ var) ≑ h
     h-path = funExt h-var-fusion


     -- The key observation is that the h-path for the op case is defined by
     -- composing comm, p-IH, and (interp-homo alg (h ∘ var) .snd) (which is
     -- refl), so there is a trivial filler comm-path of the square formed by
     -- these four paths.
     squeezeSquare : βˆ€{a}{A : Type a}{w x y z : A} (p : w ≑ x) {q : x ≑ y} (r : z ≑ y)
                   β†’ (P : w ≑ z) β†’ (sq : P ≑ p βˆ™βˆ™ q βˆ™βˆ™ sym r) β†’ I β†’ I β†’ A
     squeezeSquare p {q} r P sq i j = transport (sym (PathP≑doubleCompPathΚ³ p P q r)) sq i j


     comm-path : PathP (Ξ» i β†’ (Ξ» xs β†’ h-path i (op xs)) ≑ (Ξ» xs β†’ alg (cmap (h-path i) xs)))
                       (interp-homo alg (h ∘ var) .snd)
                       comm
     comm-path i j oxs = squeezeSquare (Ξ» k β†’ (interp-homo alg (h ∘ var) .snd) k oxs )
                                       (Ξ» k β†’ comm k oxs)
                                       (h-var-fusion (op oxs))
                                       (refl {x = h-var-fusion (op oxs)})
                                       j
                                       i


--------------------------------------------------------------------------------
-- Modality
--------------------------------------------------------------------------------

β—‡β€² : βˆ€ {p} β†’ (A β†’ Type p) β†’ Syntax A β†’ Type p
β—‡β€² P (var x) = P x
β—‡β€² P (op (O , xs)) = βˆƒ i Γ— β—‡β€² P (xs i)

β–‘β€² : βˆ€ {p} β†’ (A β†’ Type p) β†’ Syntax A β†’ Type p
β–‘β€² P (var x) = P x
β–‘β€² P (op (O , xs)) = βˆ€ i β†’ β–‘β€² P (xs i)

β–‘β€²->>=-β–‘β€² : βˆ€ {p q} (P : A β†’ Type p) (Q : B β†’ Type q) β†’
              (xs : Syntax A) (f : A β†’ Syntax B) β†’
              (βˆ€ x β†’ P x β†’ β–‘β€² Q (f x)) β†’ β–‘β€² P xs β†’ β–‘β€² Q (xs >>= f)
β–‘β€²->>=-β–‘β€² P Q (var x) f t Pxs = t x Pxs
β–‘β€²->>=-β–‘β€² P Q (op (Oα΅’ , xs)) f t Pxs i = β–‘β€²->>=-β–‘β€² P Q (xs i) f t (Pxs i)

β—‡β€²->>=-β—‡β€² : βˆ€ {p q} (P : A β†’ Type p) (Q : B β†’ Type q) β†’
              (xs : Syntax A) (f : A β†’ Syntax B) β†’
              (βˆ€ x β†’ P x β†’ β—‡β€² Q (f x)) β†’ β—‡β€² P xs β†’ β—‡β€² Q (xs >>= f)
β—‡β€²->>=-β—‡β€² P Q (var x) f t Pxs = t x Pxs
β—‡β€²->>=-β—‡β€² P Q (op (Oα΅’ , xs)) f t (i , Pxs) = i , β—‡β€²->>=-β—‡β€² P Q (xs i) f t Pxs

β–‘β€²-fmap : βˆ€ {A : Type a} {P Q : A β†’ Type p} (t : Syntax A) β†’
            (βˆ€ (x : A) β†’ P x β†’ Q x) β†’ (β–‘β€² P t β†’ β–‘β€² Q t)
β–‘β€²-fmap (var x) f p =  f x p
β–‘β€²-fmap (op (o , k)) f p = Ξ» a β†’ β–‘β€²-fmap (k a) f (p a)

β—‡β€²-fmap : βˆ€ {A : Type a} {P Q : A β†’ Type p} (t : Syntax A) β†’
            (βˆ€ (x : A) β†’ P x β†’ Q x) β†’ (β—‡β€² P t β†’ β—‡β€² Q t)
β—‡β€²-fmap (var x) f p = f x p
β—‡β€²-fmap (op (o , k)) f (a , p) = a ,  β—‡β€²-fmap (k a) f p

β–‘β€²-shift : βˆ€ {A : Type a} {P : B β†’ Type p} β†’ (f : A β†’ B) β†’ (t : Syntax A) β†’ β–‘β€² (P ∘ f) t β†’ β–‘β€² P (f <$> t)
β–‘β€²-shift f (var x) p = p
β–‘β€²-shift f (op (o , k)) p a = β–‘β€²-shift f (k a) (p a)

β—‡β€²-shift : βˆ€ {A : Type a} {P : B β†’ Type p} β†’ (f : A β†’ B) β†’ (t : Syntax A) β†’ β—‡β€² (P ∘ f) t β†’  β—‡β€² P (f <$> t)
β—‡β€²-shift f (var x) p = p
β—‡β€²-shift f (op (o , k)) (a , p) = a , β—‡β€²-shift f (k a) p

var-inj : Injective (Syntax.var {A = A})
var-inj {x = x} {y} = cong Ξ» { (var x) β†’ x ; (op _) β†’ x }

op-inj : Injective (Syntax.op {A = A})
op-inj {x = x} {y} = cong Ξ» { (var _) β†’ x ; (op x) β†’ x }

open import Cubical.Data.Sigma.Properties

opF-inj : isSet Op β†’ (O : Op) β†’ (xs ys : Arity O β†’ Syntax A) β†’ (op (O , xs) ⦂ Syntax A) ≑ op (O , ys) β†’ xs ≑ ys
opF-inj set O xs ys p =
  Ξ£-contractFst (refl , Ξ» _ β†’ set _ _ _ _) .fst (PathPΞ£ (op-inj p))

isReturn : Syntax A β†’ Bool
isReturn (var _) = true
isReturn (op _) = false

fmap-injective : (f : A β†’ B) β†’ Injective f β†’ Injective (f <$>_)
fmap-injective f inj {var x} {var y} p = cong var (inj (var-inj p))
fmap-injective {A = A} {B = B} f inj {op (i , x)} {op (j , y)} p =
  let q = op-inj { x = i , _<$>_ f ∘ x } { y = j , _<$>_ f ∘ y } p
      h = cong fst q
  in cong (op ⦂ (⟦ 𝔽 ⟧ (Syntax _) β†’ Syntax _))
    (congβ‚‚ _,_ h
    (J (Ξ» z zp β†’ βˆ€ y β†’ PathP (Ξ» l β†’ Arity (zp l) β†’ Syntax B) (_<$>_ f ∘ x) (_<$>_ f ∘ y) β†’ PathP (Ξ» l β†’ Arity (zp l) β†’ Syntax A) x y)
        (Ξ» yβ€² pβ€² β†’ funExt Ξ» k β†’ fmap-injective f inj {x k} {yβ€² k} (cong (_$ k) pβ€²)) h y (cong snd q)))
fmap-injective f inj {var x} {op y} p = absurd (true≒false (cong isReturn p))
fmap-injective f inj {op x} {var y} p = absurd (false≒true (cong isReturn p))

varβ‰’op : βˆ€ {x : A} {O k} β†’ var x β‰’ op (O , k)
varβ‰’op = trueβ‰’false ∘ cong isReturn

opβ‰’var : βˆ€ {x : A} {O k} β†’ op (O , k) β‰’ var x
opβ‰’var = falseβ‰’true ∘ cong isReturn

>>=-com-<$> : (f : A β†’ Syntax B) (g : B β†’ C) (xs : Syntax A) β†’ (xs >>= Ξ» x β†’ g <$> f x) ≑ g <$> (xs >>= f)
>>=-com-<$> f g = elim-s _ Ξ» { (var x) β†’ refl ; (op (O , k) P⟨xs⟩) β†’ cong (op ∘ _,_ O) (funExt P⟨xs⟩) }
\end{code}