Make unions a pseudo-built-in type.

3 files changed, 0 insertions, 44 deletions

diff --git a/src/Encoded/Pair.idr b/src/Encoded/Pair.idr
index 42adde5..5873e40 100644
--- a/src/Encoded/Pair.idr
+++ b/src/Encoded/Pair.idr
@@ -1,7 +1,6 @@
 module Encoded.Pair
 
 import Encoded.Bool
-import Encoded.Union
 import Term.Syntax
 
 export
diff --git a/src/Encoded/Sum.idr b/src/Encoded/Sum.idr
index 6c6da6a..fd0543a 100644
--- a/src/Encoded/Sum.idr
+++ b/src/Encoded/Sum.idr
@@ -4,7 +4,6 @@ import public Data.SnocList.Operations
 
 import Encoded.Bool
 import Encoded.Pair
-import Encoded.Union
 import Term.Syntax
 
 -- Binary Sums -----------------------------------------------------------------
diff --git a/src/Encoded/Union.idr b/src/Encoded/Union.idr
deleted file mode 100644
index 00b07e7..0000000
--- a/src/Encoded/Union.idr
+++ /dev/null
@@ -1,42 +0,0 @@
-module Encoded.Union
-
-import Term.Syntax
-
--- Binary Union ----------------------------------------------------------------
-
-export
-(<+>) : Ty -> Ty -> Ty
-N <+> N = N
-N <+> (ty2 ~> ty2') = ty2 ~> (N <+> ty2')
-(ty1 ~> ty1') <+> N = ty1 ~> (ty1' <+> N)
-(ty1 ~> ty1') <+> (ty2 ~> ty2') = (ty1 <+> ty2) ~> (ty1' <+> ty2')
-
-export
-swap : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> (ty2 <+> ty1)) ctx
-swap {ty1 = N, ty2 = N} = Id
-swap {ty1 = N, ty2 = ty2 ~> ty2'} = Abs' (\f => swap . f)
-swap {ty1 = ty1 ~> ty1', ty2 = N} = Abs' (\f => swap . f)
-swap {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} = Abs' (\f => swap . f . swap)
-
-export
-inL : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 <+> ty2)) ctx
-export
-prL : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty1) ctx
-
-inL {ty1 = N, ty2 = N} = Id
-inL {ty1 = N, ty2 = ty2 ~> ty2'} = Abs' (\n => Const (App inL [<n]))
-inL {ty1 = ty1 ~> ty1', ty2 = N} = Abs' (\f => inL . f)
-inL {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} = Abs' (\f => inL . f . prL)
-
-prL {ty1 = N, ty2 = N} = Id
-prL {ty1 = N, ty2 = ty2 ~> ty2'} = Abs' (\t => App prL [<App t [<Arb]])
-prL {ty1 = ty1 ~> ty1', ty2 = N} = Abs' (\t => prL . t)
-prL {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} = Abs' (\t => prL . t . inL)
-
-export
-inR : {ty1, ty2 : Ty} -> Term (ty2 ~> (ty1 <+> ty2)) ctx
-inR = swap . inL
-
-export
-prR : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty2) ctx
-prR = prL . swap