# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1395654325 -25200
# Node ID 203593ff1e607448f51ed5638b4e403304b784f8
# Parent  bda408a05c24bbf5012b35fd0809667da3fcfedb
add Tree example ( not yet worked )

diff -r bda408a05c24 -r 203593ff1e60 system-f.agda
--- a/system-f.agda	Sun Mar 23 07:31:20 2014 +0700
+++ b/system-f.agda	Mon Mar 24 16:45:25 2014 +0700
@@ -101,7 +101,7 @@
 
 
 Int : {l : Level } ( X : Set l ) → Set l
-Int {l} X = X → ( X → X ) → X
+Int X = X → ( X → X ) → X
 
 Zero : {l : Level } → { X : Set l } → Int X
 Zero {l} {X} = λ(x : X ) → λ(y : X → X ) → x
@@ -128,7 +128,7 @@
 lemma13 = refl
 
 It : {l : Level} {U : Set l} → U → ( U → U ) → Int U → U
-It {l} {U} u f t = t u f
+It u f t = t u f
 
 R : {l : Level} { U X : Set l}   → U → ( U → Int X →  U ) → Int _ → U 
 R {l} {U} {X} u v t =  π1 ( It {suc l} {U ×  Int X} (< u , Zero >) (λ (x : U × Int X) →  < v (π1 x) (π2 x) , S (π2 x) > ) t ) 
@@ -139,6 +139,10 @@
 -- RInt : {l : Level} { U X : Set l}   → Int U → ( Int U → Int X →  Int U ) → Int U → Int U 
 -- RInt {l} {U} {X} u v t =  π1 ( It {suc l} {Int U ×  Int X} (< u , Zero >) (λ (x : Int U × Int X) →  < v (π1 x) (π2 x) , S (π2 x) > ) t ) 
 
+-- bad adder which modifies input type
+add' : {l : Level} {X : Set l} → Int (Int X) → Int X → Int X
+add' x y = It y S x
+
 add : {l : Level} {X : Set l} → Int X → Int X → Int X
 add x y = λ z t → x (y z t) t
 
@@ -186,11 +190,27 @@
 l3 : {l : Level} {X X' : Set l} → List (Int X) (X')
 l3 = Cons n3 l2
 
-ListIt : {l : Level} {U W X : Set l} → W → ( U → W → W ) → List U W → W
-ListIt w f t = t w f
+ListIt : {l : Level} {U W : Set l} → (X : Set l) → W → ( U → W → W ) → List U W → W
+ListIt _ w f t = t w f
+
+-- Car : {l : Level} {U : Set l} {X : Set l} → List U _ → U  → U 
+-- Car x z = ListIt z ( λ u w → u ) x
+
+-- Cdr : {l : Level} {U : Set l} {X : Set l} → List U _ →  List U X
+-- Cdr w = λ x → λ y →  w x (λ x y   →  y) 
+
+-- lemma181 :{l : Level} {U : Set l} {X : Set l} → Car Zero l2 ≡ n2
+-- lemma181 = refl
+
+-- lemma182 :{l : Level} {U : Set l} {X : Set l} → Cdr l2 ≡ l1
+-- lemma182 = refl
 
 Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} → List U (Bool X) → Bool _
-Nullp {l} {U} {X} list = ListIt {suc l} {U} {Bool _} {X} (T X) (λ u w → (F X)) list
+Nullp {_} {_} {X} list = ListIt X (T X) (λ u w → (F X)) list
+
+-- bad append
+Append' : {l : Level} {U X : Set l} → List U (List U X) → List U X → List U X
+Append' {_} {_} {X} x y = ListIt X y Cons x
 
 Append : {l : Level} {U : Set l} {X : Set l} → List U X → List U X → List U X
 Append x y = λ s t → x (y s t) t
@@ -199,7 +219,7 @@
 lemma18 = refl
 
 Reverse : {l : Level} {U : Set l} {X : Set l} → List U (List U X) → List U X
-Reverse {l} {U} {X} x = ListIt {_} {U} {List U _} {X} Nil ( λ u w → Append w (Cons u Nil) ) x
+Reverse {l} {U} {X} x = ListIt X Nil ( λ u w → Append w (Cons u Nil) ) x
 
 lemma19 :{l : Level} {U : Set l} {X : Set l} → Reverse {_} {Int U} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil))
 lemma19 = refl
@@ -207,11 +227,17 @@
 Tree : {l : Level} → Set l → Set l → Set l
 Tree {l} = λ( U X : Set l)  → X → ( (U → X) →  X ) → X
 
-NilTree : {l : Level} (U : Set l) (X : Set l) → Tree U X
-NilTree U X = λ(x : X) → λ(y : (U → X) → X) → x
+NilTree : {l : Level} {U : Set l} {X : Set l} → Tree U X
+NilTree {l} {U} {X} = λ(x : X) → λ(y : (U → X) → X) → x
 
-Collect : {l : Level} (U : Set l) (X : Set l) → (U → X → ((U → X) → X) → X ) → Tree U X
-Collect U X f = λ(x : X) → λ(y : (U → X) → X) → y (λ(z : U) → f z x y )
+Collect : {l : Level} {U : Set l} {X : Set l} → (U → Tree U X ) → Tree U X
+Collect {l} {U} {X} f = λ(x : X) → λ(y : (U → X) → X) → y (λ(z : U) → f z x y )
 
 TreeIt : {l : Level} {U W X : Set l} → W → ( (U → W) → W ) → Tree U W → W
 TreeIt w h t = t w h
+
+t0 :  {l : Level} {X X' : Set l} → Tree (Bool X) X'
+t0 {l} {X} {X'} =  NilTree 
+
+t1 :  {l : Level} {X X' : Set l} → Tree (Bool X) X'
+t1 {l} {X} {X'} =  NilTree -- Collect (λ b → D b NilTree (λ c → Collect NilTree NilTree ))