WIP: define semantics in Idris.semantics-with-proof

7 files changed, 430 insertions, 41 deletions

diff --git a/src/Encoded/Arith.idr b/src/Encoded/Arith.idr
index d2f83bc..5097664 100644
--- a/src/Encoded/Arith.idr
+++ b/src/Encoded/Arith.idr
@@ -1,9 +1,14 @@
 module Encoded.Arith
 
+import Data.Nat
 import Encoded.Bool
 import Encoded.Pair
+import Syntax.PreorderReasoning
+import Term.Semantics
 import Term.Syntax
 
+-- Utilities -------------------------------------------------------------------
+
 export
 rec : {ty : Ty} -> Term (N ~> ty ~> (N * ty ~> ty) ~> ty) ctx
 rec = Abs $ Abs $ Abs $
@@ -32,10 +37,14 @@ pred = Abs'
   (\n => App
     (Rec n
       (Const Zero)
-      (Abs' (\f =>
-        Rec (App f [<Zero])
-          (Abs' (\k => Rec k (Suc Zero) (Const Zero)))
-          (Const $ Abs' (\k => Rec k (Suc Zero) (Abs' Suc . shift f))))))
+      (Abs $ Abs $
+        let f = Var (There Here) in
+        let k = Var Here in
+        Rec k
+          (Suc Zero)
+          (Const $ Rec (App f [<Zero])
+            Zero
+            (Const $ Suc $ App f [<Lit 1]))))
     [<Lit 1])
 
 export
