module Soat.SecondOrder.Algebra.Lift

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

import Soat.Data.Product
import Soat.Data.Sublist
import Soat.FirstOrder.Algebra
import Soat.FirstOrder.Term
import Soat.SecondOrder.Algebra
import Soat.SecondOrder.Signature.Lift

import Syntax.PreorderReasoning.Setoid

%ambiguity_depth 4
%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
projectAlgebra : SecondOrder.Algebra.Algebra (lift sig) -> (ctx : List sig.T)
  -> FirstOrder.Algebra.Algebra sig
projectAlgebra a ctx = MkAlgebra
  { raw = project a.raw ctx
  , algebra = MkIsAlgebra
    { equivalence = (a.setoidAt ctx).equivalence
    , semCong     = \op => a.algebra.semCong ctx _ . wrapIntro
    }
  }


public export
projectIsHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> {f : _} -> IsHomomorphism a b f
  -> (ctx : _)
  -> 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 (index b.setoid _) $
    |~ f _ _ (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 (index a.setoid _) $
      |~ 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 (reindex (\ty => (snd ty, fst ty ++ _)) a.setoid) _) $
            |~ 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 $
      (pwSetoid (a.setoidAt _) _).equivalence.reflexive _
    , semHomo = \op, tms' => CalcWith (index a.setoid _) $
      |~ 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 (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid) _) $
            |~ 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)) $
                  (pwSetoid (a.setoidAt _) _).equivalence.reflexive _))
    }
  }

