Mercurial > hg > Members > kono > Proof > category

changeset 153:3249aaddc405

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sync
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 17 Aug 2013 21:09:34 +0900
parents 5435469c6cf0
children 744be443e232
files category-ex.agda idF.agda kleisli.agda level-ex.agda list-level.agda list-nat.agda list-nat0.agda monoid-monad.agda record-ex.agda
diffstat 9 files changed, 471 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/category-ex.agda	Sat Aug 17 21:09:34 2013 +0900
@@ -0,0 +1,18 @@
+module category-ex where
+
+open import Level
+open import Category
+postulate c₁ c₂ ℓ : Level
+postulate A : Category c₁ c₂ ℓ
+
+postulate a b c : Obj A
+postulate g : Hom A a b
+postulate f : Hom A b c
+
+open Category.Category
+
+h = _o_  A f g
+
+i = A [ f o g ]
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/idF.agda	Sat Aug 17 21:09:34 2013 +0900
@@ -0,0 +1,55 @@
+module idF where
+
+open import Category
+open import HomReasoning
+
+identityFunctor : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} → Functor C C
+identityFunctor {C = C} = record { 
+       FObj      = λ x → x
+     ; FMap      = λ x → x
+     ; isFunctor = isFunctor
+     }
+  where
+        isFunctor : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} → IsFunctor C C (λ x → x) (λ x → x)
+        isFunctor {C = C} =
+          record { ≈-cong   = Lemma1
+                 ; identity = Lemma2
+                 ; distr    = Lemma3
+                 } where
+           FMap : {a b : Obj C} -> Hom C a b -> Hom C a b
+           FMap = λ x → x
+           FObj : Obj C -> Obj C
+           FObj = λ x → x
+           Lemma1 : {A B : Obj C} {f g : Hom C A B} → C [ f ≈ g ] → C [ FMap f ≈ FMap g ]
+           Lemma1 {a} {b} {f} {g}  f≈g = let open ≈-Reasoning C in
+             begin
+                 FMap f 
+             ≈⟨⟩ 
+                 f
+             ≈⟨ f≈g  ⟩ 
+                 g
+             ≈⟨⟩ 
+                 FMap g 
+             ∎ 
+           Lemma2 : {A : Obj C} →  C [ (FMap {A} {A} (Id {_} {_} {_} {C} A)) ≈ (Id {_} {_} {_} {C} (FObj A)) ]
+           Lemma2 {A} = let open ≈-Reasoning C in
+             begin
+                   (FMap {A} {A} (Id {_} {_} {_} {C} A))
+             ≈⟨⟩ 
+                   (Id {_} {_} {_} {C} (FObj A))
+             ∎ 
+           Lemma3 : {a b c : Obj C} {f : Hom C a b} {g : Hom C b c}
+              → C [ FMap (C [ g o f ]) ≈ (C [ FMap g o FMap f ] )]
+           Lemma3 {a} {b} {c} {f} {g}  = let open ≈-Reasoning C in
+             begin
+                FMap ( g o f ) 
+             ≈⟨⟩ 
+                g o f 
+             ≈⟨⟩ 
+                FMap g o FMap f 
+             ∎ 
+
+
+
+
+
--- a/kleisli.agda	Sat Aug 17 21:08:33 2013 +0900
+++ b/kleisli.agda	Sat Aug 17 21:09:34 2013 +0900
@@ -1,5 +1,5 @@
 -- -- -- -- -- -- -- -- 
---  Monad to Kleisli Category
+--  Monad to Kelisli Category
 --  defines U_T and F_T as a resolution of Monad
 --  checks Adjointness
 -- 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/level-ex.agda	Sat Aug 17 21:09:34 2013 +0900