@@ -76,6 +85,83 @@ divmod = Abs $ Abs $
     (App pair [<Zero, Zero])
     (Abs' (\p =>
       App if'
-        [<App lte [<shift d, App snd [<p]]
+        [<App lte [<shift d, App (Abs' Suc . snd) [<p]]
         , App pair [<Suc (App fst [<p]), Zero]
         , App mapSnd [<Abs' Suc, p]]))
+
+-- Properties ------------------------------------------------------------------
+
+-- Redefinition in Idris
+
+namespace Sem
+  public export
+  recHelper : Nat -> a -> ((Nat, a) -> a) -> (Nat, a)
+  recHelper k z s = rec k (0, z) (\p => (S (fst p), s p))
+
+  public export
+  rec' : Nat -> a -> ((Nat, a) -> a) -> a
+  rec' k z s = snd (recHelper k z s)
+
+  public export
+  slowPred : Nat -> Nat
+  slowPred n = rec' n 0 fst
+
+  public export
+  predHelper : Nat -> Nat -> Nat
+  predHelper n =
+    rec n
+      (const 0)
+      (\f, k =>
+        rec k
+          1
+          (const $ rec (f 0)
+            0
+            (const $ S $ f 1)))
+
+  public export
+  pred' : Nat -> Nat
+  pred' n = predHelper n 1
+
+  public export
+  divmodStep : Nat -> (Nat, Nat) -> (Nat, Nat)
+  divmodStep d (div, mod) =
+    if d <= S mod
+    then
+      (S div, 0)
+    else
+      (div, S mod)
+
+  public export
+  divmod : Nat -> Nat -> (Nat, Nat)
+  divmod n d = rec n (0, 0) (divmodStep d)
+
+-- Proofs
+
+export
+fstRecHelper : (k : Nat) -> (0 z : a) -> (0 s : (Nat, a) -> a) -> fst (recHelper k z s) = k
+fstRecHelper 0 z s = Refl
+fstRecHelper (S k) z s = cong S $ fstRecHelper k z s
+
+export
+slowPredCorrect : (k : Nat) -> slowPred k = pred k
+slowPredCorrect 0 = Refl
+slowPredCorrect (S k) = fstRecHelper k 0 fst
+
+export
+predCorrect : (k : Nat) -> pred' k = pred k
+predCorrect 0 = Refl
+predCorrect 1 = Refl
+predCorrect (S (S k)) = cong S $ predCorrect (S k)
+
+-- divmodSmall :
+--   (d, div, mod : Nat) ->
+--   {auto 0 ok : NonZero d} ->
+  -- mod <= d
+
+export
+divmodCorrect :
+  (n, d : Nat) ->
+  {auto 0 ok : NonZero d} ->
+  n = fst (divmod n d) * d + snd (divmod n d)
+divmodCorrect 0 d = Refl
+divmodCorrect (S k) d = ?divmodCorrect_rhs_1
diff --git a/src/Encoded/Bool.idr b/src/Encoded/Bool.idr
index 11bb894..b8eec99 100644
--- a/src/Encoded/Bool.idr
+++ b/src/Encoded/Bool.idr
@@ -3,18 +3,13 @@ module Encoded.Bool
 import Term.Semantics
 import Term.Syntax
 
+-- Type ------------------------------------------------------------------------
+
 export
 B : Ty
 B = N
 
-export
-Show (TypeOf B) where
-  show 0 = "true"
-  show (S k) = "false"
-
-export
-toBool : TypeOf B -> Bool
-toBool = (== 0)
+-- Universal Properties --------------------------------------------------------
 
 export
 True : Term B ctx
@@ -31,6 +26,8 @@ if' = Abs' (\b =>
     (Abs $ Const $ Var Here)
     (Const $ Const $ Abs $ Var Here))
 
+-- Utilities -------------------------------------------------------------------
+
 export
 and : Term (B ~> B ~> B) ctx
 and = Abs' (\b => App if' [<b, Id, Const False])
@@ -46,3 +43,50 @@ not = Abs' (\b => App if' [<b, False, True])
 export
 isZero : Term (N ~> B) ctx
 isZero = Id
+
+-- Semantics -------------------------------------------------------------------
+
+-- Conversion to Idris
+
+export
+toBool : TypeOf B -> Bool
+toBool = (== 0)
+
+export
+fromBool : Bool -> TypeOf B
+fromBool b = if b then 0 else 1
+
+export
+toFromId : (b : Bool) -> toBool (fromBool b) = b
+toFromId False = Refl
+toFromId True = Refl
+
+-- Redefinition in Idris
+
+namespace Sem
+  public export
+  True : TypeOf B
+  True = 0
+
+  public export
+  False : TypeOf B
+  False = 1
+
+  public export
+  if' : TypeOf B -> a -> a -> a
+  if' b = rec b (\t, _ => t) (\_, _, f => f)
+
+-- Homomorphism
+
+export
+trueHomo : toBool True = True
+trueHomo = Refl
+
+export
+falseHomo : toBool False = False
+falseHomo = Refl
+
+export
+ifHomo : (b : Bool) -> (0 x, y : a) -> if' (fromBool b) x y = if b then x else y
+ifHomo True x y = Refl
+ifHomo False x y = Refl
diff --git a/src/Encoded/Fin.idr b/src/Encoded/Fin.idr
index 901c612..fc56c50 100644
--- a/src/Encoded/Fin.idr
+++ b/src/Encoded/Fin.idr
@@ -8,12 +8,13 @@ import Encoded.Pair
 import Term.Semantics
 import Term.Syntax
 
+-- Type ------------------------------------------------------------------------
+
 export
 Fin : Nat -> Ty
 Fin k = N
 
-oldShow : Nat -> String
-oldShow = show
+-- Universal Morphisms ---------------------------------------------------------
 
 export
 zero : Term (Fin (S k)) ctx
@@ -35,6 +36,8 @@ export
 induct : {ty : Ty} -> Term (Fin (S k) ~> ty ~> (Fin k * ty ~> ty) ~> ty) ctx
 induct = rec
 
+-- Utilities -------------------------------------------------------------------
+
 export
 forget : Term (Fin k ~> N) ctx
 forget = Id
diff --git a/src/Encoded/Pair.idr b/src/Encoded/Pair.idr
index 32bb06c..d9bfae5 100644
--- a/src/Encoded/Pair.idr
+++ b/src/Encoded/Pair.idr
@@ -1,24 +1,18 @@
 module Encoded.Pair
 
+import Control.Function.FunExt
 import Encoded.Bool
 import Encoded.Union
 import Term.Semantics
 import Term.Syntax
 
+-- Type ------------------------------------------------------------------------
+
 export
 (*) : Ty -> Ty -> Ty
 ty1 * ty2 = B ~> (ty1 <+> ty2)
 
-export
-[ShowPair]
-{ty1, ty2 : Ty} ->
-Show (TypeOf ty1) =>
-Show (TypeOf ty2) =>
-Show (TypeOf (ty1 * ty2)) where
-  show f = fastConcat
-    [ "(", show (sem prL [<] (f $ sem True [<]))
-    , ", ", show (sem prR [<] (f $ sem False [<]))
-    , ")"]
+-- Universal Properties --------------------------------------------------------
 
 export
 pair : {ty1, ty2 : Ty} -> Term (ty1 ~> ty2 ~> (ty1 * ty2)) ctx
@@ -36,6 +30,8 @@ export
 snd : {ty1, ty2 : Ty} -> Term ((ty1 * ty2) ~> ty2) ctx
 snd = Abs $ App (prR . Var Here) [<False]
 
+-- Utilities -------------------------------------------------------------------
+
 export
 bimap :
   {ty1, ty1', ty2, ty2' : Ty} ->
@@ -64,3 +60,65 @@ uncurry = Abs $ Abs $
   let f = Var $ There Here in
   let p = Var Here in
   App f [<App fst [<p], App snd [<p]]
+
+-- Semantics -------------------------------------------------------------------
+
+-- Conversion to Idris
+
+export
+toPair : {ty1, ty2 : Ty} -> TypeOf (ty1 * ty2) -> (TypeOf ty1, TypeOf ty2)
+toPair f = (prL (f True), prR (f False))
+
+export
+fromPair : {ty1, ty2 : Ty} -> (TypeOf ty1, TypeOf ty2) -> TypeOf (ty1 * ty2)
+fromPair (x, y) b = if' b (inL x) (inR y)
+
+export
+toFromId :
+  FunExt =>
+  {ty1, ty2 : Ty} ->
+  (p : (TypeOf ty1, TypeOf ty2)) ->
+  toPair {ty1, ty2} (fromPair {ty1, ty2} p) = p
+toFromId (x, y) = cong2 (,) (retractL {ty1, ty2} x) (retractR {ty1, ty2} y)
+
+-- Redefinition in Idris
+
+namespace Sem
+  public export
+  pair : {ty1, ty2 : Ty} -> TypeOf ty1 -> TypeOf ty2 -> TypeOf (ty1 * ty2)
+  pair x y b = if' b (inL x) (inR y)
+
+  public export
+  fst : {ty1, ty2 : Ty} -> TypeOf (ty1 * ty2) -> TypeOf ty1
+  fst f = prL (f True)
+
+  public export
+  snd : {ty1, ty2 : Ty} -> TypeOf (ty1 * ty2) -> TypeOf ty2
+  snd f = prR (f False)
+
+-- Proofs
+
+export
+pairHomo :
+  FunExt =>
+  {ty1, ty2 : Ty} ->
+  (0 x : TypeOf ty1) ->
+  (0 y : TypeOf ty2) ->
+  toPair {ty1, ty2} (pair {ty1, ty2} x y) = (x, y)
+pairHomo x y = irrelevantEq $ toFromId (x, y)
+
+export
+fstHomo :
+  FunExt =>
+  {ty1, ty2 : Ty} ->
+  (0 p : (TypeOf ty1, TypeOf ty2)) ->
+  fst {ty1, ty2} (fromPair {ty1, ty2} p) = fst p
+fstHomo (x, y) = cong fst (pairHomo x y)
+
+export
+sndHomo :
+  FunExt =>
+  {ty1, ty2 : Ty} ->
+  (0 p : (TypeOf ty1, TypeOf ty2)) ->
+  snd {ty1, ty2} (fromPair {ty1, ty2} p) = snd p
+sndHomo (x, y) = cong snd (pairHomo x y)
diff --git a/src/Encoded/Sum.idr b/src/Encoded/Sum.idr
index e3729f9..4b65868 100644
--- a/src/Encoded/Sum.idr
+++ b/src/Encoded/Sum.idr
@@ -4,24 +4,35 @@ import public Data.List
 import public Data.List.Elem
 import public Data.List.Quantifiers
 
+import Control.Function.FunExt
 import Encoded.Bool
 import Encoded.Pair
 import Encoded.Union
+import Syntax.PreorderReasoning
 import Term.Semantics
 import Term.Syntax
 
--- Binary Sums -----------------------------------------------------------------
+%ambiguity_depth 4
+
+-- Auxilliary Functions --------------------------------------------------------
+
+public export
+mapNonEmpty : NonEmpty xs -> NonEmpty (map f xs)
+mapNonEmpty IsNonEmpty = IsNonEmpty
+
+-- Types -----------------------------------------------------------------------
 
 export
 (+) : Ty -> Ty -> Ty
 ty1 + ty2 = B * (ty1 <+> ty2)
 
 export
-{ty1, ty2 : Ty} -> Show (TypeOf ty1) => Show (TypeOf ty2) => Show (TypeOf (ty1 + ty2)) where
-  show p =
-    if toBool (sem fst [<] p)
-    then fastConcat ["Left (", show (sem (prL . snd) [<] p), ")"]
-    else fastConcat ["Right (", show (sem (prR . snd) [<] p), ")"]
+Sum : (tys : List Ty) -> {auto 0 ok : NonEmpty tys} -> Ty
+Sum = foldr1 (+)
+
+-- Universal Properties --------------------------------------------------------
+
+-- Binary
 
 export
 left : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 + ty2)) ctx
@@ -40,6 +51,8 @@ case' = Abs' (\t =>
     , Const $ Abs $ App (Var Here . prR . snd) [<shift t]
     ])
 
+-- Utilty
+
 export
 either : {ty1, ty2, ty : Ty} -> Term ((ty1 ~> ty) ~> (ty2 ~> ty) ~> (ty1 + ty2) ~> ty) ctx
 either = Abs $ Abs $ Abs $
@@ -48,15 +61,7 @@ either = Abs $ Abs $ Abs $
   let x = Var Here in
   App case' [<x, f, g]
 
--- N-ary Sums ------------------------------------------------------------------
-
-public export
-mapNonEmpty : NonEmpty xs -> NonEmpty (map f xs)
-mapNonEmpty IsNonEmpty = IsNonEmpty
-
-export
-Sum : (tys : List Ty) -> {auto 0 ok : NonEmpty tys} -> Ty
-Sum = foldr1 (+)
+-- N-ary
 
 export
 any :
@@ -78,3 +83,106 @@ tag :
 tag {tys = [_]} Here = Id
 tag {tys = _ :: _ :: _} Here = left
 tag {tys = _ :: _ :: _} (There i) = right . tag i
+
+-- Semantics -------------------------------------------------------------------
+
+-- Conversion to Idris
+
+export
+toEither :
+  {ty1, ty2 : Ty} ->
+  TypeOf (ty1 + ty2) ->
+  Either (TypeOf ty1) (TypeOf ty2)
+toEither x =
+  if' (Sem.fst x)
+    (Left (prL $ Sem.snd x))
+    (Right (prR $ Sem.snd x))
+
+export
+fromEither :
+  {ty1, ty2 : Ty} ->
+  Either (TypeOf ty1) (TypeOf ty2) ->
+  TypeOf (ty1 + ty2)
+fromEither (Left x) = pair Sem.True (inL x)
+fromEither (Right x) = pair Sem.False (inR x)
+
+export
+toFromId :
+  FunExt =>
+  {ty1, ty2 : Ty} ->
+  (x : Either (TypeOf ty1) (TypeOf ty2)) ->
+  toEither {ty1, ty2} (fromEither {ty1, ty2} x) = x
+toFromId (Left x) =
+  rewrite retractL {ty1 = B, ty2 = ty1 <+> ty2} Sem.True in
+  cong Left $ Calc $
+    |~ (Sem.prL {ty1, ty2} . Sem.prR . Sem.inR . Sem.inL) x
+    ~~ (prL {ty1, ty2} . inL) x                             ...(cong prL $ retractR (inL x))
+    ~~ x                                                    ...(retractL {ty1, ty2} x)
+toFromId (Right x) =
+  rewrite retractL {ty1 = B, ty2 = ty1 <+> ty2} Sem.False in
+  cong Right $ Calc $
+    |~ (Sem.prR {ty1, ty2} . Sem.prR . Sem.inR . Sem.inR) x
+    ~~ (prR {ty1, ty2} . inR) x                             ...(cong prR $ retractR (inR x))
+    ~~ x                                                    ...(retractR {ty1, ty2} x)
+
+-- Redefinition in Idris
+
+namespace Sem
+  public export
+  left : {ty1, ty2 : Ty} -> TypeOf ty1 -> TypeOf (ty1 + ty2)
+  left x = pair Sem.True (inL x)
+
+  public export
+  right : {ty1, ty2 : Ty} -> TypeOf ty2 -> TypeOf (ty1 + ty2)
+  right x = pair Sem.False (inR x)
+
+  public export
+  case' :
+    {ty1, ty2 : Ty} ->
+    TypeOf (ty1 + ty2) ->
+    (TypeOf ty1 -> a) ->
+    (TypeOf ty2 -> a) ->
+    a
+  case' x =
+    if' (Sem.fst x)
+      (\f, _ => f $ prL $ Sem.snd x)
+      (\_, g => g $ prR $ Sem.snd x)
+
+-- Homomorphism
+
+export
+leftHomo :
+  FunExt =>
+  {ty1, ty2 : Ty} ->
+  (0 x : TypeOf ty1) ->
+  toEither {ty1, ty2} (left {ty1, ty2} x) = Left x
+leftHomo x = irrelevantEq $ toFromId (Left x)
+
+export
+rightHomo :
+  FunExt =>
+  {ty1, ty2 : Ty} ->
+  (0 x : TypeOf ty2) ->
+  toEither {ty1, ty2} (right {ty1, ty2} x) = Right x
+rightHomo x = irrelevantEq $ toFromId (Right x)
+
+export
+caseHomo :
+  FunExt =>
+  {ty1, ty2 : Ty} ->
+  (x : Either (TypeOf ty1) (TypeOf ty2)) ->
+  (f : TypeOf ty1 -> a) ->
+  (g : TypeOf ty2 -> a) ->
+  case' {ty1, ty2} (fromEither {ty1, ty2} x) f g = either f g x
+caseHomo (Left x) f g =
+  rewrite retractL {ty1 = B, ty2 = ty1 <+> ty2} Sem.True in
+  cong f $ Calc $
+    |~ (Sem.prL {ty1, ty2} . Sem.prR . Sem.inR . Sem.inL) x
+    ~~ (prL {ty1, ty2} . inL) x                             ...(cong prL $ retractR (inL x))
+    ~~ x                                                    ...(retractL {ty1, ty2} x)
+caseHomo (Right x) f g =
+  rewrite retractL {ty1 = B, ty2 = ty1 <+> ty2} Sem.False in
+  cong g $ Calc $
+    |~ (Sem.prR {ty1, ty2} . Sem.prR . Sem.inR . Sem.inR) x
+    ~~ (prR {ty1, ty2} . inR) x                             ...(cong prR $ retractR (inR x))
+    ~~ x                                                    ...(retractR {ty1, ty2} x)
diff --git a/src/Encoded/Union.idr b/src/Encoded/Union.idr
index 00b07e7..2243ab9 100644
--- a/src/Encoded/Union.idr
+++ b/src/Encoded/Union.idr
@@ -1,8 +1,11 @@
 module Encoded.Union
 
+import Control.Function.FunExt
+import Syntax.PreorderReasoning
+import Term.Semantics
 import Term.Syntax
 
--- Binary Union ----------------------------------------------------------------
+-- Type ------------------------------------------------------------------------
 
 export
 (<+>) : Ty -> Ty -> Ty
@@ -11,6 +14,8 @@ N <+> (ty2 ~> ty2') = ty2 ~> (N <+> ty2')
 (ty1 ~> ty1') <+> N = ty1 ~> (ty1' <+> N)
 (ty1 ~> ty1') <+> (ty2 ~> ty2') = (ty1 <+> ty2) ~> (ty1' <+> ty2')
 
+-- Universal Property ----------------------------------------------------------
+
 export
 swap : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> (ty2 <+> ty1)) ctx
 swap {ty1 = N, ty2 = N} = Id
