Mercurial > hg > Members > kono > Proof > category

changeset 898:d1bd473b4efb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Apr 2020 16:16:16 +0900
parents 5a074b2c7a46
children e20853d2c6b0
files CCCGraph.agda
diffstat 1 files changed, 43 insertions(+), 37 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Mon Apr 27 23:11:12 2020 +0900
+++ b/CCCGraph.agda	Tue Apr 28 16:16:16 2020 +0900
@@ -319,57 +319,61 @@
   field
    vmap : vertex x → vertex y
    emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
+   econg : {a b : vertex x} → { f g : edge x a b } →  Graph._≅_ x f g  → Graph._≅_ y (emap f) (emap g)
 
 open GMap
 
 -- open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong )
 
 data [_]_==_ {c₁ c₂ ℓ} (C : Graph {c₁} {c₂} {ℓ}) {A B : vertex C} (f : edge C A B)
-     : ∀{X Y : vertex C} → edge C X Y → Set (suc (c₁ ⊔ c₂ )) where
-  mrefl : {g : edge C A B} → (eqv : f ≡ g ) → [ C ] f == g
+     : ∀{X Y : vertex C} → edge C X Y → Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
+  mrefl : {g : edge C A B} → (eqv : Graph._≅_ C f g ) → [ C ] f == g
 
 _=m=_ : ∀ {c₁ c₂ ℓ} {C D : Graph {c₁} {c₂} {ℓ}} 
-    → (F G : GMap C D) → Set (suc (c₂ ⊔ c₁))
+    → (F G : GMap C D) → Set (suc (c₂ ⊔ c₁ ⊔ ℓ))
 _=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f
 
 _&_ :  {v v' ℓ : Level} {x y z : Graph {v} {v'} {ℓ}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z
-f & g = record { vmap = λ x →  vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) }
+f & g = record { vmap = λ x →  vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) ; econg = λ eq → econg f ( econg g eq) }
 
-Grph : {v v' ℓ : Level} → Category (suc (v ⊔ v' ⊔ ℓ )) (suc (v ⊔ v' ⊔ ℓ)) (suc ( v ⊔ v' ))
+erefl : {v v' ℓ : Level}  (C : Graph {v} {v'} {ℓ}) → { x y : vertex C } → {f : edge C x y }  → Graph._≅_ C f f
+erefl C = IsEquivalence.refl (Graph.isEq C)
+
+Grph : {v v' ℓ : Level} → Category (suc (v ⊔ v' ⊔ ℓ )) (suc (v ⊔ v' ⊔ ℓ)) (suc ( v ⊔ v' ⊔ ℓ))
 Grph {v} {v'} {ℓ} = record {
     Obj = Graph {v} {v'} {ℓ}
   ; Hom = GMap {v} {v'}
   ; _o_ = _&_
   ; _≈_ = _=m=_
-  ; Id  = record { vmap = λ y → y ; emap = λ f → f }
+  ; Id  = record { vmap = λ y → y ; emap = λ f → f ; econg = λ eq → eq }
   ; isCategory = record {
-       isEquivalence = λ {A} {B} →  ise 
-     ; identityL = λ e → mrefl refl
-     ; identityR =  λ e → mrefl refl
-     ; o-resp-≈ = m--resp-≈ 
-     ; associative = λ e → mrefl refl
+       isEquivalence = λ {A} {B} →  ise
+     ; identityL = λ {a} {b} {f} e → mrefl ( erefl b )
+     ; identityR =  λ {a} {b} {f} e → mrefl ( erefl b)
+     ; o-resp-≈ = λ {a} {b} {c} {f} {g} {h} {i} f=g h=i  → m--resp-≈ {a} {b} {c} {f} {g} {h} {i} f=g h=i
+     ; associative = λ {a} {b} {c} {d} {f} {g} {h} e → mrefl (erefl d ) 
    }}  where
-       msym : {v v' : Level} {x y : Graph {v} {v'} {ℓ}}  { f g : GMap x y } → f =m= g → g =m= f
-       msym {_} {_} {x} {y} f=g f = lemma ( f=g f ) where
+       msym :  {x y : Graph {v} {v'} {ℓ}}  { f g : GMap x y } → f =m= g → g =m= f
+       msym  {x} {y} f=g f = lemma ( f=g f ) where
             lemma  : ∀{a b c d} {f : edge y a b} {g : edge y c d} → [ y ] f == g → [ y ] g == f
-            lemma (mrefl Ff≈Gf) = mrefl  (sym  Ff≈Gf)
-       mtrans : {v v' : Level} {x y : Graph {v} {v'} {ℓ}}  { f g h : GMap x y } → f =m= g → g =m= h → f =m= h
-       mtrans {_} {_} {x} {y} f=g g=h f = lemma ( f=g f ) ( g=h f ) where
+            lemma (mrefl Ff≈Gf) = mrefl  (IsEquivalence.sym (Graph.isEq y) Ff≈Gf) 
+       mtrans : {x y : Graph {v} {v'} {ℓ}}  { f g h : GMap x y } → f =m= g → g =m= h → f =m= h
+       mtrans  {x} {y} f=g g=h f = lemma ( f=g f ) ( g=h f ) where
            lemma : ∀{a b c d e f} {p : edge y a b} {q : edge y c d} → {r : edge y e f}  → [ y ] p == q → [ y ] q == r → [ y ] p == r
-           lemma (mrefl eqv) (mrefl eqv₁) = mrefl ( trans eqv  eqv₁ )
-       ise : {v v' : Level} {x y : Graph {v} {v'}}  → IsEquivalence {_} {suc v ⊔ suc v' } {_} ( _=m=_  {v} {v'}  {ℓ} {x} {y}) 
-       ise  = record {
-          refl =  λ f → mrefl refl
-        ; sym = msym
-        ; trans = {!!} -- mtrans
+           lemma (mrefl eqv) (mrefl eqv₁) = mrefl ( (IsEquivalence.trans (Graph.isEq y)) eqv  eqv₁ )
+       ise :  {x y : Graph {v} {v'} {ℓ}}  → IsEquivalence {_} {suc v ⊔ suc v' ⊔ suc ℓ} {_} ( _=m=_  {v} {v'}  {ℓ} {x} {y}) 
+       ise  {x} {y} = record {
+          refl =  λ {C} f → mrefl (erefl y ) 
+        ; sym = λ {x} {y} eq → msym  {_} {_} {x} {y} eq
+        ; trans = λ {x} {y} {z} eq → mtrans {_} {_} {x} {y} {z} eq
           }
-       m--resp-≈ : {v v' ℓ : Level} {A B C : Graph {v} {v'}{ℓ} }  
+       m--resp-≈ :  {A B C : Graph {v} {v'}{ℓ} }  
            {f g : GMap A B} {h i : GMap B C} → f =m= g → h =m= i → ( h & f ) =m= ( i & g )
-       m--resp-≈ {_} {_} {_} {A} {B} {C} {f} {g} {h} {i} f=g h=i e =
+       m--resp-≈ {A} {B} {C} {f} {g} {h} {i} f=g h=i e =
           lemma (emap f e) (emap g e) (emap i (emap g e)) (f=g e) (h=i ( emap g e )) where
             lemma : {a b c d : vertex B } {z w : vertex C } (ϕ : edge B a b) (ψ : edge B c d) (π : edge C z w) →
                 [ B ] ϕ  == ψ → [ C ] (emap h ψ) == π → [ C ] (emap h ϕ) == π
-            lemma _ _ _ (mrefl refl) (mrefl refl) = mrefl refl
+            lemma  ϕ ψ π (mrefl f=g ) (mrefl h=i ) = mrefl ( (IsEquivalence.trans (Graph.isEq C)) (econg h f=g ) h=i ) 
 
 ------------------------------------------------------
 --- CCC → Grph  Forgetful functor
@@ -390,27 +394,29 @@
           ∎  )
   
 fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} )  → Obj (Grph {c₁} {c₂}{ℓ})
-fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) }
+fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) ; _≅_ = Category._≈_ (cat a) ; isEq = IsCategory.isEquivalence (Category.isCategory (cat a)) }
 fmap : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grph {c₁} {c₂}) ( fobj a ) ( fobj b )
