module Soat.SecondOrder.Algebra.Lift

import Data.List.Elem
import Data.Morphism.Indexed
import Data.Setoid.Indexed

import Soat.Data.Product
import Soat.Data.Sublist

import Soat.FirstOrder.Algebra
import Soat.FirstOrder.Algebra.Coproduct
import Soat.FirstOrder.Algebra.FreeExtension
import Soat.FirstOrder.Term

import Soat.SecondOrder.Algebra
import Soat.SecondOrder.Signature.Lift

import Syntax.PreorderReasoning.Setoid

%default total

public export
project : SecondOrder.Algebra.RawAlgebra (lift sig) -> (ctx : List sig.T)
  -> FirstOrder.Algebra.RawAlgebra sig
project a ctx = MakeRawAlgebra
  (flip a.U ctx)
  (\op => a.sem ctx (MkOp (Op op.op)) . wrap (MkPair []))

public export
projectIsAlgebra : {a : _} -> forall rel . SecondOrder.Algebra.IsAlgebra (lift sig) a rel
  -> (ctx : List sig.T)
  -> FirstOrder.Algebra.IsAlgebra sig (project a ctx) (\t => rel (t, ctx))
projectIsAlgebra a ctx = MkIsAlgebra
  (\t => a.equivalence (t, ctx))
  (\op => a.semCong ctx _ . wrapIntro)

public export
projectAlgebra : SecondOrder.Algebra.Algebra (lift sig) -> (ctx : List sig.T)
  -> FirstOrder.Algebra.Algebra sig
projectAlgebra a ctx = MkAlgebra _ _ (projectIsAlgebra a.algebra ctx)

public export
projectIsHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> {f : _} -> IsHomomorphism a b f
  -> (ctx : List sig.T)
  -> IsHomomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra b ctx) (\t => f t ctx)
projectIsHomo {b = b} homo ctx = MkIsHomomorphism
  { cong    = \t => homo.cong t ctx
  , semHomo = \op, tms => CalcWith (b.setoid.index _) $
    |~ f _ ctx (a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) tms))
    ~~ b.raw.sem ctx (MkOp (Op op.op)) (map (extendFunc f ctx) (wrap (MkPair []) tms))
      ...(homo.semHomo ctx (MkOp (Op op.op)) (wrap (MkPair []) tms))
    ~~ b.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => f t ctx) tms))
      .=.(cong (b.raw.sem ctx (MkOp (Op op.op))) $ mapWrap (MkPair []) {f = extendFunc f ctx} tms)
  }

public export
projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> Homomorphism a b
  -> (ctx : _) -> Homomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra b ctx)
projectHomo f ctx = MkHomomorphism (\t => f.func t ctx) (projectIsHomo f.homo ctx)

public export
(.renameHomo) : (a : SecondOrder.Algebra.Algebra (lift sig)) -> {ctx, ctx' : _}
  -> (f : ctx `Sublist` ctx')
  -> FirstOrder.Algebra.Homomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra a ctx')
(.renameHomo) a f = MkHomomorphism
  { func = \t => a.raw.rename t f
  , homo = MkIsHomomorphism
    { cong = \t => a.algebra.renameCong t f
    , semHomo = \op, tms => CalcWith (a.setoid.index _) $
      |~ a.raw.rename _ f (a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) tms))
      ~~ a.raw.sem _ (MkOp (Op op.op)) (map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms))
        ...(a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms))
      ~~ a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => a.raw.rename t f) tms))
        ...(a.algebra.semCong _ (MkOp (Op op.op)) $
            CalcWith (pwSetoid (a.setoid.reindex (\ty => (snd ty, fst ty ++ _))) _) $
            |~ map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms)
            ~~ wrap (MkPair []) (map (\t => a.raw.rename t (reflexive {x = []} ++ f)) tms)
              .=.(mapWrap (MkPair []) tms)
            ~~ wrap (MkPair []) (map (\t => a.raw.rename t f) tms)
              .=.(cong (wrap (MkPair [])) $
                  pwEqImpliesEqual $
                  mapIntro'' (\t, tm, _, Refl => cong (\f => a.raw.rename t f tm) $ uncurryCurry f) $
                  equalImpliesPwEq Refl))
    }
  }

