Make proofs relevant.

4 files changed, 32 insertions, 32 deletions

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index fef5871..5f166d5 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -30,8 +30,8 @@ MkRawAlgebra u sem = MakeRawAlgebra u (\o => uncurry (sem o))
 public export
 record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel a.U) where
   constructor MkIsAlgebra
-  0 equivalence : IEquivalence a.U rel
-  0 semCong     : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity}
+  equivalence : IEquivalence a.U rel
+  semCong     : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity}
     -> Pointwise rel tms tms' -> rel t (a.sem op tms) (a.sem op tms')
 
 public export
@@ -51,8 +51,8 @@ record IsHomomorphism
   (f : (t : sig.T) -> a.raw.U t -> b.raw.U t)
   where
   constructor MkIsHomomorphism
-  0 cong    : (t : sig.T) -> {tm, tm' : a.raw.U t} -> a.rel t tm tm' -> b.rel t (f t tm) (f t tm')
-  0 semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
+  cong    : (t : sig.T) -> {tm, tm' : a.raw.U t} -> a.rel t tm tm' -> b.rel t (f t tm) (f t tm')
+  semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
     -> b.rel t (f t (a.raw.sem op tms)) (b.raw.sem op (map f tms))
 
 public export
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 5f5e57b..af6539b 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -116,12 +116,12 @@ public export
 FreeAlgebra : ISetoid sig.T -> Algebra sig
 FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v)
 
-public export 0
+public export
 bindTermCong : {a : Algebra sig} -> (env : SetoidEnvironment x a.setoid)
   -> {t : sig.T} -> {tm, tm' : Term sig x.U t} -> (~=~) x.relation t tm tm'
   -> a.rel t (bindTerm {a = a.raw} env.f tm) (bindTerm {a = a.raw} env.f tm')
 
-public export 0
+public export
 bindTermsCong : {a : Algebra sig} -> (env : SetoidEnvironment x a.setoid)
   -> {ts : List sig.T} -> {tms, tms' : Term sig x.U ^ ts} -> Pointwise ((~=~) x.relation) tms tms'
   -> Pointwise a.rel (bindTerms {a = a.raw} env.f tms) (bindTerms {a = a.raw} env.f tms')
@@ -148,15 +148,15 @@ public export
 bind : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) -> Homomorphism (FreeAlgebra v) a
 bind env = MkHomomorphism _ (bindHomo _ env)
 
-public export 0
-bindUnique : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid)
+public export
+bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid)
   -> (f : Homomorphism (FreeAlgebra v) a)
   -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.f t i))
   -> {t : sig.T} -> (tm : Term sig v.U t)
   -> a.rel t (f.f t tm) ((Term.bind {a = a} env).f t tm)
 
-public export 0
-bindsUnique : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid)
+public export
+bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid)
   -> (f : Homomorphism (FreeAlgebra v) a)
   -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.f t i))
   -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
diff --git a/src/Soat/Relation.idr b/src/Soat/Relation.idr
index bf5a631..9a394c2 100644
--- a/src/Soat/Relation.idr
+++ b/src/Soat/Relation.idr
@@ -70,6 +70,6 @@ IEquivalence x rel = (i : a) -> Soat.Relation.Equivalence (x i) (rel i)
 public export
 record ISetoid (a : Type) where
   constructor MkISetoid
-  0 U           : a -> Type
-  0 relation    : IRel U
-  0 equivalence : IEquivalence U relation
+  0 U         : a -> Type
+  0 relation  : IRel U
+  equivalence : IEquivalence U relation
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 3ce1726..bc3defb 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -34,28 +34,28 @@ record RawAlgebra (0 sig : Signature) where
 public export
 record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncurry a.U)) where
   constructor MkIsAlgebra
-  0 equivalence : IEquivalence (uncurry a.U) rel
+  equivalence : IEquivalence (uncurry a.U) rel
   -- Congruences
-  0 renameCong  : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx')
+  renameCong  : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx')
     -> {tm, tm' : a.U t ctx} -> rel (t, ctx) tm tm'
     -> rel (t, ctx') (a.rename t f tm) (a.rename t f tm')
-  0 semCong     : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
+  semCong     : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
     -> {tms, tms' : extend a.U ctx ^ op.arity}
     -> Pointwise (extendRel {U = a.U} rel ctx) tms tms'
     -> rel (t, ctx) (a.sem ctx op tms) (a.sem ctx op tms')
-  0 substCong   : (t : sig.T) -> (ctx : List sig.T)
+  substCong   : (t : sig.T) -> (ctx : List sig.T)
     -> forall ctx' . {tm, tm' : a.U t ctx'} -> rel (t, ctx') tm tm'
     -> {tms, tms' : flip a.U ctx ^ ctx'} -> Pointwise (\t => rel (t, ctx)) tms tms'
     -> rel (t, ctx) (a.subst t ctx tm tms) (a.subst t ctx tm' tms')
   -- rename is functorial
-  0 renameId    : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
+  renameId    : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
     -> rel (t, ctx) (a.rename t {ctx = ctx} Relation.reflexive tm) tm
-  0 renameComp  : (t : sig.T)
+  renameComp  : (t : sig.T)
     -> forall ctx, ctx', ctx'' . (f : ctx' `Sublist` ctx'') -> (g : ctx `Sublist` ctx')
     -> (tm : a.U t ctx)
     -> rel (t, ctx'') (a.rename t (transitive g f) tm) (a.rename t f $ a.rename t g tm)
   -- sem are natural transformation
-  0 semNat      : forall ctx, ctx' . (f : ctx `Sublist` ctx') -> {t : sig.T} -> (op : Op sig t)
+  semNat      : forall ctx, ctx' . (f : ctx `Sublist` ctx') -> {t : sig.T} -> (op : Op sig t)
     -> (tms : extend a.U ctx ^ op.arity)
     -> rel (t, ctx')
          (a.rename t f $ a.sem ctx op tms)
@@ -63,33 +63,33 @@ record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncur
           map (\ty => a.rename (snd ty) (Relation.reflexive {x = fst ty} ++ f)) $
           tms)
   -- var is natural transformation