@@ -0,0 +1,18 @@
+module level-ex where
+
+open import Level
+
+postulate ℓ : Level
+
+postulate A : Set ℓ
+
+postulate a : A
+
+lemma1 : Set  ℓ -> A
+lemma1  = \x -> a
+
+lemma2 : A -> Set  ℓ
+lemma2 = \x -> A
+
+lemma3 : Set  (suc ℓ)
+lemma3 = A -> Set  ℓ
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/list-level.agda	Sat Aug 17 21:09:34 2013 +0900
@@ -0,0 +1,165 @@
+module list-level where
+                                                                        
+open import Level
+
+
+postulate A : Set
+postulate B : Set
+postulate C : Set
+
+postulate a : A
+postulate b : A
+postulate c : A
+
+
+infixr 40 _::_
+data  List {a} (A : Set a) : Set a where
+   [] : List A
+   _::_ : A -> List A -> List A
+
+
+infixl 30 _++_
+_++_ : ∀ {a} {A : Set a} -> List A -> List A -> List A
+[]        ++ ys = ys
+(x :: xs) ++ ys = x :: (xs ++ ys)
+
+l1 = a :: []
+l2 = a :: b :: a :: c ::  []
+
+l3 = l1 ++ l2
+
+L1 = A :: []
+L2 = A :: B :: A :: C ::  []
+
+L3 = L1 ++ L2
+
+data Node {a} ( A : Set a ) : Set a where
+   leaf  : A -> Node A
+   node  : Node A -> Node A -> Node A
+
+flatten : ∀{n} { A : Set n } -> Node A -> List A
+flatten ( leaf a )   = a :: []
+flatten ( node a b ) = flatten a ++ flatten b
+
+n1 = node ( leaf a ) ( node ( leaf b ) ( leaf c ))
+
+open  import  Relation.Binary.PropositionalEquality
+
+infixr 20  _==_
+
+data _==_ {n} {A : Set n} :  List A -> List A -> Set n where
+      reflection  : {x : List A} -> x == x
+
+cong1 : ∀{a} {A : Set a } {b} { B : Set b } ->
+   ( f : List A -> List B ) -> {x : List A } -> {y : List A} -> x == y -> f x == f y
+cong1 f reflection = reflection
+
+eq-cons :  ∀{n} {A : Set n} {x y : List A} ( a : A ) -> x ==  y -> ( a :: x ) == ( a :: y )
+eq-cons a z = cong1 ( \x -> ( a :: x) ) z
+
+trans-list :  ∀{n} {A : Set n} {x y z : List A}  -> x ==  y -> y == z -> x == z
+trans-list reflection reflection = reflection
+
+
+==-to-≡ :  ∀{n} {A : Set n}  {x y : List A}  -> x ==  y -> x ≡ y
+==-to-≡ reflection = refl
+
+list-id-l : { A : Set } -> { x : List A} ->  [] ++ x == x
+list-id-l = reflection
+
+list-id-r : { A : Set } -> ( x : List A ) ->  x ++ [] == x
+list-id-r [] =   reflection
+list-id-r (x :: xs) =  eq-cons x ( list-id-r xs )
+
+list-assoc : {A : Set } -> ( xs ys zs : List A ) ->
+     ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
+list-assoc  [] ys zs = reflection
+list-assoc  (x :: xs)  ys zs = eq-cons x ( list-assoc xs ys zs )
+
+
+module ==-Reasoning {n} (A : Set n ) where
+
+  infixr  2 _∎
+  infixr 2 _==⟨_⟩_ _==⟨⟩_
+  infix  1 begin_
+
+
+  data _IsRelatedTo_ (x y : List A) :
+                     Set n where
+    relTo : (x≈y : x  == y  ) → x IsRelatedTo y
+
+  begin_ : {x : List A } {y : List A} →
+           x IsRelatedTo y →  x ==  y 
+  begin relTo x≈y = x≈y
+
+  _==⟨_⟩_ : (x : List A ) {y z : List A} →
+            x == y  → y IsRelatedTo z → x IsRelatedTo z
+  _ ==⟨ x≈y ⟩ relTo y≈z = relTo (trans-list x≈y y≈z)
+
+  _==⟨⟩_ : (x : List A ) {y : List A} 
+            → x IsRelatedTo y → x IsRelatedTo y
+  _ ==⟨⟩ x≈y = x≈y
+
+  _∎ : (x : List A ) → x IsRelatedTo x
+  _∎ _ = relTo reflection
+
+lemma11 : ∀{n} (A : Set n) ( x : List A ) -> x == x
+lemma11 A x =  let open ==-Reasoning A in
+     begin x ∎
+      
+++-assoc : ∀{n} (L : Set n) ( xs ys zs : List L ) -> (xs ++ ys) ++ zs  == xs ++ (ys ++ zs)
+++-assoc A [] ys zs = let open ==-Reasoning A in
+  begin -- to prove ([] ++ ys) ++ zs  == [] ++ (ys ++ zs)
+   ( [] ++ ys ) ++ zs
+  ==⟨ reflection ⟩
+    ys ++ zs
+  ==⟨ reflection ⟩
+    [] ++ ( ys ++ zs )
+  ∎
+  
+++-assoc A (x :: xs) ys zs = let open  ==-Reasoning A in
+  begin -- to prove ((x :: xs) ++ ys) ++ zs == (x :: xs) ++ (ys ++ zs)
+    ((x :: xs) ++ ys) ++ zs
+  ==⟨ reflection ⟩
+     (x :: (xs ++ ys)) ++ zs
+  ==⟨ reflection ⟩
+    x :: ((xs ++ ys) ++ zs)
+  ==⟨ cong1 (_::_ x) (++-assoc A xs ys zs) ⟩ 
+    x :: (xs ++ (ys ++ zs))
+  ==⟨ reflection ⟩
+    (x :: xs) ++ (ys ++ zs)
+  ∎
+
+
+
+--data Bool : Set where
+--      true  : Bool
+--      false : Bool
+
+
+--postulate Obj : Set
+
+--postulate Hom : Obj -> Obj -> Set
+
+
+--postulate  id : { a : Obj } -> Hom a a
+
+
+--infixr 80 _○_
+--postulate  _○_ : { a b c  : Obj } -> Hom b c -> Hom a b -> Hom a c
+
+-- postulate  axId1 : {a  b : Obj} -> ( f : Hom a b ) -> f == id ○ f
+-- postulate  axId2 : {a  b : Obj} -> ( f : Hom a b ) -> f == f ○ id
+
+--assoc : { a b c d : Obj } ->
+--    (f : Hom c d ) -> (g : Hom b c) -> (h : Hom a b) ->
+--    (f ○ g) ○ h == f ○ ( g ○ h)
+
+
+--a = Set
+
+-- ListObj : {A : Set} -> List A
+-- ListObj =  List Set
+
+-- ListHom : ListObj -> ListObj -> Set
+
--- a/list-nat.agda	Sat Aug 17 21:08:33 2013 +0900
+++ b/list-nat.agda	Sat Aug 17 21:09:34 2013 +0900
@@ -4,13 +4,11 @@
 
 
 postulate A : Set
