Initial.

Pair/Properties.lidr

+module Pair.Properties

Pair/tmp/Properties.idr

+module Pair.Properties
+
+import Isomorphism.Isomorphism
+import Isomorphism.Properties
+import FiniteAsSigmaType.Finite
+import FiniteAsSigmaType.Properties
+import Sigma.Sigma
+import Sigma.Operations
+
+
+|||
+public export
+tuplePairIso3 : {a, b, c : Type} -> Iso (a, b, c) ((a, b), c)
+tuplePairIso3 {a} {b} {c} = MkIso to from ok1 ok2
+  where to : (a, b, c) -> ((a, b), c)
+        to (x, y, z) = ((x, y), z)
+        from : ((a, b), c) -> (a, b, c)
+        from ((x, y), z) = (x, y, z)
+        ok1 : (x : ((a, b), c)) -> to (from x) = x
+        ok1 ((x, y), z) = Refl
+        ok2 : (x : (a, b, c)) -> from (to x) = x
+        ok2 (x, y, z) = Refl  
+
+|||
+public export
+tuplePairIso4 : {a, b, c, d : Type} -> Iso (a, b, c, d) ((a, b, c), d)
+tuplePairIso4 {a} {b} {c} {d} = MkIso to from ok1 ok2
+  where to : (a, b, c, d) -> ((a, b, c), d)
+        to (w, x, y, z) = ((w, x, y), z)
+        from : ((a, b, c), d) -> (a, b, c, d)
+        from ((w, x, y), z) = (w, x, y, z)
+        ok1 : (x : ((a, b, c), d)) -> to (from x) = x
+        ok1 ((w, x, y), z) = Refl
+        ok2 : (x : (a, b, c, d)) -> from (to x) = x
+        ok2 (w, x, y, z) = Refl  
+
+
+-- Finiteness of pairs and tuples
+
+||| If |P| and |Q| are finite, |(P , Q)| is finite
+public export
+finitePair : {a, b : Type} -> Finite a -> Finite b -> Finite (a, b)
+finitePair = finiteProduct
+
+
+||| Tuples of 3 finite types are finite
+public export
+finiteTuple3 : {a, b, c : Type} -> 
+               Finite a -> Finite b -> Finite c -> 
+               Finite (a, b, c)
+finiteTuple3 {a} {b} {c} fa fb fc = 
+  MkSigma _ (isoTrans (tuplePairIso3 {a} {b} {c}) (outr fabc)) where
+    fab  : Finite (a, b)
+    fab  = finiteProduct fa fb
+    fabc : Finite ((a, b), c)
+    fabc = finiteProduct fab fc
+
+
+||| Tuples of 4 finite types are finite
+public export
+finiteTuple4 : {a, b, c, d : Type} -> 
+               Finite a -> Finite b -> Finite c ->  Finite d -> 
+               Finite (a, b, c, d)
+finiteTuple4 {a} {b} {c} {d} fa fb fc fd =
+  MkSigma _ (isoTrans (tuplePairIso4 {a} {b} {c} {d}) (outr fabcd)) where
+    fabc  : Finite (a, b, c)
+    fabc  = finiteTuple3 fa fb fc
+    fabcd : Finite ((a, b, c), d)
+    fabcd = finiteProduct fabc fd