renameBodyFunc : (f : ctx `Sublist` ctx')
  -> cast (flip Elem ctx) ~> (FreeAlgebra {sig = sig} (irrelevantCast (flip Elem ctx'))).setoid
renameBodyFunc f = mate (\_ => Done . curry f)

indexFunc : {ctx : List sig.T} -> (tms : Term sig (flip Elem ctx) ^ ts)
  -> cast (flip Elem ts) ~> (FreeAlgebra {sig = sig} (irrelevantCast (flip Elem ctx))).setoid
indexFunc tms = mate (\_ => 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 => bindTerm {a = Free _} (renameBodyFunc f).H)
  (\_, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair []))
  Done
  (\_, _, t, ts => bindTerm {a = Free _} (\_ => index ts) t)

public export
InitialIsAlgebra : (0 sig : _)
  -> SecondOrder.Algebra.IsAlgebra
       (lift sig)
       (Initial sig)
InitialIsAlgebra sig = MkIsAlgebra
  { equivalence = (bundle $ \(t, ctx) => index (FreeAlgebra (irrelevantCast (flip Elem ctx))).setoid t).equivalence
  , renameCong  = \t, f => bindTermCong ?renameCongEnv t
  , semCong     = \_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro
  , substCong   = \_, _, eq, eqs => bindTermCong'
    {rel = \_ => Equal}
    {a = FreeAlgebra (irrelevantCast (flip Elem _))}
    (\t, Refl => index eqs _)
    eq
  , renameId    = \t, ctx, tm =>
    (FreeAlgebra (irrelevantCast (flip Elem _))).setoid.equivalence.symmetric _ _ _ $
    bindUnique ?renameIdEnv idHomo (\i => Done' $ sym $ curryUncurry id i) $
    tm
  , renameComp  = \t, f, g, tm =>
    tmRelSym (\_ => MkSymmetric symmetric) $
    bindUnique
      ?renameCompEnv
      -- (ifunc (\_ => curry (transitive g f)))
      (compHomo (bindHomo ?renameCompFunc) (bindHomo ?renameCompFunc'))
      (\i => Done' $ sym $ curryUncurry (curry f . curry g) i) $
    tm
  , semNat      = \f, (MkOp (Op op)), tms =>
    Call' (MkOp op) $
    CalcWith (pwSetoid (FreeAlgebra (irrelevantCast (flip Elem _))).setoid _) $
    |~ bindTerms {a = Free _} (\_ => Done . curry f) (unwrap (MkPair []) tms)
    ~~ map (\_ => bindTerm {a = Free _} (\_ => Done . curry f)) (unwrap (MkPair []) tms)
      .=.(bindTermsIsMap {a = Free _} _ _)
    ~~ map (\_ => bindTerm {a = Free _} (\_ => Done . curry (reflexive {x = []} ++ f))) (unwrap (MkPair []) tms)
      ..<(mapIntro' (\t =>
            bindTermCong'
              {rel = \_ => Equal}
              {a = FreeAlgebra (irrelevantCast (flip Elem _))}
              (\_, Refl => Done' $ curryUncurry (curry f) _)) $
          (pwSetoid (FreeAlgebra (irrelevantCast (flip Elem _))).setoid _).equivalence.reflexive _)
    ~~ unwrap (MkPair []) (map (\ty => bindTerm {a = Free _} (\_ => Done . curry (reflexive {x = fst ty} ++ f))) tms)
      .=.(mapUnwrap (MkPair []) tms)
  , varNat      = \_, _ => Done' Refl
  , substNat    = \t, f, tm, tms =>
    bindUnique
      {a = FreeAlgebra (irrelevantCast (flip Elem _))}
      (indexFunc _)
      (compHomo
        (bindHomo ?substNatFunc)
        (bindHomo (indexFunc tms)))
      ?substNatCong
      -- (\i =>
      --   tmRelReflexive (\_ => MkReflexive reflexive) $
      --   sym $
      --   indexMap tms i)
      tm
  , substExnat  = \t, ctx, f, tm, tms =>
    bindUnique
      {a = FreeAlgebra (irrelevantCast (flip Elem _))}
      (indexFunc _)
      (compHomo
        (bindHomo (indexFunc tms))
        (bindHomo ?substExnatFunc))
      ?substExnatCong
      -- (\i =>
      --   tmRelReflexive (\_ => MkReflexive reflexive) $
      --   sym $
      --   indexShuffle f i)
      tm
  , substComm   = \t, ctx, tm, tms, tms' =>
    bindUnique
      {a = FreeAlgebra (irrelevantCast (flip Elem _))}
      (indexFunc _)
      (compHomo
        (bindHomo (indexFunc tms'))
        (bindHomo (indexFunc tms)))
      ?substCommCong
      -- (\i =>
      --   tmRelReflexive (\_ => MkReflexive reflexive) $
      --   sym $
      --   indexMap tms i)
      tm
  , substVarL   = ?substVarL -- \_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _
  , substVarR   = \t, ctx, tm =>
    (FreeAlgebra (irrelevantCast (flip Elem _))).setoid.equivalence.symmetric _ _ _ $
    bindUnique
      {a = FreeAlgebra (irrelevantCast (flip Elem _))}
      (indexFunc _)
      idHomo
      ?substVarRCong
      -- (\i =>
      --   tmRelReflexive (\_ => MkReflexive reflexive) $
      --   sym $
      --   indexTabulate Done i)
      tm
  , substCompat = \ctx, (MkOp (Op op)), tms, tms' =>
    Call' (MkOp op) $
    CalcWith (pwSetoid (FreeAlgebra (irrelevantCast (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 (irrelevantCast (flip Elem _))}
            (\t, Refl => CalcWith (index (FreeAlgebra (irrelevantCast (flip Elem _))).setoid _) $
              |~ index (map (\_ => bindTerm {a = Free _} (\_ => Done . curry ([] {ys = []} ++ reflexive))) tms') _
              ~~ bindTerm {a = Free _} (\_ => Done . curry ([] {ys = []} ++ reflexive)) (index tms' _)
                .=.(indexMap tms' _)
              ~~ index tms' _
                ..<(bindUnique
                      ?substCompatEnv
                      idHomo
                      (\i => Done' $ sym $ trans (curryUncurry _ i) (curryUncurry id i))
                      (index tms' _)))) $
          (pwSetoid (FreeAlgebra (irrelevantCast (flip Elem _))).setoid _).equivalence.reflexive $
          unwrap (MkPair []) tms)
    ~~ unwrap (MkPair []) (map ((Initial sig).extendSubst ctx tms') tms)
      .=.(mapUnwrap (MkPair []) tms)
  }
-- InitialIsAlgebra sig = MkIsAlgebra
--   (\(t, ctx) => tmRelEq (\_ => equiv) t)
--   (\t, f => bindTermCong {a = FreeAlgebra (irrelevantCast (flip Elem _))} (renameBodyFunc f))
--   (\_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro)
--   (\_, _, eq, eqs => bindTermCong'
--     {a = FreeAlgebra (irrelevantCast (flip Elem _))}
--     (\t, Refl => index eqs _)
--     eq)
--   (\t, ctx, tm =>
--     tmRelSym (\_ => MkSymmetric symmetric) $
--     bindUnique (renameBodyFunc reflexive) idHomo (\i => Done' $ sym $ curryUncurry id i) $
--     tm)
--   (\t, f, g, tm =>
--     tmRelSym (\_ => MkSymmetric symmetric) $
--     bindUnique
--       {a = FreeAlgebra (irrelevantCast (flip Elem _))}
--       (renameBodyFunc (transitive g f))
--       (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (renameBodyFunc g)))
--       (\i => Done' $ sym $ curryUncurry (curry f . curry g) i) $
--     tm)
--   (\f, (MkOp (Op op)), tms =>
--     Call' (MkOp op) $
--     Pointwise.map (\_ => tmRelReflexive (\_ => MkReflexive reflexive)) $
--     pwTrans (\_ => MkTransitive transitive) (equalImpliesPwEq $ bindTermsIsMap {a = Free _} _ _) $
--     pwTrans (\_ => MkTransitive transitive)
--       (mapIntro' (\t, eq =>
--         tmRelEqualIsEqual $
--         bindTermCong'
--           {rel = \_ => Equal}
--           {a = FreeAlgebra (irrelevantCast (flip Elem _))}
--           (\_, Refl => Done' $ sym $ curryUncurry (curry f) _) $
--         tmRelReflexive (\_ => MkReflexive reflexive) $
--         eq) $
--        equalImpliesPwEq Refl) $
--     equalImpliesPwEq $
--     mapUnwrap _ _)
--     -- Pointwise.map (\_ => tmRelReflexive (\_ => MkReflexive reflexive)) $
--     -- transitive (equalImpliesPwEq $ bindTermsIsMap {a = Free _} _ (unwrap (MkPair []) tms)) $
--     -- transitive
--     --   (mapIntro
--     --      (\t, eq =>
--     --        bindTermCong'
--     --          {v = irrelevantCast (flip Elem _)}
--     --          {a = FreeAlgebra (irrelevantCast (flip Elem _))}
--     --          (\_, Refl => Done' $ sym $ curryUncurry (curry f) _) $
--     --        tmRelReflexive (\_ => MkReflexive reflexive) $
--     --        eq) $
--     --    equalImpliesPwEq Refl) $
--     -- equalImpliesPwEq $
--     -- mapUnwrap
--     --   (MkPair [])
--     --   (\ty => (renameFunc (reflexive ++ f)).func (snd ty))
--     --   tms)
--   (\_, _ => Done' Refl)
--   (\t, f, tm, tms =>
--     bindUnique
--       {a = FreeAlgebra (irrelevantCast (flip Elem _))}
--       (indexFunc _)
--       (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (indexFunc tms)))
--       (\i =>
--         tmRelReflexive (\_ => MkReflexive reflexive) $
--         sym $
--         indexMap tms i)
--       tm)
--   (\t, ctx, f, tm, tms =>
--     bindUnique
--       {a = FreeAlgebra (irrelevantCast (flip Elem _))}
--       (indexFunc _)
--       (compHomo (bindHomo (indexFunc tms)) (bindHomo (renameBodyFunc f)))
--       (\i =>
--         tmRelReflexive (\_ => MkReflexive reflexive) $
--         sym $
--         indexShuffle f i)
--       tm)
--   (\t, ctx, tm, tms, tms' =>
--     bindUnique
--       {a = FreeAlgebra (irrelevantCast (flip Elem _))}
--       (indexFunc _)
--       (compHomo (bindHomo (indexFunc tms')) (bindHomo (indexFunc tms)))
--       (\i =>
--         tmRelReflexive (\_ => MkReflexive reflexive) $
--         sym $
--         indexMap tms i)
--       tm)
--   (\_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _)
--   (\t, ctx, tm =>
--     tmRelSym (\_ => MkSymmetric symmetric) $
--     bindUnique
--       {a = FreeAlgebra (irrelevantCast (flip Elem _))}
--       (indexFunc _)
--       idHomo
--       (\i =>
--         tmRelReflexive (\_ => MkReflexive reflexive) $
--         sym $
--         indexTabulate Done i)
--       tm)
--   (\ctx, (MkOp (Op op)), tms, tms' =>
--     Call' (MkOp op) $
--     tmsRelTrans (\_ => MkTransitive transitive)
--       (tmsRelSym (\_ => MkSymmetric symmetric) $
--        bindsUnique
--          {a = FreeAlgebra (irrelevantCast (flip Elem _))}
--          (indexFunc tms')
--          (bindHomo (indexFunc _))
--          (\i =>
--            (tmRelTrans (\_ => MkTransitive transitive)
--               (tmRelReflexive (\_ => MkReflexive reflexive) $
--                indexMap
--                  {f = (\_ => bindTerm {a = Free _} (\_ => Done . curry (uncurry (curry reflexive))))}
--                  tms'
--                  i) $
--             tmRelSym (\_ => MkSymmetric symmetric) $
--             (bindUnique
--                {a = FreeAlgebra (irrelevantCast (flip Elem _))}
--                (renameBodyFunc _)
--                idHomo
--                (\i =>
--                  Done' $
--                  sym $
--                  transitive (curryUncurry (curry reflexive) i) (curryUncurry id i))
--                (index tms' i))))
--          (unwrap (MkPair []) tms)) $
--     tmsRelReflexive (\_ => MkReflexive reflexive) $
--     mapUnwrap _ _)

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

-- public export
-- freeToInitialIsHomo : (0 sig : _) -> (ctx : List sig.T)
--   -> IsHomomorphism {sig = sig}
--        (FreeAlgebra (irrelevantCast (flip Elem ctx)))
--        (projectAlgebra (InitialAlgebra sig) ctx)
--        (\_ => Basics.id)
-- freeToInitialIsHomo sig ctx = MkIsHomomorphism
--   (\_ => id)
--   (\(MkOp op), tms =>
--     Call' (MkOp op) $
--     tmsRelSym (\_ => MkSymmetric symmetric) $
--     tmsRelReflexive (\_ => MkReflexive reflexive) $
--     transitive (unwrapWrap _ _) (mapId tms))

-- public export
-- freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T)
--   -> Homomorphism {sig = sig}
--        (FreeAlgebra (irrelevantCast (flip Elem ctx)))
--        (projectAlgebra (InitialAlgebra sig) ctx)
-- freeToInitialHomo sig ctx = MkHomomorphism (\_ => id) (freeToInitialIsHomo sig ctx)

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

-- public export
-- fromInitialIsHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
--   -> IsHomomorphism (InitialAlgebra sig) a (fromInitial a.raw)
-- fromInitialIsHomo a = MkIsHomomorphism
--   (\t , ctx => bindTermCong {a = projectAlgebra a ctx} (a.varFunc ctx))
--   (\t, f => bindUnique'
--     {v = irrelevantCast (flip Elem _)}
--     {a = projectAlgebra a _}
--     (compHomo (bindHomo (a.varFunc _)) (bindHomo (renameBodyFunc f)))
--     (compHomo (a.renameHomo f) (bindHomo (a.varFunc _)))
--     (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i))
--   (\ctx, (MkOp (Op op)), tms =>
--     a.algebra.semCong ctx (MkOp (Op op)) $
--     map (\_ => (a.algebra.equivalence _).equalImpliesEq) $
--     equalImpliesPwEq $
--     transitive
--       (cong (wrap _) $ bindTermsIsMap {a = project a.raw _} (\_ => a.raw.var) $ unwrap _ tms) $
--     transitive
--       (sym $ mapWrap (MkPair []) {f = \_ => fromInitial a.raw _ _} $ unwrap _ tms) $
--     cong (map _) $
--     wrapUnwrap tms)
--   (\_ => (a.algebra.equivalence _).reflexive)
--   (\t, ctx, tm, tms => bindUnique'
--     {v = irrelevantCast (flip Elem _)}
--     {a = projectAlgebra a _}
--     (compHomo (bindHomo (a.varFunc _)) (bindHomo (indexFunc tms)))
--     (compHomo (a.substHomo1 ctx _) (bindHomo (a.varFunc _)))
--     (\i =>
--       (a.algebra.equivalence _).transitive
--         (bindUnique
--           {v = irrelevantCast (flip Elem _)}
--           {a = projectAlgebra a _}
--           (a.varFunc _)
--           (bindHomo (a.varFunc _))
--           (\i => (a.algebra.equivalence _).reflexive)
--           (index tms i)) $
--       (a.algebra.equivalence _).symmetric $
--       (a.algebra.equivalence _).transitive
--         (a.algebra.substVarL ctx i _) $
--       (a.algebra.equivalence _).equalImpliesEq $
--       indexMap {f = \t => bindTerm {a = project a.raw ctx} (\_ => a.raw.var)} tms 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 = irrelevantCast (flip Elem _)}
--   {a = projectAlgebra a ctx}
--   (a.varFunc ctx)
--   (compHomo (projectHomo f ctx) (freeToInitialHomo sig ctx))
--   f.homo.varHomo