# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1556071781 -32400
# Node ID aa4fbd00724786fbf131f1dfc6645fcfd8f43c05
# Parent  bca72fffdc1a8f9cf245d0b80f0c7f63e76ef883
using setoid

diff -r bca72fffdc1a -r aa4fbd007247 CCChom.agda
--- a/CCChom.agda	Tue Apr 23 16:34:38 2019 +0900
+++ b/CCChom.agda	Wed Apr 24 11:09:41 2019 +0900
@@ -607,73 +607,12 @@
       ε : {a b : Objs } → arrow ((a <= b) ∧ b ) a
       _* : {a b c : Objs } → arrow (c ∧ b ) a → arrow c ( a <= b )
 
-   data Arrow { obj : Set } { hom : obj → obj → Set } : ( a b : obj ) → Set where
-     id : ( a : obj ) → Arrow a a
-     mono : { a b : obj } → hom a b → Arrow a b
-     connected : {a b : obj } → {c : obj} → hom b c →  Arrow {obj} {hom} a b → Arrow a c
- 
-   _+_ : { obj : Set } { hom : obj → obj → Set } {a b c : obj   } (f : (Arrow {obj} {hom} b c )) → (g : (Arrow {obj} {hom} a b )) → Arrow {obj} {hom} a c
-   id a + id .a = id a
-   id b + mono x = mono x
-   id a + connected x y = connected x y
-   mono x + id a = mono x
-   mono x + mono y = connected x (mono y)
-   mono x + connected y z = connected x ( connected y z )
-   connected x y + z = connected x ( y + z )
- 
-   data _==_ : {a b  : Objs } → (f g : Arrow {Objs} {arrow} a b ) → Set where
-      rrefl  : {a b : Objs } → {f : Arrow {Objs} {arrow} a b } →  f == f
-      irefl  : {a : Objs } → ( id a ) == ( id a )
-      mrefl  : {a b : Objs } {x : arrow a b } → ( mono x ) == ( mono x )
-      trefl  : {a : Objs } { x y : Arrow a ⊤ } → x == y
-      crefl  : {a b c : Objs } { x : arrow b c } → {f g : Arrow a b } → f == g → ( connected x f ) == ( connected x g )
-
-   ==sym : {a b  : Objs } → {f g : Arrow {Objs} {arrow} a b } → f == g  → g == f
-   ==sym rrefl = rrefl
-   ==sym irefl = irefl
-   ==sym mrefl = mrefl
-   ==sym trefl = trefl
-   ==sym (crefl x) = crefl ( ==sym x )
 
-   ==trans : {a b : Objs } → {f g h : Arrow {Objs} {arrow} a b } → f == g → g == h  → f == h
-   ==trans rrefl rrefl = rrefl
-   ==trans rrefl irefl = rrefl
-   ==trans rrefl mrefl = rrefl
-   ==trans rrefl trefl = trefl
-   ==trans rrefl (crefl y) = crefl y
-   ==trans irefl rrefl = rrefl
-   ==trans irefl irefl = rrefl
-   ==trans irefl trefl = trefl
-   ==trans mrefl rrefl = rrefl
-   ==trans mrefl mrefl = rrefl
-   ==trans mrefl trefl = trefl
-   ==trans trefl rrefl = trefl
-   ==trans trefl mrefl = trefl
-   ==trans trefl trefl = trefl
-   ==trans (crefl x) rrefl = (crefl x)
-   ==trans (crefl x) trefl = trefl
-   ==trans (crefl x) (crefl y) = crefl ( ==trans x y )
-   ==trans trefl irefl = trefl
-   ==trans trefl (crefl y) = trefl
+   open import discrete
+   open graphtocat
 