public export
(.substHomo1) : (a : SecondOrder.Algebra.Algebra (lift sig)) -> (ctx : List sig.T)
  -> {ctx' : List sig.T} -> (tms : (\t => a.raw.U t ctx) ^ ctx')
  -> FirstOrder.Algebra.Homomorphism {sig = sig} (projectAlgebra a ctx') (projectAlgebra a ctx)
(.substHomo1) a ctx tms = MkHomomorphism
  { func = \t, tm => a.raw.subst t ctx tm tms
  , homo = MkIsHomomorphism
    { cong = \t, eq => a.algebra.substCong t ctx eq $ pwRefl (\_ => (a.algebra.equivalence _).refl)
    , semHomo = \op, tms' => CalcWith (a.setoid.index _) $
      |~ a.raw.subst _ ctx (a.raw.sem ctx' (MkOp (Op op.op)) (wrap (MkPair []) tms')) tms
      ~~ a.raw.sem ctx (MkOp (Op op.op)) (map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms'))
        ...(a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms)
      ~~ a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm tms) tms'))
        ...(a.algebra.semCong ctx (MkOp (Op op.op)) $
            CalcWith (pwSetoid (a.setoid.reindex (\ty => (snd ty, fst ty ++ ctx))) _) $
            |~ map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms')
            ~~ wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm (map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms)) tms')
              .=.(mapWrap (MkPair []) tms')
            ~~ wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm tms) tms')
              ...(wrapIntro $
                  mapIntro' (\t, eq =>
                    a.algebra.substCong t ctx eq $
                    CalcWith (pwSetoid (a.setoidAt _) _) $
                    |~ map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms
                    ~~ map (\t => a.raw.rename t reflexive) tms
                      .=.(pwEqImpliesEqual $
                          mapIntro' (\t => cong2 (a.raw.rename t) $ uncurryCurry reflexive) $
                          equalImpliesPwEq Refl)
                    ~~ map (\t => id) tms
                      ...(mapIntro' (\t, Refl => a.algebra.renameId t ctx _) $
                          equalImpliesPwEq Refl)
                    ~~ tms
                      .=.(mapId tms)) $
                  pwRefl (\t => (a.algebra.equivalence _).refl)))
    }
  }

indexFunc : {x : ISetoid a} -> (tms : x.U ^ ts) -> IFunction (isetoid (flip Elem ts)) x
indexFunc tms = MkIFunction
  (\_ => index tms)
  (\_ => (x.equivalence _).equalImpliesEq . cong (index tms))

public export
Initial : (0 sig : _) -> SecondOrder.Algebra.RawAlgebra (lift sig)
Initial sig = MakeRawAlgebra
  (\t, ctx => Term sig (flip Elem ctx) t)
  (\t, f => free (\_ => curry f) t)
  (\_, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair []))
  Done
  (\t, _, tm, tms => bindTerm {a = Free _} (\_ => index tms) t tm)

public export
InitialIsAlgebra : (0 sig : _)
  -> SecondOrder.Algebra.IsAlgebra
       (lift sig)
       (Initial sig)
       (\(t, ctx) => (~=~) {sig = sig} {v = flip Elem ctx} (\_ => Equal) t)
