Mercurial > hg > Members > kono > Proof > category

changeset 254:45b81fcb8a64

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
equalizer fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 14 Sep 2013 10:04:18 +0900
parents 24e83b8b81be
children 7e7b2c38dee1
files equalizer.agda free-monoid.agda
diffstat 2 files changed, 55 insertions(+), 54 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Wed Sep 11 20:26:48 2013 +0900
+++ b/equalizer.agda	Sat Sep 14 10:04:18 2013 +0900
@@ -96,17 +96,16 @@
 equalizer+iso : {a b c c' : Obj A } {f g : Hom A a b } {e : Hom A c a } 
                 (h-1 : Hom A c' c ) → (h : Hom A c c' ) →
                 A [ A [ h o h-1 ]  ≈ id1 A c' ] → A [ A [ h-1  o h ]  ≈ id1 A c ] →
-                 ( fe=ge' : A [ A [ f o A [ e o h-1 ] ] ≈ A [ g o A [  e  o h-1 ] ] ] )
                 ( eqa : Equalizer A e f g ) 
            → Equalizer A (A [ e  o h-1  ] ) f g
-equalizer+iso  {a} {b} {c} {c'} {f} {g} {e} h-1 h  hh-1=1 h-1h=1  fe=ge' eqa =  record {
+equalizer+iso  {a} {b} {c} {c'} {f} {g} {e} h-1 h  hh-1=1 h-1h=1  eqa =  record {
       fe=ge = fe=ge1 ;
       k = λ j eq → A [ h o k eqa j eq ] ;
       ek=h = ek=h1 ;
       uniqueness = uniqueness1
   } where
       fe=ge1 :  A [ A [ f o  A [ e  o h-1  ]  ]  ≈ A [ g o  A [ e  o h-1  ]  ] ]
-      fe=ge1 = fe=ge'
+      fe=ge1 = f1=gh ( fe=ge eqa )
       ek=h1 :   {d : Obj A} {j : Hom A d a} {eq : A [ A [ f o j ] ≈ A [ g o j ] ]} →
                 A [ A [  A [ e  o h-1  ]  o A [ h o k eqa j eq ] ] ≈ j ]
       ek=h1 {d} {j} {eq} =  let open ≈-Reasoning (A) in
@@ -249,7 +248,8 @@
                    ∎ )⟩
                      k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) )
               ∎ )⟩
-                 equalizer keqa'  o k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) ) ≈⟨ ek=h keqa' ⟩
+                 equalizer keqa'  o k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) ) 
+              ≈⟨ ek=h keqa' ⟩
                  id c
               ∎
 
@@ -258,7 +258,7 @@
 --------------------------------
 ----
 --
--- An equalizer satisfies Burroni equations
+-- Existence of equalizer satisfies Burroni equations
 --
 ----
 
@@ -351,9 +351,10 @@
 
      lemma-b4 : {d : Obj A} {j : Hom A d c} → A [
               A [ k (eqa f g) (A [ A [ equalizer (eqa f g) o j ] o 
-                 equalizer (eqa (A [ f o A [ equalizer (eqa f g {e}) o j ] ]) (A [ g o A [ equalizer (eqa f g {e} ) o j ] ])) ])
-                     (lemma-equ4 {a} {b} {c} f g (A [ equalizer (eqa f g) o j ])) o
-              k (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ f o A [ equalizer (eqa f g) o j ] ])) (id1 A d) (f1=f1 (A [ f o A [ equalizer (eqa f g) o j ] ])) ]
+                              equalizer (eqa (A [ f o A [ equalizer (eqa f g {e}) o j ] ]) (A [ g o A [ equalizer (eqa f g {e} ) o j ] ])) ])
+                     (lemma-equ4 {a} {b} {c} f g (A [ equalizer (eqa f g) o j ])) 
+                 o k (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ f o A [ equalizer (eqa f g) o j ] ])) 
+                     (id1 A d) (f1=f1 (A [ f o A [ equalizer (eqa f g) o j ] ])) ]
               ≈ j ]
      lemma-b4 {d} {j} = let open ≈-Reasoning (A) in
              begin
--- a/free-monoid.agda	Wed Sep 11 20:26:48 2013 +0900
+++ b/free-monoid.agda	Sat Sep 14 10:04:18 2013 +0900
@@ -20,30 +20,30 @@
 infixr 40 _::_
 data  List  (A : Set c ) : Set c where
    [] : List A
-   _::_ : A -> List A -> List A
+   _::_ : A → List A → List A
 
 
 infixl 30 _++_
-_++_ :   {A : Set c } -> List A -> List A -> List A
+_++_ :   {A : Set c } → List A → List A → List A
 []        ++ ys = ys
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
 ≡-cong = Relation.Binary.PropositionalEquality.cong 
 
