\begin{code}
{-# OPTIONS --safe #-}

open import Prelude
open import Signatures
open import Cubical.Relation.Binary

open import FreeMonad.Theory hiding (ν)

--------------------------------------------------------------------------------
-- A Free monad, which is the syntax type quotiented by a theory
--------------------------------------------------------------------------------

module FreeMonad.Relation {ℓ}
  (𝔽 : Signature)
  (𝒯 : Theory 𝔽 ℓ) where

open Signature 𝔽
open import FreeMonad.Syntax 𝔽
open Theory 𝒯

private variable x y z : Syntax A
private
  variable
    ν : Type a
    𝒞 : Type c


open SyntaxBind

module MonomorphicRel {A : Type} where
\end{code}
%<*relation-decl>
\begin{code}
  data _~ₜ_ : Syntax A → Syntax A → Type where
\end{code}
%</relation-decl>
\begin{code}
module MonomorphicTerm where
  open MonomorphicRel

\end{code}
%<*term-sig>
\begin{code}
  Term : Type → Type
\end{code}
%</term-sig>
%<*term-def>
\begin{code}
  Term A = Syntax A / _~ₜ_
\end{code}
%</term-def>
\begin{code}


--------------------------------------------------------------------------------
-- The equivalence relation on syntax generated from a theory
------------------------------------------------------------------------------
module _ {A : Type a} where
  infix  _~ₜ_
  data _~ₜ_ : Syntax A → Syntax A → Type (ℓ ℓ⊔ a) where
\end{code}
%<*refl>
\begin{code}
    reflₜ   : x ≡ y → x ~ₜ y
\end{code}
%</refl>
%<*sym>
\begin{code}
    symₜ    : x ~ₜ y → y ~ₜ x
\end{code}
%</sym>
%<*trans>
\begin{code}
    transₜ  : x ~ₜ y → y ~ₜ z → x ~ₜ z
\end{code}
%</trans>
%<*cong>
\begin{code}
    congₜ   :  ∀ Oᵢ (kₗ kᵣ : Arity Oᵢ → Syntax A) →  (∀ i → kₗ i ~ₜ kᵣ i)
               → op (Oᵢ , kₗ) ~ₜ op (Oᵢ , kᵣ)
\end{code}
%</cong>
%<*eq>
\begin{code}
    eqₜ     :  ∀ i γ ρ → let lhs ≐ rhs = Eqns i .eqn γ in lhs >>= ρ ~ₜ rhs >>= ρ
\end{code}
%</eq>
%<*trunc>
\begin{code}
    truncₜ  : (eq₁ eq₂ : x ~ₜ y) → eq₁ ≡ eq₂
\end{code}
%</trunc>
\begin{code}
Term : Type a → Type _
Term ν = Syntax ν / _~ₜ_
\end{code}
%<*specialised-constructor-sig>
\begin{code}[inline]
[_]ₜ : Syntax A → Term A
\end{code}
%</specialised-constructor-sig>
%<*specialised-constructor>
\begin{code}[inline]
[_]ₜ = [_]
\end{code}
%</specialised-constructor>
\begin{code}

  -- resp-model : Syntax A → Syntax A → Type _
  -- resp-model xs ys = ∀ {B : Type} → (ϕ : 𝔽 -Alg[ B ]) → ∀ k → ϕ Models 𝒯 → interp ϕ k xs ≡ interp ϕ k ys

  -- lemma₁ : (xs ys : Syntax A) → xs ~ₜ ys → resp-model xs ys
  -- lemma₁ xs ys (reflₜ p) ϕ k x = cong (interp ϕ k) p
  -- lemma₁ xs ys (symₜ r)     ϕ k x = sym (lemma₁ ys xs r ϕ k x)
  -- lemma₁ xs ys (transₜ p q) ϕ k t = lemma₁ xs _ p ϕ k t ; lemma₁ _ ys q ϕ k t
  -- lemma₁ .(op (Oᵢ , kₗ)) .(op (Oᵢ , kᵣ)) (congₜ Oᵢ kₗ kᵣ x₁) ϕ k t = cong (ϕ ∘ _,_ Oᵢ) (funExt λ i → lemma₁ (kₗ i) (kᵣ i) (x₁ i) ϕ k t)
  -- lemma₁ .(Theory.Eqns 𝒯 i .eqn Γ .lhs >>= v) .(Theory.Eqns 𝒯 i .eqn Γ .rhs >>= v) (eqₜ i Γ v) ϕ k t = interp-comp ϕ k v (Theory.Eqns 𝒯 i .eqn Γ .lhs) ; t i Γ (interp ϕ k ∘ v) ; sym (interp-comp ϕ k v (Theory.Eqns 𝒯 i .eqn Γ .rhs))
  -- lemma₁ xs ys (truncₜ p q i) ϕ k x = {!!}

  -- lemma₂ : (xs ys : Syntax A) → resp-model xs ys → xs ~ₜ ys
  -- lemma₂ xs ys r = {!!}

--------------------------------------------------------------------------------
-- The relation is an equivalence
--------------------------------------------------------------------------------

~ₜ-equiv : BinaryRelation.isEquivRel (_~ₜ_ {A = A})
~ₜ-equiv .BinaryRelation.isEquivRel.reflexive _ = reflₜ refl
~ₜ-equiv .BinaryRelation.isEquivRel.symmetric _ _ = symₜ
~ₜ-equiv .BinaryRelation.isEquivRel.transitive _ _ _ = transₜ

--------------------------------------------------------------------------------
-- The quotient is effective
--------------------------------------------------------------------------------

~ₜ-effective : (x y : Syntax A) → [ x ] ≡ [ y ] → x ~ₜ y
~ₜ-effective = effective/ (λ _ _ → truncₜ) ~ₜ-equiv

--------------------------------------------------------------------------------
-- Smart constructor for law
--------------------------------------------------------------------------------

lawₜ : ∀ i g  →
       let lhs ≐ rhs = Eqns i .eqn g in lhs ~ₜ rhs
lawₜ i g = let lhs ≐ rhs = Eqns i .eqn g in
  reflₜ (sym (interp-id lhs))   ⟨ transₜ ⟩
  eqₜ i g var ⟨ transₜ ⟩
  reflₜ (interp-id rhs)

--------------------------------------------------------------------------------
-- We can define a interp on the quotiented type, as long as the algebra
-- respects the theory.
--------------------------------------------------------------------------------

module _ (ϕ : 𝔽 -Alg[ B ]) (ρ : A → B) (m : ϕ Models 𝒯) (set : isSet B) where
\end{code}
%<*interp-t-cong-sig>
\begin{code}
  interpₜ-cong  : ∀ {x y : Syntax A} →  x ~ₜ y →  interp ϕ ρ x ≡ interp ϕ ρ y
\end{code}
%</interp-t-cong-sig>
%<*interp-t-cong-eq>
\begin{code}
  interpₜ-cong (reflₜ p)          = cong (interp ϕ ρ) p
  interpₜ-cong (symₜ p)           = sym (interpₜ-cong p)
  interpₜ-cong (transₜ x~z z~y)   = interpₜ-cong x~z ; interpₜ-cong z~y
\end{code}
%</interp-t-cong-eq>
%<*interp-t-cong-cong>
\begin{code}
  interpₜ-cong (congₜ Oᵢ k k′ p)  = cong ϕ (cong (Oᵢ ,_) (funExt (λ i → interpₜ-cong (p i))))
\end{code}
%</interp-t-cong-cong>
%<*interp-t-cong-eqt>
\begin{code}
  interpₜ-cong (eqₜ i γ k) = let lhs ≐ rhs = Eqns i .eqn γ in
    interp ϕ ρ (interp op k lhs)       ≡⟨ interp-comp ϕ ρ k lhs ⟩
    interp ϕ (interp ϕ ρ ∘ k) lhs      ≡⟨ m i γ (interp ϕ ρ ∘ k) ⟩
    interp ϕ (interp ϕ ρ ∘ k) rhs      ≡˘⟨ interp-comp ϕ ρ k rhs ⟩
    interp ϕ ρ (interp op k rhs)       ∎
\end{code}
%</interp-t-cong-eqt>
\begin{code}
  interpₜ-cong {x} {y} (truncₜ p q i) =  set  (interp ϕ ρ x) (interp ϕ ρ y) (interpₜ-cong p) (interpₜ-cong q) i
\end{code}
%<*interp-t-sig>
\begin{code}
interpₜ : (ϕ : 𝔽 -Alg[ 𝒞 ]) (ρ : ν → 𝒞) → ϕ Models 𝒯 → isSet 𝒞 → Term ν → 𝒞
\end{code}
%</interp-t-sig>
%<*interp-t-impl>
\begin{code}
interpₜ ϕ ρ resp set = rec/ set (interp ϕ ρ) (λ _ _ → interpₜ-cong ϕ ρ resp set)
\end{code}
%</interp-t-impl>
\begin{code}
\end{code}
\begin{code}
open SyntaxBind

>>=-cong : (f : A → Syntax B) → {xs ys : Syntax A} → xs ~ₜ ys → (xs >>= f) ~ₜ (ys >>= f)
>>=-cong f (reflₜ x) = reflₜ (cong (_>>= f) x)
>>=-cong f (symₜ p) = symₜ (>>=-cong f p)
>>=-cong f (transₜ p q) = transₜ (>>=-cong f p) (>>=-cong f q)
>>=-cong f (truncₜ p q i) = truncₜ (>>=-cong f p) (>>=-cong f q) i
>>=-cong f (congₜ Oᵢ kₗ kᵣ x) = congₜ Oᵢ (kₗ >=> f) (kᵣ >=> f) λ i → >>=-cong f (x i)
>>=-cong f (eqₜ i Γ k) =
  reflₜ (interp-comp op _ _ (Eqns i .eqn Γ .lhs)) ⟨ transₜ ⟩ eqₜ i Γ (k >=> f) ⟨ transₜ ⟩ reflₜ (sym (interp-comp op _ _ (Eqns i .eqn Γ .rhs)))

<$>-cong : (f : A → B) {xs ys : Syntax A} → xs ~ₜ ys → (f <$> xs) ~ₜ (f <$> ys)
<$>-cong f = >>=-cong (var ∘ f)

<$>-just-injective : (xs ys : Syntax A) → just <$> xs ~ₜ just <$> ys → xs ~ₜ ys
<$>-just-injective xs ys p =
  reflₜ (sym (interp-id xs) ; sym (interp-comp op (maybe xs var) (var ∘ just) xs)) ⟨ transₜ ⟩
  >>=-cong (maybe xs var) p ⟨ transₜ ⟩
  reflₜ (interp-comp op (maybe xs var) (var ∘ just) ys ; interp-id ys)
\end{code}