InitialIsAlgebra sig = MkIsAlgebra
  { equivalence = \(t, ctx) => tmRelEq (\_ => equiv) t
  , renameCong  = \t, f => freeCong (ifunc (\_ => curry f)) t
  , semCong     = \_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro
  , substCong   = \_, _, eq, eqs => bindTermCong'
    {a = FreeAlgebra (isetoid (flip Elem _))}
    (\t, Refl => index eqs _)
    _
    eq
  , renameId    = \t, ctx, tm =>
    tmRelSym (\_ => MkSymmetric symmetric) $
    freeUnique (ifunc (\_ => curry reflexive)) idHomo (\i => Done' $ sym $ curryUncurry id i) $
    tm
  , renameComp  = \t, f, g, tm =>
    tmRelSym (\_ => MkSymmetric symmetric) $
    freeUnique
      (ifunc (\_ => curry (transitive g f)))
      (compHomo (freeHomo (ifunc (\_ => curry f))) (freeHomo (ifunc (\_ => curry g))))
      (\i => Done' $ sym $ curryUncurry (curry f . curry g) i) $
    tm
  , semNat      = \f, (MkOp (Op op)), tms =>
    Call' (MkOp op) $
    CalcWith (pwSetoid (FreeAlgebra (isetoid (flip Elem _))).setoid _) $
    |~ bindTerms {a = Free _} (\_ => Done . curry f) _ (unwrap (MkPair []) tms)
    ~~ map (free (\_ => curry f)) (unwrap (MkPair []) tms)
      .=.(bindTermsIsMap {a = Free _} _ _)
    ~~ map (free (\_ => curry (reflexive {x = []} ++ f))) (unwrap (MkPair []) tms)
      ..<(mapIntro' (\t =>
            freeCong'
              {rel = \_ => Equal}
              {u = isetoid (flip Elem _)}
              (\_, Refl => curryUncurry (curry f) _)
              _) $
          tmsRelRefl (\_ => MkReflexive reflexive) (unwrap (MkPair []) tms))
    ~~ unwrap (MkPair []) (map (\ty => free (\_ => curry (reflexive {x = fst ty} ++ f)) (snd ty)) tms)
      .=.(mapUnwrap (MkPair []) tms)
  , varNat      = \_, _ => Done' Refl
  , substNat    = \t, f, tm, tms =>
    bindUnique
      {a = FreeAlgebra (isetoid (flip Elem _))}
      (indexFunc _)
      (compHomo
        (freeHomo (ifunc (\_ => curry f)))
        (bindHomo (indexFunc tms)))
      (\i =>
        tmRelReflexive (\_ => MkReflexive reflexive) $
        sym $
        indexMap tms i)
      tm
  , substExnat  = \t, ctx, f, tm, tms =>
    bindUnique
      {a = FreeAlgebra (isetoid (flip Elem _))}
      (indexFunc _)
      (compHomo
        (bindHomo (indexFunc tms))
        (freeHomo (ifunc (\_ => curry f))))
      (\i =>
        tmRelReflexive (\_ => MkReflexive reflexive) $
        sym $
        indexShuffle f i)
      tm
  , substComm   = \t, ctx, tm, tms, tms' =>
    bindUnique
      {a = FreeAlgebra (isetoid (flip Elem _))}
      (indexFunc _)
      (compHomo
        (bindHomo (indexFunc tms'))
        (bindHomo (indexFunc tms)))
      (\i =>
        tmRelReflexive (\_ => MkReflexive reflexive) $
        sym $
        indexMap tms i)
      tm
  , substVarL   = \_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _
  , substVarR   = \t, ctx, tm =>
    tmRelSym (\_ => MkSymmetric symmetric) $
    bindUnique
      {a = FreeAlgebra (isetoid (flip Elem _))}
      (indexFunc _)
      idHomo
      (\i =>
        tmRelReflexive (\_ => MkReflexive reflexive) $
        sym $
        indexTabulate Done i)
      tm
  , substCompat = \ctx, (MkOp (Op op)), tms, tms' =>
    Call' (MkOp op) $
    CalcWith (pwSetoid (FreeAlgebra (isetoid (flip Elem _))).setoid _) $
    |~ bindTerms {a = Free _} (\_ => index tms') _ (unwrap (MkPair []) tms)
    ~~ map (bindTerm {a = Free _} (\_ => index tms')) (unwrap (MkPair []) tms)
      .=.(bindTermsIsMap {a = Free _} _ _)
    ~~ map (\t => (Initial sig).extendSubst ctx tms' ([], t)) (unwrap (MkPair []) tms)
      ..<(mapIntro' (\t => bindTermCong'
            {rel = \_ => Equal}
            {a = FreeAlgebra (isetoid (flip Elem _))}
            (\t, Refl => CalcWith ((FreeAlgebra (isetoid (flip Elem _))).setoid.index _) $
              |~ index (map (free (\_ => curry ([] {ys = []} ++ reflexive))) tms') _
              ~~ free (\_ => curry ([] {ys = []} ++ reflexive)) _ (index tms' _)
                .=.(indexMap tms' _)
              ~~ index tms' _
                ..<(freeUnique
                      (ifunc (\_ => curry ([] {ys = []} ++ reflexive)))
                      idHomo
                      (\i => Done' $ sym $ trans (curryUncurry _ i) (curryUncurry id i))
                      (index tms' _)))
            _) $
          tmsRelRefl (\_ => MkReflexive reflexive) $
          unwrap (MkPair []) tms)
    ~~ unwrap (MkPair []) (map ((Initial sig).extendSubst ctx tms') tms)
      .=.(mapUnwrap (MkPair []) tms)
  }

public export
InitialAlgebra : (0 sig : _) -> SecondOrder.Algebra.Algebra (lift sig)
InitialAlgebra sig = MkAlgebra (Initial sig) _ (InitialIsAlgebra sig)

public export
ProjectInitialIsFree : (0 sig : _) -> (ctx : List sig.T)
  -> Isomorphism {sig = sig}
       (FreeAlgebra (isetoid (flip Elem ctx)))
       (projectAlgebra (InitialAlgebra sig) ctx)
ProjectInitialIsFree sig ctx = MkIsomorphism
  { to     = MkHomomorphism
    { func = \_ => id
    , homo = MkIsHomomorphism
      { cong = \_ => id
      , semHomo = \(MkOp op), ts =>
        Call' (MkOp op) $
        tmsRelReflexive (\_ => MkReflexive Refl) $
        sym $
        trans (unwrapWrap (extend (Initial sig).U ctx) _) (mapId ts)
      }
    }
  , from   = MkHomomorphism
    { func = \_ => id
    , homo = MkIsHomomorphism
      { cong = \_ => id
      , semHomo = \(MkOp op), ts =>
        Call' (MkOp op) $
        tmsRelReflexive (\_ => MkReflexive Refl) $
        trans (unwrapWrap (extend (Initial sig).U ctx) ts) (sym $ mapId ts)
      }
    }
  , fromTo = \tm => tmRelRefl (\_ => MkReflexive Refl) tm
  , toFrom = \tm => tmRelRefl (\_ => MkReflexive Refl) tm
  }

public export
fromInitial : (a : RawAlgebra (lift sig))
  -> (t : _) -> (ctx : _) -> (Initial sig).U t ctx -> a.U t ctx
fromInitial a t ctx = bindTerm {a = project a ctx} (\_ => a.var) t

public export
fromInitialIsHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
  -> IsHomomorphism (InitialAlgebra sig) a (fromInitial a.raw)
fromInitialIsHomo a = MkIsHomomorphism
  { cong       = \t, ctx => bindTermCong {a = projectAlgebra a ctx} (a.varFunc ctx) t
  , renameHomo = \t, f => bindUnique'
    {v = isetoid (flip Elem _)}
    {a = projectAlgebra a _}
    (compHomo (bindHomo (a.varFunc _)) (freeHomo (ifunc (\_ => curry f))))
    (compHomo (a.renameHomo f) (bindHomo (a.varFunc _)))
    (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i)
  , semHomo    = \ctx, (MkOp (Op op)), tms =>
    a.algebra.semCong ctx (MkOp (Op op)) $
    CalcWith (pwSetoid (a.setoid.reindex (\ty => (snd ty, fst ty ++ ctx))) _) $
    |~ wrap (MkPair []) (bindTerms {a = project a.raw ctx} (\_ => a.raw.var) _ (unwrap (MkPair []) tms))
    ~~ wrap (MkPair []) (map (\t => fromInitial a.raw t ctx) (unwrap (MkPair []) tms))
      .=.(cong (wrap _) $ bindTermsIsMap {a = project a.raw ctx} _ _)
    ~~ wrap (MkPair []) (unwrap (MkPair []) (map (extendFunc (fromInitial a.raw) ctx) tms))
      .=.(cong (wrap _) $ mapUnwrap (MkPair []) tms)
    ~~ map (extendFunc (fromInitial a.raw) ctx) tms
      .=.(wrapUnwrap _)
  , varHomo    = \_ => (a.algebra.equivalence _).reflexive
  , substHomo  = \t, ctx, tm, tms =>
    bindUnique'
      {v = isetoid (flip Elem _)}
      {a = projectAlgebra a _}
      (compHomo
        (bindHomo (a.varFunc _))
        (bindHomo (indexFunc tms)))
      (compHomo
        (a.substHomo1 ctx _) (bindHomo (a.varFunc _)))
      (\i => CalcWith (a.setoid.index _) $
        |~ bindTerm {a = project a.raw _} (\_ => a.raw.var) _ (index tms i)
        ~~ index (map (bindTerm {a = project a.raw _} (\_ => a.raw.var)) tms) i
          .=<(indexMap {f = bindTerm {a = project a.raw _} (\_ => a.raw.var)} tms i)
        ~~ a.raw.subst _ ctx (a.raw.var i) (map (bindTerm {a = project a.raw _} (\_ => a.raw.var)) tms)
          ..<(a.algebra.substVarL ctx i _))
      tm
  }

public export
fromInitialHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
  -> Homomorphism (InitialAlgebra sig) a
fromInitialHomo a = MkHomomorphism (fromInitial a.raw) (fromInitialIsHomo a)

public export
fromInitialUnique : {a : SecondOrder.Algebra.Algebra (lift sig)}
  -> (f : Homomorphism (InitialAlgebra sig) a)
  -> (t : sig.T) -> (ctx : List sig.T) -> (tm : Term sig (flip Elem ctx) t)
  -> a.relation (t, ctx) (f.func t ctx tm) (fromInitial a.raw t ctx tm)
fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique
  {v = isetoid (flip Elem _)}
  {a = projectAlgebra a ctx}
  (a.varFunc ctx)
  (compHomo (projectHomo f ctx) (ProjectInitialIsFree sig ctx).to)
  f.homo.varHomo

public export
FreeExtension : RawAlgebra sig -> RawAlgebra (lift sig)
FreeExtension a = MakeRawAlgebra
  { U      = \t, ctx => (FreeExtension a (flip Elem ctx)).U t
  , rename = \t, f => extend (\_ => curry f) t
  , sem    = \ctx, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair [])
  , var    = Done . Right . Done
  , subst  = \t, ctx, tm, tms =>
    coproduct
      {z = FreeExtension a (flip Elem _)}
      (\_ => Done . Left)
      (bindTerm {a = FreeExtension a (flip Elem _)} (\_ => index tms))
      t
      tm
  }

public export
FreeExtensionAlgebra : Algebra sig -> Algebra (lift sig)
FreeExtensionAlgebra a = MkAlgebra
  { raw = FreeExtension a.raw
  , relation = \(t, ctx) => (FreeExtensionAlgebra a (isetoid (flip Elem ctx))).relation t
  , algebra  = MkIsAlgebra
    { equivalence = \(t, ctx) => (FreeExtensionAlgebra a (isetoid (flip Elem ctx))).algebra.equivalence t
    , renameCong  = \t, f => extendCong (ifunc (\_ => curry f)) t
    , semCong     = \_ , (MkOp (Op op)) => Call (MkOp op) . unwrapIntro
    , substCong   = \t, ctx, eq, eqs => coproductCong' {z = FreeExtensionAlgebra a (isetoid (flip Elem ctx))}
      (injectLHomo {y = FreeAlgebra (isetoid (flip Elem ctx))})
      (injectLHomo {y = FreeAlgebra (isetoid (flip Elem ctx))})
      (bindHomo (indexFunc _))
      (bindHomo (indexFunc _))
      (\_ => DoneL)
      (bindTermCong' {a = FreeExtensionAlgebra a (isetoid (flip Elem _))} (\_, Refl => index eqs _))
      t
      eq
    , renameId    = \t, ctx, tm =>
      (((FreeExtensionAlgebra a (isetoid (flip Elem _)))).algebra.equivalence _).symmetric $
      extendUnique
        { v     = isetoid (flip Elem _)
        , u     = isetoid (flip Elem _)
        , f     = ifunc ?f -- (\_ => curry reflexive)
        , g     = idHomo
        , congL = ?congL
        , congR = ?congR
        , tm    = ?tm
        }
      -- extendUnique (ifunc (\_ => curry reflexive)) idHomo ?congL ?congR tm
    , renameComp  = \t, f, g, tm => ?renameComp
    , semNat      = \f, (MkOp (Op op)), tms => Call (MkOp op) $ ?semNat
    , varNat      = \f, i => (((FreeExtensionAlgebra a (isetoid (flip Elem _)))).algebra.equivalence _).reflexive
    , substNat    = \t, f, tm, tms => ?substNat
    , substExnat  = \t, ctx, f, tm, tms => ?substExnat
    , substComm   = \t, ctx, tm, tms, tms' => ?substComm
    , substVarL   = \ctx, i, tms => ?substVarL
    , substVarR   = \t, ctx, tm => ?substVarR
    , substCompat = \ctx, (MkOp (Op op)), tms, tms' => Call (MkOp op) $ ?substCompat
    }
  }

public export
ProjectFreeExtensionIsOriginal : (a : FirstOrder.Algebra.Algebra sig)
  -> Isomorphism (projectAlgebra (FreeExtensionAlgebra a) []) a

public export
FreeExtensionIsFree : (a : Algebra sig) -> (b : Algebra (lift sig))
  -> Isomorphism (projectAlgebra b []) a
  -> Homomorphism (FreeExtensionAlgebra a) b

-- -- public export
-- -- FreeExtension : RawAlgebra sig -> RawAlgebra (lift sig)
-- -- FreeExtension a = MakeRawAlgebra
-- --   { U      = \t, ctx => (Coproduct a (Free (flip Elem ctx))).U t
-- --   , rename = \t, f => coproduct
-- --     {z = Coproduct a (Free (flip Elem _))}
-- --     (\_ => Done . Left)
-- --     (\t => Done . Right . (Initial sig).rename t f)
-- --     t
-- --   , sem    = \ctx, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair [])
-- --   , var    = Done . Right . Done
-- --   , subst  = \t, ctx, tm, tms => coproduct
-- --     {z = Coproduct a (Free (flip Elem _))}
-- --     (\_ => Done . Left)
-- --     (\_ => bindTerm {a = Coproduct a (Free (flip Elem ctx))} (\_ => index tms))
-- --     t
-- --     tm
-- --   }

-- -- public export 0
-- -- FreeExtensionRelation : (algebra : FirstOrder.Algebra.IsAlgebra sig a rel)
-- --   -> IRel (uncurry (FreeExtension a).U)
-- -- FreeExtensionRelation algebra (t, ctx) =
-- --   (CoproductAlgebra (MkAlgebra _ _ algebra) (FreeAlgebra (isetoid (flip Elem ctx)))).relation t

-- -- public export
-- -- FreeExtensionIsAlgebra : {a : RawAlgebra sig} -> forall rel . (algebra : IsAlgebra sig a rel)
-- --   -> IsAlgebra (lift sig) (FreeExtension a) (FreeExtensionRelation algebra)
-- -- FreeExtensionIsAlgebra algebra = MkIsAlgebra
-- --   { equivalence = \(t, ctx) => ?equivalence
-- --   , renameCong  = \t, f => coproductCong
-- --     (injectLHomo (MkAlgebra _ _ algebra) (FreeAlgebra (isetoid (flip Elem _))))
-- --     (compHomo (injectRHomo a ?y) ?g)
-- --     -- (compHomo
-- --     --   (injectRHomo (MkAlgebra _ _ algebra) (FreeAlgebra (isetoid (flip Elem _))))
-- --     --   ((InitialAlgebra sig).renameHomo f))
-- --     t
-- --   , semCong     = \ctx, (MkOp (Op op)) => Call (MkOp op) . unwrapIntro
-- --   , substCong   = \t, ctx, eq, eqs => coproductCong'
-- --     (injectLHomo (MkAlgebra _ _ algebra) (FreeAlgebra (isetoid (flip Elem _))))
-- --     (injectLHomo (MkAlgebra _ _ algebra) (FreeAlgebra (isetoid (flip Elem _))))
-- --     (bindHomo (indexFunc _ _))
-- --     (bindHomo (indexFunc _ _))
-- --     (\_ => DoneL)
-- --     ?rhs -- (bindTermCong' (\_ => index ?eqseqs))
-- --     _
-- --     ?eq
-- --   , renameId    = ?renameId
-- --   , renameComp  = ?renameComp
-- --   , semNat      = ?semNat
-- --   , varNat      = ?varNat
-- --   , substNat    = ?substNat
-- --   , substExnat  = ?substExnat
-- --   , substComm   = ?substComm
-- --   , substVarL   = ?substVarL
-- --   , substVarR   = ?substVarR
-- --   , substCompat = ?substCompat
-- --   }

-- -- public export
-- -- FreeExtensionAlgebra : Algebra sig -> Algebra (lift sig)
-- -- FreeExtensionAlgebra a = MkAlgebra _ _ $ FreeExtensionIsAlgebra a.algebra