-list-id-l : { A : Set c } -> { x : List A } ->  [] ++ x ≡ x
+list-id-l : { A : Set c } → { x : List A } →  [] ++ x ≡ x
 list-id-l {_} {_} = refl
-list-id-r : { A : Set c } -> { x : List A } ->  x ++ [] ≡ x
+list-id-r : { A : Set c } → { x : List A } →  x ++ [] ≡ x
 list-id-r {_} {[]} =   refl
-list-id-r {A} {x :: xs} =  ≡-cong ( \y -> x :: y ) ( list-id-r {A} {xs} ) 
-list-assoc : {A : Set c} -> { xs ys zs : List A } ->
+list-id-r {A} {x :: xs} =  ≡-cong ( λ y → x :: y ) ( list-id-r {A} {xs} ) 
+list-assoc : {A : Set c} → { xs ys zs : List A } →
       ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs )
 list-assoc  {_} {[]} {_} {_} = refl
-list-assoc  {A} {x :: xs}  {ys} {zs} = ≡-cong  ( \y  -> x :: y ) 
+list-assoc  {A} {x :: xs}  {ys} {zs} = ≡-cong  ( λ y  → x :: y ) 
          ( list-assoc {A} {xs} {ys} {zs} )
-list-o-resp-≈ :  {A : Set c} ->  {f g : List A } → {h i : List A } → 
+list-o-resp-≈ :  {A : Set c} →  {f g : List A } → {h i : List A } → 
                   f ≡  g → h ≡  i → (h ++ f) ≡  (i ++ g)
 list-o-resp-≈  {A} refl refl = refl
-list-isEquivalence : {A : Set c} -> IsEquivalence {_} {_} {List A }  _≡_ 
+list-isEquivalence : {A : Set c} → IsEquivalence {_} {_} {List A }  _≡_ 
 list-isEquivalence {A} =      -- this is the same function as A's equivalence but has different types
    record { refl  = refl
      ; sym   = sym
@@ -67,15 +67,15 @@
 
 record Monomorph ( a b : ≡-Monoid )  : Set (suc c) where
   field
-      morph : Carrier a -> Carrier b  
+      morph : Carrier a → Carrier b  
       identity     :  morph (ε a)  ≡  ε b
-      homo :  ∀{x y} -> morph ( _∙_ a x  y ) ≡ ( _∙_ b (morph  x ) (morph  y) )
+      homo :  ∀{x y} → morph ( _∙_ a x  y ) ≡ ( _∙_ b (morph  x ) (morph  y) )
 
 open Monomorph
 
-_+_ : { a b c : ≡-Monoid } -> Monomorph b c -> Monomorph a b -> Monomorph a c
+_+_ : { a b c : ≡-Monoid } → Monomorph b c → Monomorph a b → Monomorph a c
 _+_ {a} {b} {c} f g =  record {
-      morph = \x ->  morph  f ( morph g x ) ;
+      morph = λ x →  morph  f ( morph g x ) ;
       identity  = identity1 ;
       homo  = homo1 
    } where
@@ -83,16 +83,16 @@
       -- morph f (ε b) = ε c ,  morph g (ε a) ) ≡  ε b
       -- morph f  morph g (ε a) ) ≡  morph f (ε b) = ε c
       identity1 = trans ( ≡-cong (morph f ) ( identity g ) )  ( identity f )
-      homo1 :  ∀{x y} -> morph f ( morph g ( _∙_ a x  y )) ≡ ( _∙_ c (morph f (morph  g x )) (morph f (morph  g y) ) )
-      --  ∀{x y} -> morph f ( morph g ( _∙_ a x  y )) ≡ morph f ( ( _∙_ c  (morph  g x )) (morph  g y) ) 
-      --  ∀{x y} -> morph f ( ( _∙_ c  (morph  g x )) (morph  g y) )  
+      homo1 :  ∀{x y} → morph f ( morph g ( _∙_ a x  y )) ≡ ( _∙_ c (morph f (morph  g x )) (morph f (morph  g y) ) )
+      --  ∀{x y} → morph f ( morph g ( _∙_ a x  y )) ≡ morph f ( ( _∙_ c  (morph  g x )) (morph  g y) ) 
+      --  ∀{x y} → morph f ( ( _∙_ c  (morph  g x )) (morph  g y) )  
       --         ≡ ( _∙_ c (morph f (morph  g x )) (morph f (morph  g y) ) )
       homo1 = trans  (≡-cong (morph f ) ( homo g) ) ( homo f ) 
 
-M-id : { a : ≡-Monoid } -> Monomorph a a 
-M-id = record { morph = \x -> x  ; identity = refl ; homo = refl }
+M-id : { a : ≡-Monoid } → Monomorph a a 
+M-id = record { morph = λ x → x  ; identity = refl ; homo = refl }
 
