|
16
|
1 module tuple where
|
|
|
2
|
|
|
3 open import Level
|
|
|
4
|
|
|
5
|
|
|
6
|
|
|
7 _×_ : {l : Level} -> Set l -> Set l -> Set (suc l)
|
|
|
8 _×_ {l} U V = {X : Set l} -> (U -> V -> X) -> X
|
|
|
9
|
|
|
10 <_,_> : {l : Level} {A B : Set l} -> A -> B -> A × B
|
|
|
11 <_,_> {l} {A} {B} a b = \{X : Set l} -> \(x : A -> B -> X) -> x a b
|
|
|
12
|
|
|
13
|
|
|
14 CodeSegment : {l : Level} -> Set l -> Set l -> Set l -> Set l -> Set (suc l)
|
|
|
15 CodeSegment A B C D = (A × B) -> (C × D)
|
|
|
16
|
|
|
17
|
|
|
18 data Nat : Set where
|
|
|
19 O : Nat
|
|
|
20 S : Nat -> Nat
|
|
|
21
|
|
|
22 data Unit : Set where
|
|
|
23 unit : Unit
|
|
|
24
|
|
|
25
|
|
|
26 fst : {l : Level} {A B : Set l} -> A × B -> A
|
|
|
27 fst x = x (\a b -> a)
|
|
|
28
|
|
|
29 snd : {l : Level} {A B : Set l} -> A × B -> B
|
|
|
30 snd x = x (\a b -> b)
|
|
|
31
|
|
|
32
|
|
|
33
|
|
|
34 plus1 : CodeSegment Nat Unit Nat Unit
|
|
|
35 plus1 a = < (S (fst a)) , unit >
|
|
|
36
|
|
|
37
|
|
|
38 twice' : Nat -> Nat
|
|
|
39 twice' O = O
|
|
|
40 twice' (S n) = (S (S (twice' n)))
|
|
|
41
|
|
|
42 twice : CodeSegment Nat Unit Nat Unit
|
|
|
43 twice a = < (twice' (fst a)) , unit >
|
|
|
44
|
|
|
45
|
|
|
46 _∘_ : {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
|
|
|
47 _∘_ cs2 cs1 x = cs2 (cs1 x)
|
|
|
48
|
|
|
49
|
|
|
50 hoge : CodeSegment Nat Unit Nat Unit
|
|
|
51 hoge = ((plus1 ∘ twice) ∘ twice)
|