-   assoc-+ : {a b c d : Objs   }
-        (f : (Arrow  {Objs} {arrow} c d )) → (g : (Arrow {Objs} {arrow} b c )) → (h : (Arrow {Objs} {arrow} a b )) →
-        ( f + (g + h)) ==  ((f + g) + h )
-   assoc-+ (id a) (id .a) (id .a) = irefl
-   assoc-+ (id a) (id .a) (mono x) = mrefl
-   assoc-+ (id a) (id .a) (connected h h₁) = crefl rrefl 
-   assoc-+ (id a) (mono x) (id a₁) = mrefl
-   assoc-+ (id a) (mono x) (mono x₁) = crefl mrefl
-   assoc-+ (id a) (mono x) (connected h h₁) = crefl rrefl
-   assoc-+ (id a) (connected g h) _ = crefl rrefl
-   assoc-+ (mono x) (id a) (id .a) = mrefl
-   assoc-+ (mono x) (id a) (mono x₁) = crefl mrefl
-   assoc-+ (mono x) (id a) (connected h h₁) = crefl rrefl
-   assoc-+ (mono x) (mono x₁) (id a) = crefl mrefl
-   assoc-+ (mono x) (mono x₁) (mono x₂) = crefl ( crefl mrefl )
-   assoc-+ (mono x) (mono x₁) (connected h h₁) = crefl ( crefl rrefl )
-   assoc-+ (mono x) (connected g g₁) _ = crefl rrefl
-   assoc-+ (connected f g) (x) (y) = crefl ( assoc-+ g x y ) 
+   GC :   Category  Level.zero Level.zero Level.zero   
+   GC = GraphtoCat Objs arrow
 
    product : {a b c : Objs } → Arrow c a → Arrow c b → Arrow {Objs} {arrow} c ( a ∧ b )
    product {a} {b} {c} y (connected {_} {_} {d} x g) =   connected (< π , x ・ π'  >) ( product y g )
@@ -688,61 +627,74 @@
    star {a} {b} {c} (mono x) = mono ( x * )
    star {a} {b} {c} (connected {_} {d} {_} x y) = connected (  ( x  ・  ε  ) * ) ( star y )
 
+
+   data _==_ : {a b  : Objs } → (f g : Arrow {Objs} {arrow} a b ) → Set  where
+      rrefl  : {a b : Objs } → {f : Arrow {Objs} {arrow} a b } →  f == f
+      trefl : {a b : Objs} → {h i : Arrow {Objs} {arrow} ⊤ b } {f g : Arrow {Objs} {arrow} a ⊤ } → h == i → (h + f) == (i + g)
+
+   ≡→== : {a b  : Objs } → {f g : Arrow {Objs} {arrow} a b } → f ≡ g → f == g
+   ≡→== refl = rrefl
+
+   r== : {a b : Objs } →  { f : Arrow {Objs} {arrow} a b } → f == f
+   r== = ≡→== refl
+
+   s== : {a b : Objs } →  { f g : Arrow {Objs} {arrow} a b } → f == g → g == f
+   s== rrefl = rrefl
+   s== (trefl rrefl) = trefl rrefl
+   s== (trefl (trefl eq)) = trefl {!!}
+
+   t== : {a b : Objs } →  { i j k : Arrow {Objs} {arrow} a b } → i == j → j == k → i == k
+   t== rrefl rrefl = rrefl
+   t== eq eq1 = {!!}
+
+   ctcong : {a b c : Objs } →  { f g : Arrow {Objs} {arrow} a b } → { x : arrow b c } → f == g  → connected x f == connected x g
+   ctcong rrefl = rrefl
+   ctcong (trefl eq) = trefl {!!}
+
+   ccc-e2 : {a : Objs } → ∀ { f : Arrow {Objs} {arrow} a ⊤ } →  f ==  mono (○ a) 
+   ccc-e2 {a} {f} = {!!}
+
+   -- Reflexive : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
+   -- Reflexive _∼_ = ∀ {x} → x ∼ x
+
+   open  import  Relation.Binary.Core
+   open  import  Relation.Binary
+   import Relation.Binary.EqReasoning as EqR
+
+   cccIEQ : {a b : Objs } → Setoid Level.zero Level.zero
+   cccIEQ {a} {b} = record {
+        Carrier   = Arrow {Objs} {arrow} a b 
+      ; _≈_       = _==_
+      ; isEquivalence = record {refl = r== ; trans = t== ; sym = s== }
+    }
+
+
    GraphtoCCC :   Category  Level.zero Level.zero Level.zero   
    GraphtoCCC  = record {
             Obj  = Objs ;
-            Hom = λ a b →   Arrow a b  ;
-            _o_ =  λ{a} {b} {c} x y → _+_  x y ;
-            _≈_ =  λ x y → x  == y ;
+            Hom = λ a b →   Arrow  {Objs} {arrow} a b  ;
+            _o_ =  _+_ ;
+            _≈_ =   _==_  ;
             Id  =  λ{a} → id a ;
             isCategory  = record {
-                    isEquivalence =  record {refl = rrefl ; trans = ==trans ; sym = ==sym } ;
-                    identityL  = λ{a b f} → identityL    {a} {b} {f} ;
-                    identityR  = λ{a b f} → identityR    {a} {b} {f} ;
-                    o-resp-≈  = λ{a b c f g h i} →  o-resp-≈     {a} {b} {c} {f} {g} {h} {i} ;
-                    associative  = λ{a b c d f g h } → assoc-+  f g h
+                    isEquivalence =  record {refl = r== ; trans = t== ; sym = s== }
+                 ;  identityL  = identityL
+                 ;  identityR  = identityR
+                 ;  o-resp-≈  = λ{a b c f g h i} →  {!!}
+                 ;  associative  = λ{a b c d f g h } → {!!}
                }
-           }  where
-                identityL :   {A B : Objs } {f : ( Arrow    A B) } →  ((id B)  + f) ==  f
-                identityL {_} {_} {id a} = irefl
-                identityL {_} {_} {mono x} = mrefl
-                identityL {_} {_} {connected x f} = crefl rrefl
-                identityR :   {A B : Objs } {f : ( Arrow {Objs} {arrow}  A B) } →   ( f + id A )  == f
-                identityR {_} {_} {id a} = irefl
-                identityR {_} {_} {mono x} = mrefl
-                identityR {_} {_} {connected x f} = crefl ( identityR )
-                o-resp-≈ :   {A B C : Objs   } {f g :  ( Arrow    A B)} {h i : ( Arrow B C)} →
-                    f  == g → h  == i → ( h + f )  == ( i + g )
-                o-resp-≈ {_} {_} {_} {f} {.f} {h} {.h} rrefl rrefl = rrefl
-                o-resp-≈ {_} {_} {_} {f} {.f} {.(id _)} {.(id _)} rrefl irefl = rrefl
-                o-resp-≈ {_} {_} {_} {f} {.f} {.(mono _)} {.(mono _)} rrefl mrefl = rrefl
-                o-resp-≈ {_} {_} {_} {f} {.f} {h} {i} rrefl trefl = trefl
-                o-resp-≈ {_} {_} {_} {f} {.f} {.(connected _ _)} {.(connected _ _)} rrefl (crefl h=i) = crefl ( o-resp-≈ rrefl h=i )
-                o-resp-≈ {_} {_} {_} {.(id _)} {.(id _)} {h} {.h} irefl rrefl = rrefl
-                o-resp-≈ {_} {_} {_} {.(id _)} {.(id _)} {.(id _)} {.(id _)} irefl irefl = rrefl
-                o-resp-≈ {_} {_} {_} {.(id _)} {.(id _)} {.(mono _)} {.(mono _)} irefl mrefl = rrefl
-                o-resp-≈ {_} {_} {_} {.(id _)} {.(id _)} {h} {i} irefl trefl = trefl
-                o-resp-≈ {_} {_} {_} {.(id _)} {.(id _)} {.(connected _ _)} {.(connected _ _)} irefl (crefl h=i) = crefl ( o-resp-≈ rrefl h=i )
-                o-resp-≈ {_} {_} {_} {.(mono _)} {.(mono _)} {h} {.h} mrefl rrefl = rrefl
-                o-resp-≈ {_} {_} {_} {.(mono _)} {.(mono _)} {.(id _)} {.(id _)} mrefl irefl = rrefl
-                o-resp-≈ {_} {_} {_} {.(mono _)} {.(mono _)} {.(mono _)} {.(mono _)} mrefl mrefl = rrefl
-                o-resp-≈ {_} {_} {_} {.(mono _)} {.(mono _)} {h} {i} mrefl trefl = trefl
-                o-resp-≈ {_} {_} {_} {.(mono _)} {.(mono _)} {.(connected _ _)} {.(connected _ _)} mrefl (crefl h=i) = crefl ( o-resp-≈ rrefl h=i )
-                o-resp-≈ {_} {_} {_} {.(connected _ _)} {.(connected _ _)} {id a} {.(id a)} (crefl f=g) rrefl = crefl f=g
-                o-resp-≈ {_} {_} {_} {.(connected _ _)} {.(connected _ _)} {mono x} {.(mono x)} (crefl f=g) rrefl = crefl ( crefl f=g )
-                o-resp-≈ {_} {_} {_} {.(connected _ _)} {.(connected _ _)} {connected x h} {.(connected x h)} (crefl f=g) rrefl =
-                   crefl ( o-resp-≈ (crefl f=g) rrefl )
-                o-resp-≈ {_} {_} {_} {.(connected _ _)} {.(connected _ _)} {.(id _)} {.(id _)} (crefl f=g) irefl = crefl f=g
-                o-resp-≈ {_} {_} {_} {.(connected _ _)} {.(connected _ _)} {.(mono _)} {.(mono _)} (crefl f=g) mrefl = crefl (crefl f=g) 
-                o-resp-≈ {_} {_} {_} {.(connected _ _)} {.(connected _ _)} {h} {i} (crefl f=g) trefl = trefl
-                o-resp-≈ {_} {_} {_} {.(connected _ _)} {.(connected _ _)} {.(connected _ _)} {.(connected _ _)} (crefl f=g) (crefl h=i) = 
-                   crefl ( o-resp-≈ (crefl f=g) h=i  )
-                o-resp-≈ {_} {_} {_} {f} {g} {h} {.h} trefl rrefl = {!!}
-                o-resp-≈ {_} {_} {_} {f} {g} {.(id ⊤)} {.(id ⊤)} trefl irefl = {!!}
-                o-resp-≈ {_} {_} {_} {f} {g} {.(mono _)} {.(mono _)} trefl mrefl = {!!}
-                o-resp-≈ {_} {_} {_} {f} {g} {h} {i} trefl trefl = trefl
-                o-resp-≈ {_} {_} {_} {f} {g} {.(connected _ _)} {.(connected _ _)} trefl (crefl h=i) = {!!}
+           } where
+       identityL : {a b : Objs } →  { f : Arrow {Objs} {arrow} a b } → (id b + f) == f
+       identityL {a} {.a} {id a} = rrefl
+       identityL {a} {b} {mono x} = rrefl
+       identityL {a} {b} {connected x f} = rrefl
+       identityR : {a b : Objs } →  { f : Arrow {Objs} {arrow} a b } → (f + id a ) == f
+       identityR {a} {.a} {id a} = rrefl
+       identityR {a} {b} {mono x} = rrefl
+       identityR {a} {b} {connected x f} = ctcong identityR
 
+--          ≈⟨ {!!} ⟩
+--          ∎ where open EqR cccIEQ -- open IsEquivalence cccIEQ
 
 --      GLCCC : CCC GraphtoCCC 
 --      GLCCC = record {
@@ -758,7 +710,6 @@
 --          ;  isCCC = isc
 --        } where
 --           GC = GraphtoCCC 
---           isc : ? -- IsCCC GC ⊤ (λ f → mono (○ f)) _∧_ ( λ f g → product f g) (mono π) (mono π') _<=_ star (mono ε ) 
 --           e2 : {a : Obj GC } → ∀ { f : Hom GC a ⊤ } →  GC [ f ≈ mono (○ a) ]
 --           e2 {.⊤} {id .⊤} = {!!}
 --           e2 {a} {mono x} = {!!}