From ab6f8d8aa077b3a8e7040b82c91afe4e67b6237b Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 22 Apr 2023 16:12:49 +0100
Subject: Package a visible induction statement.

---
 src/Core/Reducible.idr | 49 +++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 47 insertions(+), 2 deletions(-)

diff --git a/src/Core/Reducible.idr b/src/Core/Reducible.idr
index fe31a7a..ea37093 100644
--- a/src/Core/Reducible.idr
+++ b/src/Core/Reducible.idr
@@ -18,10 +18,12 @@ data Level = Small | Large
 
 %name Level l
 
+export
 Sized Level where
   size Small = 0
   size Large = 1
 
+public export
 record LogicalRelation (eq : Equality) where
   constructor MkLogRel
   0 TypeRed : forall n. Env n -> Term n -> Type
@@ -29,6 +31,7 @@ record LogicalRelation (eq : Equality) where
   0 TermRed : forall n. (env : Env n) -> (t, a : Term n) -> TypeRed {n} env a -> Type
   0 TermEq : forall n. (env : Env n) -> (t, u, a : Term n) -> TypeRed {n} env a -> Type
 
+public export
 data TypeRed :
   (eq : Equality) ->
   (l : Level) ->
@@ -36,6 +39,7 @@ data TypeRed :
   (env : Env n) ->
   (a : Term n) ->
   Type
+public export
 data TypeEq :
   (eq : Equality) ->
   (l : Level) ->
@@ -44,6 +48,7 @@ data TypeEq :
   (a, b : Term n) ->
   TypeRed eq l rec {n} env a ->
   Type
+public export
 data TermRed :
   (eq : Equality) ->
   (l : Level) ->
@@ -52,6 +57,7 @@ data TermRed :
   (t, a : Term n) ->
   TypeRed eq l rec {n} env a ->
   Type
+public export
 data TermEq :
   (eq : Equality) ->
   (l : Level) ->
@@ -61,8 +67,9 @@ data TermEq :
   TypeRed eq l rec {n} env a ->
   Type
 
--- -- Neutrals
+-- Neutrals
 
+public export
 record NeutralTyRed
   (eq : Equality)
   (l : Level)
@@ -78,6 +85,7 @@ record NeutralTyRed
   0 ntrl : Neutral a'
   prf : eq.NtrlEq env (Element a' ntrl) (Element a' ntrl) Set
 
+public export
 record NeutralTyEq
   (eq : Equality)
   (l : Level)
@@ -94,6 +102,7 @@ record NeutralTyEq
   0 ntrl : Neutral b'
   prf : eq.NtrlEq env (Element red.a' red.ntrl) (Element b' ntrl) Set
 
+public export
 record NeutralTmRed
   (eq : Equality)
   (l : Level)
@@ -110,6 +119,7 @@ record NeutralTmRed
   0 ntrl : Neutral t'
   prf : eq.NtrlEq env (Element t' ntrl) (Element t' ntrl) a
 
+public export
 record NeutralTmEq
   (eq : Equality)
   (l : Level)
@@ -132,6 +142,7 @@ record NeutralTmEq
 
 -- Set
 
+public export
 record SetTyRed
   (eq : Equality)
   (l : Level)
@@ -145,6 +156,7 @@ record SetTyRed
   tyWf' : TypeWf env Set
   prf : Smaller Small l
 
+public export
 record SetTyEq
   (eq : Equality)
   (l : Level)
@@ -158,6 +170,7 @@ record SetTyEq
   steps : TypeReduce env b Set
   tyWf' : TypeWf env Set
 
+public export
 record SetTmRed
   (eq : Equality)
   (l : Level)
@@ -175,6 +188,7 @@ record SetTmRed
   prf : eq.TermEq env t' t' a
   tyRed : (rec Small red.prf).TypeRed env t
 
+public export
 record SetTmEq
   (eq : Equality)
   (l : Level)
@@ -200,6 +214,7 @@ record SetTmEq
 
 -- Pi
 
+public export
 record PiTyRed
   (eq : Equality)
   (l : Level)
@@ -243,6 +258,7 @@ record PiTyRed
       (subst g (Wkn thin :< pure u))
       (codRed thinWf red)
 
+public export
 record PiTyEq
   (eq : Equality)
   (l : Level)
@@ -276,6 +292,7 @@ record PiTyEq
       (subst g (Wkn thin :< pure t))
       (red.codRed thinWf red')
 
+public export
 record PiTmRed
   (eq : Equality)
   (l : Level)
@@ -317,6 +334,7 @@ record PiTmRed
       (subst red.g (Wkn thin :< pure u))
       (red.codRed thinWf red')
 
+public export
 record PiTmEq
   (eq : Equality)
   (l : Level)
@@ -375,9 +393,36 @@ data TermEq where
 
 -- Induction -------------------------------------------------------------------
 
+public export
+levelAccRecurse : (sizeL : Nat) -> (l' : Level) -> (size l' `LT` sizeL) -> SizeAccessible l'
+levelAccRecurse (S l) l' (LTESucc prf) =
+  Access (\l'', prf' => levelAccRecurse l l'' $ transitive prf' prf)
+
+public export
+levelAccessible : (l : Level) -> SizeAccessible l
+levelAccessible l = Access (levelAccRecurse $ size l)
+
+public export
+levelIndHelper :
+  {0 p : Level -> Type} ->
+  (step : (l : Level) -> ((l' : Level) -> Smaller l' l -> p l') -> p l) ->
+  (l : Level) ->
+  (0 acc : SizeAccessible l) ->
+  p l
+levelIndHelper step l (Access rec) = step l (\l', prf => levelIndHelper step l' $ rec l' prf)
+
+public export
+levelInd :
+  {0 p : Level -> Type} ->
+  (step : (l : Level) -> ((l' : Level) -> Smaller l' l -> p l') -> p l) ->
+  (l : Level) ->
+  p l
+levelInd step l = levelIndHelper step l (levelAccessible l)
+
+public export
 LogRel : (eq : Equality) -> Level -> LogicalRelation eq
 LogRel eq =
-  sizeRec $ \l, rec =>
+  levelInd $ \l, rec =>
     MkLogRel
       (TypeRed eq l rec)
       (TypeEq eq l rec)
-- 
cgit v1.2.3