1 files changed, 60 insertions, 2 deletions

diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 973ff3d..bfeb360 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -2,7 +2,10 @@ module Data.Term
 
 import public Data.DPair
 import public Data.Vect
+
+import Data.Fin.Extra
 import Data.Vect.Properties.Map
+
 import Syntax.PreorderReasoning
 
 %prefix_record_projections off
@@ -88,12 +91,20 @@ subAssoc f g (Op op ts) = cong (Op op) $ Calc $
 
 export
 subComp :
-  (f : Fin k -> Term sig n) ->
-  (r : Fin j -> Fin k) ->
+  (0 f : Fin k -> Term sig n) ->
+  (0 r : Fin j -> Fin k) ->
   f . pure r .=. f . r
 subComp f r i = Refl
 
 export
+subAssoc' :
+  (f : Fin k -> Term sig n) ->
+  (g : Fin j -> Fin k) ->
+  (t : Term sig j) ->
+  (f . g) <$> t = f <$> pure g <$> t
+subAssoc' f g = subAssoc f (Var . g)
+
+export
 compCong2 :
   {0 f1, f2 : Fin k -> Term sig n} ->
   {0 g1, g2 : Fin j -> Term sig k} ->
@@ -119,6 +130,53 @@ compCongR :
   f . g1 .=. f . g2
 compCongR f prf = compCong2 (\_ => Refl) prf
 
+-- Substitution is a Semigroupoid ----------------------------------------------
+
+export
+(++) :
+  {j : Nat} ->
+  (Fin j -> Term sig n) ->
+  (Fin k -> Term sig n) ->
+  Fin (j + k) -> Term sig n
+f ++ g = either f g . splitSum
+
+export
+appendWeakenN :
+  {j : Nat} ->
+  (0 f : Fin j -> Term sig n) ->
+  (0 g : Fin k -> Term sig n) ->
+  (f ++ g) . weakenN k .=. f
+appendWeakenN f g i = cong (either f g) $ splitSumOfWeakenN i
+
+export
+appendShift :
+  {j : Nat} ->
+  (0 f : Fin j -> Term sig n) ->
+  (0 g : Fin k -> Term sig n) ->
+  (f ++ g) . shift j .=. g
+appendShift f g i = cong (either f g) $ splitSumOfShift i
+
+export
+appendCong2 :
+  {j : Nat} ->
+  {0 f : Fin j -> Term sig n} ->
+  {0 g : Fin k -> Term sig n} ->
+  {0 h : Fin (j + k) -> Term sig n} ->
+  h . weakenN k .=. f ->
+  h . shift j .=. g ->
+  h .=. f ++ g
+appendCong2 prf1 prf2 x with (splitSum x) proof prf
+  _ | Left i = Calc $
+    |~ h x
+    ~~ h (indexSum (splitSum x)) ..<(cong h (indexOfSplitSumInverse x))
+    ~~ h (weakenN k i)           ...(cong (h . indexSum) prf)
+    ~~ f i                       ...(prf1 i)
+  _ | Right i = Calc $
+    |~ h x
+    ~~ h (indexSum (splitSum x)) ..<(cong h (indexOfSplitSumInverse x))
+    ~~ h (shift j i)             ...(cong (h . indexSum) prf)
+    ~~ g i                       ...(prf2 i)
+
 -- Injectivity -----------------------------------------------------------------
 
 export