-fmap f =  record { vmap = FObj (cmap f) ; emap = FMap (cmap f) }
+fmap f =  record { vmap = FObj (cmap f) ; emap = FMap (cmap f) ; econg = IsFunctor.≈-cong (Functor.isFunctor (cmap f))  }
 
 UX : {c₁ c₂ ℓ : Level} → ( ≈-to-≡ : (A : Category c₁ c₂ ℓ ) →  {a b : Obj A} → {f g : Hom A a b} → A [ f ≈ g ] → f ≡ g  )
-    → Functor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂})
+    → Functor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂} {ℓ} )
 FObj (UX {c₁} {c₂} {ℓ} ≈-to-≡  ) a = fobj a
 FMap (UX ≈-to-≡)  f =  fmap f
 isFunctor (UX {c₁} {c₂} {ℓ}  ≈-to-≡)  = isf where
   -- if we don't need ≈-cong ( i.e.   f ≈ g → UX f =m= UX g ), all lemmas are not necessary
   open import HomReasoning
   isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂}) fobj fmap
-  IsFunctor.identity isf {a} {b} {f} e = mrefl refl 
-  IsFunctor.distr isf f = mrefl refl
-  IsFunctor.≈-cong isf {a} {b} {f} {g} eq {x} {y} e = lemma (extensionality Sets ( λ z → lemma4 (
-               ≃-cong (cat b) (eq (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g)))
-          ))) (eq e) where
-      lemma4 : {x y : vertex (fobj b) } →  [_]_~_ (cat b)  (id1 (cat b) x) (id1 (cat b) y) → x ≡ y
-      lemma4 (refl eqv) = refl 
-      lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ fobj b ] emap (fmap f) e == emap (fmap g) e
-      lemma refl (refl eqv) = mrefl ( ≈-to-≡ (cat b) eqv )
+  IsFunctor.identity isf {a} {b} {f} e = mrefl (erefl (fobj a))
+  IsFunctor.distr isf {a} {b} {c} f = mrefl (erefl (fobj c))
+  IsFunctor.≈-cong isf {a} {b} {f} {g} eq {x} {y} e = {!!} where --  [ fobj b ] emap (fmap f) e == emap (fmap g) e
+        lemma = econg (fmap f) {!!}
+    --   lemma (extensionality Sets ( λ z → lemma4 (
+    --           ≃-cong (cat b) (eq (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g)))
+    --      ))) (eq e) where
+    --  lemma4 : {x y : vertex (fobj b) } →  [_]_~_ (cat b)  (id1 (cat b) x) (id1 (cat b) y) → x ≡ y
+    --  lemma4 (refl eqv) = refl 
+    --  lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ fobj b ] emap (fmap f) e == emap (fmap g) e
+    --  lemma refl (refl eqv) = mrefl {!!} -- (econg (fmap f ) ? ) -- ( ≈-to-≡ (cat b) eqv )