1 files changed, 68 insertions, 10 deletions
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)