Mercurial > hg > Members > kono > Proof > category

changeset 838:be4b8e70fa8e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add category
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Apr 2020 08:43:50 +0900
parents d809e2502be4
children 111ee96c09ab
files CCCGraph1.agda
diffstat 1 files changed, 36 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph1.agda	Thu Apr 02 08:16:17 2020 +0900
+++ b/CCCGraph1.agda	Thu Apr 02 08:43:50 2020 +0900
@@ -4,11 +4,12 @@
 
 open import HomReasoning
 open import cat-utility
-open  import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import CCC
 open import graph
 
 module ccc-from-graph {c₁  c₂  : Level} (G : Graph {c₁} {c₂} )  where
+   open import  Relation.Binary.PropositionalEquality hiding ( [_] )
    open Graph
    
    data Objs : Set (c₁ ⊔ c₂) where
@@ -33,11 +34,43 @@
    _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
    _・_ {a} {b} {⊤} _ _ = iv (○ a) (id a)
    id a ・ g = g
-   < f , g > ・  h = < ( f ・ h ) , ( g ・ h ) >
+   < f , g > ・  h = <  f ・ h  ,  g ・ h  >
    iv f (id _) ・ h = iv f h
    iv π < g , g₁ > ・  h = g ・ h
    iv π' < g , g₁ > ・  h = g₁ ・ h
    iv ε < g , g₁ > ・  h = iv ε < g ・ h , g₁ ・ h >
-   iv (f *) < g , g₁ > ・ h = iv (f *) < g ・ h , g₁ ・ h > -- Arrows b a Arrows a b
+   iv (f *) < g , g₁ > ・ h = iv (f *) < g ・ h , g₁ ・ h > 
    iv f (iv f₁ g) ・ h = iv f (  (iv f₁ g) ・ h )
 
+   PL :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
+   PL = record {
+            Obj  = Objs;
+            Hom = λ a b →  Arrows  a b ;
+            _o_ =  λ{a} {b} {c} x y → x ・ y ;
+            _≈_ =  λ x y → x  ≡ y ;
+            Id  =  λ{a} → id a ;
+            isCategory  = record {
+                    isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
+                    identityL  = identityL; 
+                    identityR  = identityR ; 
+                    o-resp-≈  = o-resp-≈  ; 
+                    associative  = λ{a b c d f g h } → associative  f g h
+               }
+           }  where
+               identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f
+               identityL {_} {_} {id a} = {!!}
+               identityL {a} {b} {< f , f₁ >} = {!!}
+               identityL {_} {_} {iv f f₁} = {!!}
+               identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f
+               identityR {a} {_} {id a} = {!!}
+               identityR {a} {b} {< f , g >} = {!!} -- cong ( λ k → iv x k ) ( identityR {_} {_} {f} )
+               identityR {a} {b} {iv x f} = {!!} -- cong ( λ k → iv x k ) ( identityR {_} {_} {f} )
+               o-resp-≈  : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
+                            f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
+               o-resp-≈  refl refl = refl
+               associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
+                            (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
+               associative (id a) g h = {!!}
+               associative (< f , f1 > ) g h = {!!}
+               associative (iv x f) g h = {!!} -- cong ( λ k → iv x k ) ( associative f g h )
+