--- a/freyd.agda	Mon Jan 06 17:18:13 2014 +0900
+++ b/freyd.agda	Sat Mar 15 10:15:54 2014 +0900
@@ -36,7 +36,7 @@
       uniqueness  : ( a : Obj A ) →  ( f : Hom A i a ) → A [ f ≈  initial a ]
 
 
--- A has initial object if it has PreInitial-SmallFullSubcategory
+-- A complete catagory has initial object if it has PreInitial-SmallFullSubcategory
 
 open NTrans
 open Limit

--- a/record-ex.agda	Mon Jan 06 17:18:13 2014 +0900
+++ b/record-ex.agda	Sat Mar 15 10:15:54 2014 +0900
@@ -35,6 +35,12 @@
 ya : A
 ya = and1 z
 
+lemma1 : A ∧ B → A
+lemma1 a =  and1 a
+
+lemma2 : A → B → A ∧ B 
+lemma2 a b =  record { and1 = a ; and2 = b }
+
 open  import  Relation.Binary.PropositionalEquality
 
 data Nat : Set where

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/system-f.agda	Sat Mar 15 10:15:54 2014 +0900
@@ -0,0 +1,66 @@
+open import Level
+open import Relation.Binary.PropositionalEquality
+
+module system-f {l : Level} where
+
+postulate A : Set
+postulate B : Set
+
+data _∨_  (A B : Set) : Set where
+  or1 : A -> A ∨ B
+  or2 : B -> A ∨ B
+
+lemma01 : A -> A ∨ B
+lemma01 a = or1 a
+
+lemma02 : B -> A ∨ B
+lemma02 b = or2 b
+
+lemma03 : {C : Set} -> (A ∨ B) -> (A -> C) -> (B -> C) -> C
+lemma03 (or1 a) ac bc = ac a
+lemma03 (or2 b) ac bc = bc b
+
+postulate U : Set l
+postulate V : Set l
+
+
+Bool = {X : Set l} -> X -> X -> X
+
+T : Bool
+T = \{X : Set l} -> \(x y : X) -> x
+
+F : Bool
+F = \{X : Set l} -> \(x y : X) -> y
+
+D : {U : Set l} -> U -> U -> Bool -> U
+D {U} u v t = t {U} u v
+
+lemma04 : {u v : U} -> D u v T ≡  u
+lemma04 = refl
+
+lemma05 : {u v : U} -> D u v F ≡  v
+lemma05 = refl
+
+_×_ : Set l -> Set l ->  Set (suc l)
+U × V =  {X : Set l} -> (U -> V -> X)  -> X 
+
+<_,_> : {U V : Set l} -> U -> V -> (U ×  V) 
+<_,_> {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v
+
+π1 : {U V : Set l} -> (U ×  V) -> U
+π1 {U} {V}  t = t {U} (\(x : U) -> \(y : V) -> x)
+
+π2 : {U V : Set l} -> (U ×  V) -> V
+π2 {U} {V}  t = t {V} (\(x : U) -> \(y : V) -> y)
+
+lemma06 : {U V : Set l } -> {u : U } -> {v : V} -> π1 ( < u , v > ) ≡  u
+lemma06 = refl
+
+lemma07 : {U V : Set l } -> {u : U } -> {v : V} -> π2 ( < u , v > ) ≡  v
+lemma07 = refl
+
+hoge : {U V : Set l} -> U -> V  -> (U ×  V)
+hoge u v = < u , v >
+
+-- lemma08 :  (t : U ×  V)  -> < π1 t  , π2 t > ≡ t
+-- lemma08 t = {!!}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/system-t.agda	Sat Mar 15 10:15:54 2014 +0900
@@ -0,0 +1,146 @@
+module system-t where
+open  import  Relation.Binary.PropositionalEquality
+
+record _×_ ( U : Set ) ( V : Set )   :  Set where
+    field
+       π1 : U
+       π2 : V
+
+<_,_> : {U V : Set} -> U -> V -> U × V
+< u , v >  = record {π1 = u ; π2 = v }
+
+open _×_
+
+postulate U : Set
+postulate V : Set
+
+postulate v : V
+postulate u : U
+
+f : U -> V
+f = \u -> v
+
+
+UV : Set
+UV = U × V
+
+uv : U × V
+uv  = < u , v >
+
+lemma01 : π1  < u , v >   ≡ u
+lemma01 = refl
+
+lemma02 : π2  < u , v >   ≡ v
+lemma02 = refl
+
+lemma03 : (uv : U × V ) → < π1  uv , π2 uv >   ≡ uv
+lemma03 uv = refl
+
+lemma04 : (λ x →  f x ) u ≡  f u
+lemma04 = refl
+
+lemma05 : (λ  x → f x ) ≡  f
+lemma05 = refl
+
+nn = λ (x : U ) →  u
+n1 = λ ( x : U ) →  f x
+
+data Bool : Set where
+  T : Bool 
+  F : Bool
+
+D : { U : Set } -> U -> U -> Bool -> U 
+D u v T = u 
+D u v F = v
+
+data Int : Set where 
+    zero : Int
+    S : Int →  Int
+
+pred : Int -> Int
+pred zero = zero
+pred (S t) = t
+
+R : { U : Set } -> U -> ( U -> Int -> U ) -> Int -> U
+R u v zero = u 
+R u v ( S t ) = v (R u v t) t
+
+null : Int -> Bool
+null zero = T
+null (S _)  = F
+
+It : { T : Set } -> T -> (T -> T) -> Int -> T
+It u v zero = u
+It u v ( S t ) = v (It u v t )
+
+R' : { T : Set } -> T -> ( T -> Int -> T ) -> Int -> T
+R' u v t = π1 ( It ( < u , zero > ) (λ x →  < v (π1 x) (π2 x) , S (π2 x) > ) t )
+
+sum : Int -> Int -> Int
+sum x y = R y ( λ z -> λ w -> S z ) x
+
+mul : Int -> Int -> Int
+mul x y = R zero ( λ z -> λ w -> sum y z ) x 
+
+sum' : Int -> Int -> Int
+sum' x y = R' y ( λ z -> λ w -> S z ) x
+
+mul' : Int -> Int -> Int
+mul' x y = R' zero ( λ z -> λ w -> sum y z ) x
+
+fact : Int -> Int
+fact  n = R  (S zero) (λ z -> λ w -> mul (S w) z ) n
+
+fact' : Int -> Int
+fact' n = R' (S zero) (λ z -> λ w -> mul (S w) z ) n
+
+f3 = fact (S (S (S zero)))
+f3' = fact' (S (S (S zero)))
+
+lemma21 : f3 ≡ f3'
+lemma21 = refl
+
+lemma07 : { U : Set } -> ( u : U ) -> ( v : U -> Int -> U ) ->( t :  Int ) -> 
+        (π2 (It < u , zero > (λ x → < v (π1 x) (π2 x) , S (π2 x) >) t )) ≡  t
+lemma07 u v zero   =  refl
+lemma07 u v (S t)  =  cong ( \x -> S x ) ( lemma07 u v t )
+
+lemma06 : { U : Set } -> ( u : U ) -> ( v : U -> Int -> U ) ->( t :  Int ) -> ( (R u v t) ≡  (R' u v t ))
+lemma06 u v zero = refl 
+lemma06 u v (S t) =  trans  ( cong ( \x ->  v x t )  ( lemma06 u v t ) ) 
+                            ( cong ( \y ->  v (R' u v t) y ) (sym ( lemma07 u v t ) ) )
+
+lemma08 : ( n m : Int ) -> ( sum' n m ≡ sum n m )
+lemma08 zero _ = refl 
+lemma08 (S t) y =  cong ( \x -> S x ) ( lemma08 t y ) 
+
+lemma09 : ( n m : Int ) -> ( mul' n m ≡ mul n m )
+lemma09 zero _ = refl 
+lemma09 (S t) y =  cong ( \x -> sum y x) ( lemma09 t y ) 
+
+lemma10 : ( n : Int ) -> ( fact n  ≡ fact n )
+lemma10 zero = refl 
+lemma10 (S t) =  cong ( \x -> mul (S t) x ) ( lemma10 t ) 
+
+lemma11 : ( n : Int ) -> ( fact n  ≡ fact' n )
+lemma11 n = lemma06 (S zero) (λ z -> λ w -> mul (S w) z ) n
+
+lemma06' : { U : Set } -> ( u : U ) -> ( v : U -> Int -> U ) ->( t :  Int ) -> ( (R u v t) ≡  (R' u v t ))
+lemma06' u v zero = refl
+lemma06' u v (S t) = let open ≡-Reasoning in 
+   begin 
+       R u v (S t)
+   ≡⟨⟩
+       v (R u v t) t
+   ≡⟨ cong (\x -> v x t ) ( lemma06' u v t )  ⟩
+       v (R' u v t) t
+   ≡⟨ cong (\x -> v (R' u v t) x ) ( sym ( lemma07 u v t )) ⟩
+       v (R' u v t) (π2 (It < u , zero > (λ x → < v (π1 x) (π2 x) , S (π2 x) >) t))
+   ≡⟨⟩
+       R' u v (S t)
+   ∎
+
+
+
+
+