diff options
Diffstat (limited to 'src/Data/Term.idr')
| -rw-r--r-- | src/Data/Term.idr | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/src/Data/Term.idr b/src/Data/Term.idr index 385b864..973ff3d 100644 --- a/src/Data/Term.idr +++ b/src/Data/Term.idr @@ -93,6 +93,32 @@ subComp : f . pure r .=. f . r subComp f r i = Refl +export +compCong2 : + {0 f1, f2 : Fin k -> Term sig n} -> + {0 g1, g2 : Fin j -> Term sig k} -> + f1 .=. f2 -> + g1 .=. g2 -> + f1 . g1 .=. f2 . g2 +compCong2 prf1 prf2 i = Calc $ + |~ f1 <$> g1 i + ~~ f1 <$> g2 i ...(cong (f1 <$>) $ prf2 i) + ~~ f2 <$> g2 i ...(subExtensional prf1 (g2 i)) + +compCongL : + {0 f1, f2 : Fin k -> Term sig n} -> + f1 .=. f2 -> + (0 g : Fin j -> Term sig k) -> + f1 . g .=. f2 . g +compCongL prf g = compCong2 prf (\_ => Refl) + +compCongR : + (0 f : Fin k -> Term sig n) -> + {0 g1, g2 : Fin j -> Term sig k} -> + g1 .=. g2 -> + f . g1 .=. f . g2 +compCongR f prf = compCong2 (\_ => Refl) prf + -- Injectivity ----------------------------------------------------------------- export |