-postulate B : Set
-postulate C : Set
 
 postulate a : A
 postulate b : A
 postulate c : A
-postulate d : B
+
 
 infixr 40 _::_
 data  List  (A : Set ) : Set  where
@@ -24,7 +22,6 @@
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
 l1 = a :: []
--- l1' = A :: []
 l2 = a :: b :: a :: c ::  []
 
 l3 = l1 ++ l2
@@ -127,3 +124,35 @@
   ∎
 
 
+
+--data Bool : Set where
+--      true  : Bool
+--      false : Bool
+
+
+--postulate Obj : Set
+
+--postulate Hom : Obj -> Obj -> Set
+
+
+--postulate  id : { a : Obj } -> Hom a a
+
+
+--infixr 80 _○_
+--postulate  _○_ : { a b c  : Obj } -> Hom b c -> Hom a b -> Hom a c
+
+-- postulate  axId1 : {a  b : Obj} -> ( f : Hom a b ) -> f == id ○ f
+-- postulate  axId2 : {a  b : Obj} -> ( f : Hom a b ) -> f == f ○ id
+
+--assoc : { a b c d : Obj } ->
+--    (f : Hom c d ) -> (g : Hom b c) -> (h : Hom a b) ->
+--    (f ○ g) ○ h == f ○ ( g ○ h)
+
+
+--a = Set
+
+-- ListObj : {A : Set} -> List A
+-- ListObj =  List Set
+
+-- ListHom : ListObj -> ListObj -> Set
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/list-nat0.agda	Sat Aug 17 21:09:34 2013 +0900
@@ -0,0 +1,126 @@
+module list-nat0 where
+                                                                        
+open import Level
+
+
+postulate a : Set
+postulate b : Set
+postulate c : Set
+
+
+infixr 40 _::_
+data  List ∀ {a} (A : Set a) : Set a where
+   [] : List A
+   _::_ : A -> List A -> List A
+
+
+infixl 30 _++_
+-- _++_ : {a : Level } -> {A : Set a} -> List A -> List A -> List A
+_++_ : ∀ {a} {A : Set a} -> List A -> List A -> List A
+[]        ++ ys = ys
+(x :: xs) ++ ys = x :: (xs ++ ys)
+
+
+l1 = a :: []
+l2 = a :: b :: a :: c ::  []
+
+l3 = l1 ++ l2
+
+infixr 20  _==_
+
+data _==_ {n} {A : Set n} :  List A -> List A -> Set n where
+      reflection  : {x : List A} -> x == x
+      eq-cons : {x y : List A} { a : A } -> x ==  y -> ( a :: x ) == ( a :: y )
+      trans-list : {x y z : List A} { a : A } -> x ==  y -> y == z -> x == z
+--      eq-nil  : [] == []
+
+list-id-l : { A : Set } -> { x : List A} ->  [] ++ x == x
+list-id-l = reflection
+
+list-id-r : { A : Set } -> ( x : List A ) ->  x ++ [] == x
+list-id-r [] =   reflection
+list-id-r (x :: xs) =  eq-cons ( list-id-r xs )
+
+
+-- listAssoc : { A : Set } -> { a b c : List A} ->  ( ( a ++ b ) ++ c ) == ( a ++ ( b ++ c ) )
+-- listAssoc   = eq-reflection
+
+list-assoc : {A : Set } -> ( xs ys zs : List A ) ->
+     ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
+list-assoc  [] ys zs = reflection
+list-assoc  (x :: xs)  ys zs = eq-cons ( list-assoc xs ys zs )
+
+
+
+open  import  Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+
+cong1 : ∀{a} {A : Set a } {b} { B : Set b } ->
+   ( f : A -> B ) -> {x : A } -> {y : A} -> x ≡ y -> f x ≡ f y
+cong1 f refl = refl
+
+lemma11 :  ∀{n} ->  ( Set n ) IsRelatedTo ( Set n )
+lemma11  = relTo refl
+
+lemma12 : {L : Set}  ( x : List L ) -> x ++ x ≡ x ++ x
+lemma12 x =  begin  x ++ x  ∎
+
+
+++-assoc : {L : Set} ( xs ys zs : List L ) -> (xs ++ ys) ++ zs  ≡ xs ++ (ys ++ zs)
+++-assoc [] ys zs = -- {A : Set} ->  -- let open ==-Reasoning A in
+  begin -- to prove ([] ++ ys) ++ zs  ≡ [] ++ (ys ++ zs)
+   ( [] ++ ys ) ++ zs
+  ≡⟨ refl ⟩
+    ys ++ zs
+  ≡⟨ refl ⟩
+    [] ++ ( ys ++ zs )
+  ∎
+  
+++-assoc (x :: xs) ys zs = -- {A : Set} -> -- let open  ==-Reasoning A in
+  begin -- to prove ((x :: xs) ++ ys) ++ zs ≡ (x :: xs) ++ (ys ++ zs)
+    ((x :: xs) ++ ys) ++ zs
+  ≡⟨ refl ⟩
+     (x :: (xs ++ ys)) ++ zs
+  ≡⟨ refl ⟩
+    x :: ((xs ++ ys) ++ zs)
+  ≡⟨ cong1 (_::_ x) (++-assoc xs ys zs) ⟩ 
+    x :: (xs ++ (ys ++ zs))
+  ≡⟨ refl ⟩
+    (x :: xs) ++ (ys ++ zs)
+  ∎
+
+
+
+
+
+--data Bool : Set where
+--      true  : Bool
+--      false : Bool
+
+
+--postulate Obj : Set
+
+--postulate Hom : Obj -> Obj -> Set
+
+
+--postulate  id : { a : Obj } -> Hom a a
+
+
+--infixr 80 _○_
+--postulate  _○_ : { a b c  : Obj } -> Hom b c -> Hom a b -> Hom a c
+
+-- postulate  axId1 : {a  b : Obj} -> ( f : Hom a b ) -> f == id ○ f
+-- postulate  axId2 : {a  b : Obj} -> ( f : Hom a b ) -> f == f ○ id
+
+--assoc : { a b c d : Obj } ->
+--    (f : Hom c d ) -> (g : Hom b c) -> (h : Hom a b) ->
+--    (f ○ g) ○ h == f ○ ( g ○ h)
+
+
+--a = Set
+
+-- ListObj : {A : Set} -> List A
+-- ListObj =  List Set
+
+-- ListHom : ListObj -> ListObj -> Set
+
--- a/monoid-monad.agda	Sat Aug 17 21:08:33 2013 +0900
+++ b/monoid-monad.agda	Sat Aug 17 21:09:34 2013 +0900
@@ -175,7 +175,7 @@
 postulate f :  b -> c'
 postulate g :  a -> b
 