-_==_ : { a b : ≡-Monoid } -> Monomorph a b -> Monomorph a b -> Set c 
+_==_ : { a b : ≡-Monoid } → Monomorph a b → Monomorph a b → Set c 
 _==_  f g =  morph f ≡ morph g
 
 isMonoids : IsCategory ≡-Monoid Monomorph _==_  _+_  (M-id)
@@ -100,13 +100,13 @@
                     ; identityL =  refl
                     ; identityR =  refl
                     ; associative = refl
-                    ; o-resp-≈ =    \{a} {b} {c} {f} {g} {h} {i} -> o-resp-≈ {a} {b} {c} {f} {g} {h} {i}
+                    ; o-resp-≈ =    λ {a} {b} {c} {f} {g} {h} {i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i}
                     }
      where
         o-resp-≈ :  {a b c :  ≡-Monoid } {f g : Monomorph a b } → {h i : Monomorph b c } → 
                           f ==  g → h ==  i → (h + f) ==  (i + g)
         o-resp-≈  {A} refl refl = refl
-        isEquivalence1 : { a b : ≡-Monoid } -> IsEquivalence {_} {_} {Monomorph a b}  _==_ 
+        isEquivalence1 : { a b : ≡-Monoid } → IsEquivalence {_} {_} {Monomorph a b}  _==_ 
         isEquivalence1  =      -- this is the same function as A's equivalence but has different types
            record { refl  = refl
              ; sym   = sym
@@ -129,32 +129,32 @@
 
 U : Functor B A
 U = record {
-       FObj = \m -> Carrier m ;
-       FMap = \f -> morph f ;
+       FObj = λ m → Carrier m ;
+       FMap = λ f → morph f ;
        isFunctor = record {
-              ≈-cong   = \x -> x
+              ≈-cong   = λ x → x
              ; identity = refl
              ; distr    = refl
        }
    } 
 
 -- FObj 
-list  : (a : Set c) -> ≡-Monoid
+list  : (a : Set c) → ≡-Monoid
 list a = record {
     Carrier    =  List a
     ; _∙_      = _++_
     ; ε        = []
     ; isMonoid = record {
-          identity = ( ( \x -> list-id-l {a}  ) , ( \x -> list-id-r {a} ) ) ;
+          identity = ( ( λ x → list-id-l {a}  ) , ( λ x → list-id-r {a} ) ) ;
           isSemigroup = record {
-               assoc =  \x -> \y -> \z -> sym ( list-assoc {a} {x} {y} {z} )
+               assoc =  λ x → λ y → λ z → sym ( list-assoc {a} {x} {y} {z} )
              ; isEquivalence = list-isEquivalence
-             ; ∙-cong = \x -> \y ->  list-o-resp-≈ y x
+             ; ∙-cong = λ x → λ y →  list-o-resp-≈ y x
           }
       }
     }
 
-Generator : Obj A -> Obj B
+Generator : Obj A → Obj B
 Generator s =  list s
 
 -- solution
@@ -162,17 +162,17 @@
 open UniversalMapping
 
 --   [a,b,c] → f(a) ∙ f(b) ∙ f(c)
-Φ :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →  List a -> Carrier b
+Φ :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →  List a → Carrier b
 Φ {a} {b} {f} [] = ε b
 Φ {a} {b} {f} ( x :: xs ) = _∙_ b  ( f x ) (Φ {a} {b} {f} xs )
 
 solution : (a : Obj A ) (b : Obj B) ( f : Hom A a (FObj U b) ) →  Hom B (Generator a ) b 
 solution a b f = record {
-         morph = \(l : List a) -> Φ l   ;
+         morph = λ (l : List a) → Φ l   ;
          identity = refl ;
-         homo = \{x y} -> homo1 x y 
+         homo = λ {x y} → homo1 x y 
     } where
-        _*_ : Carrier b -> Carrier b -> Carrier b
+        _*_ : Carrier b → Carrier b → Carrier b
         _*_  f g = _∙_ b f g
         homo1 : (x y : Carrier (Generator a)) → Φ ((Generator a ∙ x) y) ≡ (b ∙ Φ x) (Φ y)
         homo1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ y))
@@ -194,7 +194,7 @@
              ∎ )
 
 eta :  (a : Obj A) → Hom A a ( FObj U (Generator a) )
-eta  a = \( x : a ) ->  x :: []
+eta  a = λ ( x : a ) →  x :: []
 
 -- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming )
 -- postulate extensionality : { a b : Obj A } {f g : Hom A a b } → (∀ {x} → (f x ≡ g x))  → ( f ≡ g ) 