-  0 varNat      : forall t, ctx, ctx' . (f : ctx `Sublist` ctx') -> (i : Elem t ctx)
+  varNat      : forall t, ctx, ctx' . (f : ctx `Sublist` ctx') -> (i : Elem t ctx)
     -> rel (t, ctx') (a.rename t f $ a.var i) (a.var $ curry f i)
   -- subst is natural transformation
-  0 substNat    : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx')
+  substNat    : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx')
     -> forall ctx'' . (tm : a.U t ctx'') -> (tms : flip a.U ctx ^ ctx'')
     -> rel (t, ctx')
          (a.rename t f $ a.subst t ctx tm tms)
          (a.subst t ctx' tm $ map (\t => a.rename t f) tms)
   -- subst is extranatural transformation
-  0 substExnat  : (t : sig.T) -> (ctx : List sig.T)
+  substExnat  : (t : sig.T) -> (ctx : List sig.T)
     -> forall ctx', ctx'' . (f : ctx' `Sublist` ctx'')
     -> (tm : a.U t ctx') -> (tms : flip a.U ctx ^ ctx'')
     -> rel (t, ctx) (a.subst t ctx (a.rename t f tm) tms) (a.subst t ctx tm (shuffle f tms))
   -- var, subst is a monoid
-  0 substComm   : (t : sig.T) -> (ctx : List sig.T)
+  substComm   : (t : sig.T) -> (ctx : List sig.T)
     -> forall ctx', ctx'' . (tm : a.U t ctx'')
     -> (tms : flip a.U ctx' ^ ctx'') -> (tms' : flip a.U ctx ^ ctx')
     -> rel (t, ctx)
          (a.subst t ctx (a.subst t ctx' tm tms) tms')
          (a.subst t ctx tm $ map (\t, tm => a.subst t ctx tm tms') tms)
-  0 substVarL   : forall t . (ctx : List sig.T) -> forall ctx' . (i : Elem t ctx')
+  substVarL   : forall t . (ctx : List sig.T) -> forall ctx' . (i : Elem t ctx')
     -> (tms : flip a.U ctx ^ ctx')
     -> rel (t, ctx) (a.subst t ctx (a.var i) tms) (index tms i)
-  0 substVarR   : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
+  substVarR   : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
     -> rel (t, ctx) (a.subst t ctx {ctx' = ctx} tm $ tabulate a.var) tm
   -- sem, var and subst are compatible
-  0 substCompat : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
+  substCompat : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
     -> forall ctx' . (tms : extend a.U ctx' ^ op.arity) -> (tms' : flip a.U ctx ^ ctx')
     -> rel (t, ctx)
          (a.subst t ctx (a.sem ctx' op tms) tms')
@@ -117,18 +117,18 @@ record IsHomomorphism
   (f : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx)
   where
   constructor MkIsHomomorphism
-  0 cong       : (t : sig.T) -> (ctx : List sig.T) -> {tm, tm' : a.raw.U t ctx}
+  cong       : (t : sig.T) -> (ctx : List sig.T) -> {tm, tm' : a.raw.U t ctx}
     -> a.rel (t, ctx) tm tm' -> b.rel (t, ctx) (f t ctx tm) (f t ctx tm')
-  0 renameHomo : (t : sig.T) -> forall ctx, ctx' . (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx)
+  renameHomo : (t : sig.T) -> forall ctx, ctx' . (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx)
     -> b.rel (t, ctx') (f t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ f t ctx tm)
-  0 semHomo    : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
+  semHomo    : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
     -> (tms : extend a.raw.U ctx ^ op.arity)
     -> b.rel (t, ctx)
          (f t ctx $ a.raw.sem ctx op tms)
          (b.raw.sem ctx op $ map (\ty => f (snd ty) (fst ty ++ ctx)) tms)
-  0 varHomo    : forall t, ctx . (i : Elem t ctx)
+  varHomo    : forall t, ctx . (i : Elem t ctx)
     -> b.rel (t, ctx) (f t ctx $ a.raw.var i) (b.raw.var i)
-  0 substHomo  : (t : sig.T) -> (ctx : List sig.T) -> forall ctx' . (tm : a.raw.U t ctx')
+  substHomo  : (t : sig.T) -> (ctx : List sig.T) -> forall ctx' . (tm : a.raw.U t ctx')
     -> (tms : flip a.raw.U ctx ^ ctx')
     -> b.rel (t, ctx)
          (f t ctx $ a.raw.subst t ctx tm tms)