1 files changed, 51 insertions, 11 deletions
diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr
index a2500e9..959702d 100644
--- a/src/Core/Thinning.idr
+++ b/src/Core/Thinning.idr
@@ -56,6 +56,37 @@ view (IsThinner IsBase) = Drop (id _)
 view (IsThinner (IsDrop thin)) = Drop (IsThinner thin)
 view (IsThinner (IsKeep thin)) = Keep (IsThinner thin)
 
+-- Composition -----------------------------------------------------------------
+
+comp : Thinner m n -> Thinner k m -> Thinner k n
+comp IsBase thin2 = IsDrop thin2
+comp (IsDrop thin1) thin2 = IsDrop (comp thin1 thin2)
+comp (IsKeep thin1) IsBase = IsDrop thin1
+comp (IsKeep thin1) (IsDrop thin2) = IsDrop (comp thin1 thin2)
+comp (IsKeep thin1) (IsKeep thin2) = IsKeep (comp thin1 thin2)
+
+export
+(.) : m `Thins` n -> k `Thins` m -> k `Thins` n
+IsId . thin2 = thin2
+IsThinner thin1 . IsId = IsThinner thin1
+IsThinner thin1 . IsThinner thin2 = IsThinner (comp thin1 thin2)
+
+-- Specific Cases
+
+export
+compRightId : (thin : m `Thins` n) -> thin . id m = thin
+compRightId IsId = Refl
+compRightId (IsThinner thin) = Refl
+
+export
+compKeep :
+  (thin1 : m `Thins` n) ->
+  (thin2 : k `Thins` m) ->
+  keep thin1 . keep thin2 = keep (thin1 . thin2)
+compKeep IsId thin2 = Refl
+compKeep (IsThinner thin1) IsId = Refl
+compKeep (IsThinner thin1) (IsThinner thin2) = Refl
+
 -- Weakening -------------------------------------------------------------------
 
 wkn' : Fin m -> Thinner m n -> Fin n
@@ -69,17 +100,26 @@ wkn : Fin m -> m `Thins` n -> Fin n
 wkn i IsId = i
 wkn i (IsThinner thin) = wkn' i thin
 
--- Composition -----------------------------------------------------------------
+-- Properties
 
-comp : Thinner m n -> Thinner k m -> Thinner k n
-comp IsBase thin2 = IsDrop thin2
-comp (IsDrop thin1) thin2 = IsDrop (comp thin1 thin2)
-comp (IsKeep thin1) IsBase = IsDrop thin1
-comp (IsKeep thin1) (IsDrop thin2) = IsDrop (comp thin1 thin2)
-comp (IsKeep thin1) (IsKeep thin2) = IsKeep (comp thin1 thin2)
+wkn'Homo :
+  (i : Fin k) ->
+  (thin2 : Thinner m n) ->
+  (thin1 : Thinner k m) ->
+  wkn' (wkn' i thin1) thin2 = wkn' i (comp thin2 thin1)
+wkn'Homo i IsBase thin1 = Refl
+wkn'Homo i (IsDrop thin2) thin1 = cong FS (wkn'Homo i thin2 thin1)
+wkn'Homo i (IsKeep thin2) IsBase = Refl
+wkn'Homo i (IsKeep thin2) (IsDrop thin1) = cong FS (wkn'Homo i thin2 thin1)
+wkn'Homo FZ (IsKeep thin2) (IsKeep thin1) = Refl
+wkn'Homo (FS i) (IsKeep thin2) (IsKeep thin1) = cong FS (wkn'Homo i thin2 thin1)
 
 export
-(.) : m `Thins` n -> k `Thins` m -> k `Thins` n
-IsId . thin2 = thin2
-IsThinner thin1 . IsId = IsThinner thin1
-IsThinner thin1 . IsThinner thin2 = IsThinner (comp thin1 thin2)
+wknHomo :
+  (i : Fin k) ->
+  (thin1 : k `Thins` m) ->
+  (thin2 : m `Thins` n) ->
+  wkn (wkn i thin1) thin2 = wkn i (thin2 . thin1)
+wknHomo i IsId thin2 = sym $ cong (wkn i) $ compRightId thin2
+wknHomo i (IsThinner thin1) IsId = Refl
+wknHomo i (IsThinner thin1) (IsThinner thin2) = wkn'Homo i thin2 thin1