@@ -203,10 +203,10 @@
 FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta  
 FreeMonoidUniveralMapping = 
     record {
-       _* = \{a b} -> \f -> solution a b f ; 
+       _* = λ {a b} → λ f → solution a b f ; 
        isUniversalMapping = record {
-             universalMapping = \{a b f} -> universalMapping {a} {b} {f} ; 
-             uniquness = \{a b f g} -> uniquness {a} {b} {f} {g}
+             universalMapping = λ {a b f} → universalMapping {a} {b} {f} ; 
+             uniquness = λ {a b f g} → uniquness {a} {b} {f} {g}
        }
     } where
         universalMapping :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →  FMap U ( solution a b f  ) o eta a   ≡ f
@@ -221,18 +221,18 @@
                          ( λ (x : a ) →  _∙_ b  ( f x ) (Φ {a} {b} {f} [] ) )
                      ≡⟨⟩
                          ( λ (x : a ) →  _∙_ b  ( f x ) ( ε b ) )
-                     ≡⟨ ≡-cong ( \ g -> ( ( λ (x : a ) →  g x ) )) (extensionality {a} lemma-ext1) ⟩
+                     ≡⟨ ≡-cong ( λ  g → ( ( λ (x : a ) →  g x ) )) (extensionality {a} lemma-ext1) ⟩
                          ( λ (x : a ) →  f x  )
                      ≡⟨⟩
                           f
                      ∎  where
-                        lemma-ext1 : ∀( x : a ) ->  _∙_ b  ( f x ) ( ε b )  ≡ f x
+                        lemma-ext1 : ∀( x : a ) →  _∙_ b  ( f x ) ( ε b )  ≡ f x
                         lemma-ext1 x = ( proj₂ ( IsMonoid.identity ( isMonoid b) ) ) (f x)
         uniquness :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →
              { g :  Hom B (Generator a) b } → (FMap U g) o (eta a )  ≡ f  → B [ solution a b f ≈ g ]
         uniquness {a} {b} {f} {g} eq =  
                      extensionality  lemma-ext2 where
-                        lemma-ext2 : ( ∀( x : List a ) -> (morph ( solution a b f)) x  ≡ (morph g) x  )
+                        lemma-ext2 : ( ∀( x : List a ) → (morph ( solution a b f)) x  ≡ (morph g) x  )
                         -- (morph ( solution a b f)) []  ≡ (morph g) []  )
                         lemma-ext2 [] = let open ≡-Reasoning in
                              begin
@@ -247,26 +247,26 @@
                                 (morph ( solution a b f)) ( x :: xs )
                              ≡⟨ homo ( solution a b f) {x :: []} {xs} ⟩
                                  _∙_ b ((morph ( solution a b f)) ( x :: []) )  ((morph ( solution a b f)) xs )
-                             ≡⟨  ≡-cong ( \ k -> (_∙_ b ((morph ( solution a b f)) ( x :: []) ) k )) (lemma-ext2 xs )   ⟩
+                             ≡⟨  ≡-cong ( λ  k → (_∙_ b ((morph ( solution a b f)) ( x :: []) ) k )) (lemma-ext2 xs )   ⟩
                                  _∙_ b ((morph ( solution a b f)) ( x :: []) )  ((morph g) ( xs ))
-                             ≡⟨  ≡-cong ( \k -> ( _∙_ b ( k x ) ((morph g) ( xs )) )) (
+                             ≡⟨  ≡-cong ( λ k → ( _∙_ b ( k x ) ((morph g) ( xs )) )) (
                                  begin
-                                     ( \x -> (morph ( solution a b f)) ( x :: [] ) )
+                                     ( λ x → (morph ( solution a b f)) ( x :: [] ) )
                                  ≡⟨ extensionality {a} lemma-ext3 ⟩
-                                     ( \x -> (morph g) ( x :: [] ) )
+                                     ( λ x → (morph g) ( x :: [] ) )
                                  ∎  
                              ) ⟩
                                  _∙_ b ((morph g) ( x :: [] )) ((morph g) ( xs ))
                              ≡⟨ sym ( homo g ) ⟩
                                 (morph g) ( x :: xs )
                              ∎   where
-                         lemma-ext3 :  ∀( x : a ) -> (morph ( solution a b f)) (x :: [])  ≡ (morph g) ( x :: []  )
+                         lemma-ext3 :  ∀( x : a ) → (morph ( solution a b f)) (x :: [])  ≡ (morph g) ( x :: []  )
                          lemma-ext3 x = let open ≡-Reasoning in
                              begin
                                (morph ( solution a b f)) (x :: [])
                              ≡⟨  ( proj₂  ( IsMonoid.identity ( isMonoid b) )(f x) ) ⟩
                                 f x
-                             ≡⟨  sym ( ≡-cong (\f -> f x )  eq  ) ⟩
+                             ≡⟨  sym ( ≡-cong (λ f → f x )  eq  ) ⟩
                                (morph g) ( x :: []  )
                              ∎