# HG changeset patch
# User atton
# Date 1481958421 0
# Node ID 62dfa11a8629fe902ae05b87e0030ddb4c79f169
# Parent  31b1b7cc43cd8d7251ddcd48693b1591b74b0ba5
Define tuple compose

diff -r 31b1b7cc43cd -r 62dfa11a8629 cbc/tuple.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbc/tuple.agda	Sat Dec 17 07:07:01 2016 +0000
@@ -0,0 +1,51 @@
+module tuple where
+
+open import Level
+
+
+
+_×_ : {l : Level} -> Set l -> Set l -> Set (suc l)
+_×_ {l} U V = {X : Set  l} -> (U -> V -> X) -> X
+
+<_,_> : {l : Level} {A B : Set l} -> A -> B -> A × B
+<_,_> {l} {A} {B} a b = \{X : Set l} -> \(x : A -> B -> X) -> x a b
+
+
+CodeSegment : {l : Level} -> Set l -> Set l -> Set l -> Set l -> Set (suc l)
+CodeSegment A B C D  = (A × B) -> (C × D)
+
+
+data Nat : Set where
+  O : Nat
+  S : Nat -> Nat
+
+data Unit : Set where
+  unit : Unit
+
+
+fst : {l : Level} {A B : Set l} -> A × B  -> A
+fst x = x (\a b -> a)
+
+snd : {l : Level} {A B : Set l} -> A × B -> B
+snd x = x (\a b -> b)
+
+
+
+plus1 : CodeSegment Nat Unit Nat Unit
+plus1 a = < (S (fst a)) , unit >
+
+
+twice' : Nat -> Nat
+twice' O     = O
+twice' (S n) = (S (S (twice' n)))
+
+twice : CodeSegment Nat Unit Nat Unit
+twice a = < (twice' (fst a)) , unit >
+
+
+_∘_ : {l : Level} {A B C D E F : Set l} -> CodeSegment C D E F -> CodeSegment A B C D -> CodeSegment A B E F
+_∘_ cs2 cs1 x = cs2 (cs1 x)
+
+
+hoge : CodeSegment Nat Unit Nat Unit
+hoge = ((plus1 ∘ twice) ∘ twice)