-LemmaMM12 =  Monad.join MonoidMonad (F m f) (F m' g)
+Lemma-MM12 =  Monad.join MonoidMonad (F m f) (F m' g)
 
 open import kleisli {_} {_} {_} {A} {T} {η} {μ} {MonoidMonad}
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/record-ex.agda	Sat Aug 17 21:09:34 2013 +0900
@@ -0,0 +1,54 @@
+module record-ex where
+
+data _∨_  (A B : Set) : Set where
+      or1 : A -> A ∨ B
+      or2 : B -> A ∨ B
+
+postulate A B C : Set
+postulate a1 a2 a3 : A
+postulate b1 b2 b3 : B
+
+x : ( A ∨ B )
+x = or1 a1
+y : ( A ∨ B )
+y = or2 b1
+
+f : ( A ∨ B ) -> A
+f (or1 a) = a
+f (or2 b) = a1
+
+record _∧_ (A B : Set) : Set where
+       field
+          and1 : A
+          and2 : B
+
+z : A ∧ B
+z = record { and1 = a1 ; and2 = b2 }
+
+xa : A
+xa = _∧_.and1 z
+xb : B
+xb = _∧_.and2 z
+
+open _∧_
+
+ya : A
+ya = and1 z
+
+open  import  Relation.Binary.PropositionalEquality
+
+data Nat : Set where
+   zero : Nat
+   suc  : Nat -> Nat
+
+record Mod3 (m : Nat) : Set where
+   field
+      mod3 : (suc (suc (suc m ))) ≡ m
+   n : Nat
+   n = m
+
+open Mod3 
+
+Lemma1 :  ( x : Mod3 ( suc (suc (suc (suc zero))))) ( y : Mod3 ( suc zero ) ) -> n x  ≡ n y 
+Lemma1 x y =  mod3 y
+