@@ -40,3 +45,82 @@ inR = swap . inL
 export
 prR : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty2) ctx
 prR = prL . swap
+
+-- Semantics -------------------------------------------------------------------
+
+-- Redefinition in Idris
+
+namespace Sem
+  public export
+  swap : {ty1, ty2: Ty} -> TypeOf (ty1 <+> ty2) -> TypeOf (ty2 <+> ty1)
+  swap {ty1 = N, ty2 = N} = id
+  swap {ty1 = N, ty2 = ty2 ~> ty2'} = \f => Sem.swap . f
+  swap {ty1 = ty1 ~> ty1', ty2 = N} = \f => Sem.swap . f
+  swap {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} = \f => Sem.swap . f . Sem.swap
+
+  public export
+  inL : {ty1, ty2 : Ty} -> TypeOf ty1 -> TypeOf (ty1 <+> ty2)
+
+  public export
+  prL : {ty1, ty2 : Ty} -> TypeOf (ty1 <+> ty2) -> TypeOf ty1
+
+  inL {ty1 = N, ty2 = N} = id
+  inL {ty1 = N, ty2 = ty2 ~> ty2'} = \n => const (Sem.inL n)
+  inL {ty1 = ty1 ~> ty1', ty2 = N} = \f => Sem.inL . f
+  inL {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} = \f => Sem.inL . f . Sem.prL
+
+  prL {ty1 = N, ty2 = N} = id
+  prL {ty1 = N, ty2 = ty2 ~> ty2'} = \f => Sem.prL (f $ arb ty2)
+  prL {ty1 = ty1 ~> ty1', ty2 = N} = \f => Sem.prL . f
+  prL {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} = \f => Sem.prL . f . Sem.inL
+
+  public export
+  inR : {ty1, ty2 : Ty} -> TypeOf ty2 -> TypeOf (ty1 <+> ty2)
+  inR = Sem.swap . inL
+
+  public export
+  prR : {ty1, ty2 : Ty} -> TypeOf (ty1 <+> ty2) -> TypeOf ty2
+  prR = prL . Sem.swap
+
+-- Proofs
+
+export
+swapInvolutive :
+  FunExt =>
+  {ty1, ty2 : Ty} ->
+  (0 x : TypeOf (ty1 <+> ty2)) ->
+  Sem.swap {ty1 = ty2, ty2 = ty1} (Sem.swap {ty1, ty2} x) = x
+swapInvolutive {ty1 = N, ty2 = N} x = Refl
+swapInvolutive {ty1 = N, ty2 = ty2 ~> ty2'} x = funExt (\y => swapInvolutive (x y))
+swapInvolutive {ty1 = ty1 ~> ty1', ty2 = N} x = funExt (\y => swapInvolutive (x y))
+swapInvolutive {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} x = funExt (\y =>
+  Calc $
+    |~ (Sem.swap . Sem.swap . x . Sem.swap . Sem.swap) y
+    ~~ (x . Sem.swap . Sem.swap) y                       ...(swapInvolutive (x _))
+    ~~ x y                                               ...(cong x $ swapInvolutive y))
+
+export
+retractL :
+  FunExt =>
+  {ty1, ty2 : Ty} ->
+  (0 x : TypeOf ty1) ->
+  prL {ty1, ty2} (inL {ty1, ty2} x) = x
+retractL {ty1 = N, ty2 = N} x = Refl
+retractL {ty1 = N, ty2 = ty2 ~> ty2'} x = retractL {ty1 = N, ty2 = ty2'} x
+retractL {ty1 = ty1 ~> ty1', ty2 = N} x = funExt (\y => retractL (x y))
+retractL {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} x = funExt (\y =>
+  Calc $
+    |~ (Sem.prL . Sem.inL . x . Sem.prL {ty2} . Sem.inL) y
+    ~~ (x . Sem.prL {ty2} . Sem.inL) y                     ...(retractL (x _))
+    ~~ x y                                                 ...(cong x $ retractL {ty2} y))
+
+export
+retractR :
+  FunExt =>
+  {ty1, ty2 : Ty} ->
+  (0 x : TypeOf ty2) ->
+  prR {ty1, ty2} (inR {ty1, ty2} x) = x
+retractR x = Calc $
+  |~ (Sem.prL . Sem.swap . Sem.swap . Sem.inL) x
+  ~~ (Sem.prL . Sem.inL) x                       ...(cong prL $ swapInvolutive (inL x))
+  ~~ x                                           ...(retractL x)
diff --git a/src/Term/Semantics.idr b/src/Term/Semantics.idr
index 2e61040..dd76f62 100644
--- a/src/Term/Semantics.idr
+++ b/src/Term/Semantics.idr
@@ -10,6 +10,7 @@ TypeOf : Ty -> Type
 TypeOf N = Nat
 TypeOf (ty ~> ty') = TypeOf ty -> TypeOf ty'
 
+public export
 rec : Nat -> a -> (a -> a) -> a
 rec 0 x f = x
 rec (S k) x f = f (rec k x f)
@@ -66,3 +67,8 @@ fullSem' (Rec (MakePair t (MakePair u v _ `Over` thin) _)) = do
 export
 sem : Term ty ctx -> All TypeOf ctx -> TypeOf ty
 sem t = runIdentity (sem' t)
+
+export
+arb : (ty : Ty) -> TypeOf ty
+arb N = 0
+arb (ty ~> ty') = const (arb ty')