Mercurial > hg > Members > kono > Proof > category

changeset 927:2c5ae3015a05

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
level hell
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 10 May 2020 16:36:42 +0900
parents a7332c329b57
children c1222aa20244
files CCCGraph.agda README.txt
diffstat 2 files changed, 56 insertions(+), 46 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Tue May 05 08:23:54 2020 +0900
+++ b/CCCGraph.agda	Sun May 10 16:36:42 2020 +0900
@@ -1,6 +1,6 @@
 open import Level
 open import Category 
-module CCCgraph where
+module CCCgraph  where
 
 open import HomReasoning
 open import cat-utility
@@ -265,7 +265,7 @@
 open import graph
 open Graph
 
-record GMap {v v' : Level} (x y : Graph {v} {v'} )  : Set (v ⊔ v' ) where
+record GMap {c₁ c₂ : Level} (x y : Graph {c₁} {c₂} )  : Set (c₁ ⊔ c₂ ) where
   field
    vmap : vertex x → vertex y
    emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
@@ -282,13 +282,13 @@
     → (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
+_&_ :  {c₁ c₂ : Level} {x y z : Graph {c₁} {c₂}} ( 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 ) }
 
-Grph : {v v' : Level} → Category (suc (v ⊔ v')) (v ⊔ v') (suc ( v ⊔ v'))
-Grph {v} {v'} = record {
-    Obj = Graph {v} {v'}
-  ; Hom = GMap {v} {v'}
+Grph : {c₁ c₂ : Level} → Category (suc (c₁ ⊔ c₂)) (c₁ ⊔ c₂) (suc ( c₁ ⊔ c₂))
+Grph {c₁} {c₂} = record {
+    Obj = Graph {c₁} {c₂}
+  ; Hom = GMap {c₁} {c₂}
   ; _o_ = _&_
   ; _≈_ = _=m=_
   ; Id  = record { vmap = λ y → y ; emap = λ f → f }
@@ -299,21 +299,21 @@
      ; o-resp-≈ = m--resp-≈ 
      ; associative = λ e → mrefl refl
    }}  where
-       msym : {v v' : Level} {x y : Graph {v} {v'} }  { f g : GMap x y } → f =m= g → g =m= f
+       msym : {c₁ c₂ : Level} {x y : Graph {c₁} {c₂} }  { 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 : {c₁ c₂ : Level} {x y : Graph {c₁} {c₂} }  { 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 : {c₁ c₂ : Level} {x y : Graph {c₁} {c₂}}  → IsEquivalence {_} {suc c₁ ⊔ suc c₂ } {_} ( _=m=_  {c₁} {c₂}  {x} {y}) 
        ise  = record {
           refl =  λ f → mrefl refl
         ; sym = msym
         ; trans = mtrans
           }
-       m--resp-≈ : {v v' : Level} {A B C : Graph {v} {v'} }  
+       m--resp-≈ : {c₁ c₂ : Level} {A B C : Graph {c₁} {c₂} }  
            {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 =
           lemma (emap f e) (emap g e) (emap i (emap g e)) (f=g e) (h=i ( emap g e )) where
@@ -323,11 +323,13 @@
 
 --- Forgetful functor
 
-≃-cong : {c₁ c₂ ℓ : Level}  (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B }
+module forgetful  {c₁ c₂ : Level} where
+
+  ≃-cong : {c₁ c₂ ℓ : Level}  (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B }
       → { f f'   : Hom B a b }
       → { g g' : Hom B a' b' }
       → [_]_~_ B f g → B [ f ≈ f' ] → B [ g ≈ g' ] → [_]_~_ B f' g'
-≃-cong B {a} {b} {a'} {b'} {f} {f'} {g} {g'}  (refl {g2} eqv) f=f' g=g' = let open ≈-Reasoning B in refl {_} {_} {_} {B} {a'} {b'} {f'} {g'} ( begin
+  ≃-cong B {a} {b} {a'} {b'} {f} {f'} {g} {g'}  (refl {g2} eqv) f=f' g=g' = let open ≈-Reasoning B in refl {_} {_} {_} {B} {a'} {b'} {f'} {g'} ( begin
              f'
           ≈↑⟨ f=f' ⟩
              f
@@ -337,25 +339,25 @@
              g'
           ∎  )
   
-fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} )  → Obj (Grph {c₁} {c₂})
-fobj a = record { vertex = Obj (cat a) ; edge = Hom (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) }
+  fobj : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂} )  → Obj (Grph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂})
+  fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) }
+  fmap :  {a b : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) } → Hom (Cart ) a b → Hom (Grph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂}) ( fobj a ) ( fobj b )
+  fmap f =  record { vmap = FObj (cmap f) ; emap = FMap (cmap f) }
 
-UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂}  )
-FObj UX a = fobj a
-FMap UX f =  fmap f
-isFunctor UX  = isf where
-  isf : IsFunctor Cart Grph fobj fmap
-  IsFunctor.identity isf {a} {b} {f} e = mrefl refl
-  IsFunctor.distr isf {a} {b} {c} f = mrefl refl
-  IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = lemma ( (extensionality Sets ( λ z → lemma4 (
-               ≃-cong (cat b) (f=g (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g)))
-          )))) (f=g 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 (≡←≈ b eqv)
+  UX :  Functor (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (Grph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂}  )
+  FObj UX a = fobj a
+  FMap UX f =  fmap f
+  isFunctor UX  = isf where
+    isf : IsFunctor Cart Grph fobj fmap
+    IsFunctor.identity isf {a} {b} {f} e = mrefl refl
+    IsFunctor.distr isf {a} {b} {c} f = mrefl refl
+    IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = lemma ( (extensionality Sets ( λ z → lemma4 (
+                 ≃-cong (cat b) (f=g (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g)))
+            )))) (f=g 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 (≡←≈ b eqv)
 
 
 open ccc-from-graph.Objs
@@ -363,38 +365,39 @@
 open ccc-from-graph.Arrows
 open graphtocat.Chain
 
-ccc-graph-univ :  {c₁ : Level } → UniversalMapping (Grph {suc c₁} {c₁}  ) (Cart {suc c₁} {c₁} {c₁} ) UX
-ccc-graph-univ {c₁}   = record {
-     F = λ g → csc g ;
-     η = λ a → record { vmap = λ y → {!!} ; emap = λ f x y →  next f (x y) } ;
-     _* = {!!} ;
+ccc-graph-univ :  {c₁ c₂ : Level } → UniversalMapping (Grph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)}) (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (forgetful.UX {c₁} {c₂} )
+ccc-graph-univ {c₁} {c₂}  = record {
+     F = λ g → csc {!!} ;
+     η = λ a → record { vmap = λ y →  cobj {!!} {!!}; emap = λ f x y →  next f (x y) } ;
+     _* = solution ;
      isUniversalMapping = record {
          universalMapping = {!!} ;
          uniquness = {!!}
       }
   } where
+       open forgetful  {c₁} {c₂}
        open ccc-from-graph
-       csc : Graph {suc c₁} {c₁} → Obj (Cart {suc c₁} {c₁} {c₁})
-       csc g = record { cat = Sets {c₁}  ; ccc = sets {c₁}; ≡←≈ = λ eq → eq } 
-       cs : (g : Graph {c₁} {c₁}) → Functor  (ccc-from-graph.PL g) (Sets {c₁})
+       csc : Graph {c₁} {c₂} → Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂})
+       csc  g = record { cat = Sets {c₁ ⊔ c₂}  ; ccc = sets {c₁ ⊔ c₂} ; ≡←≈ = λ eq → eq } 
+       cs :  (g : Graph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)}) → Functor  (ccc-from-graph.PL g) (Sets {suc (c₁ ⊔ c₂)})
        cs g = CS g
-       pl : (g : Graph {c₁} {c₁} ) → Category  c₁  c₁  c₁
+       pl :  (g : Graph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)} ) → Category _ _ _
        pl g = PL g
-       cobj  : {g : Obj Grph} {c : Obj (Cart {c₁} {c₁} {c₁})} → Hom Grph g (FObj UX c)  → Objs g → Obj (cat c)
+       cobj  :   {g : Obj (Grph   {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)})} {c : Obj (Cart)} → Hom Grph g (FObj UX c)  → Objs g → Obj (cat c)
        cobj {g} {c} f (atom x) = vmap f x
        cobj {g} {c} f ⊤ = CCC.１ (ccc c)
        cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) (cobj {g} {c} f x) (cobj {g} {c} f y)
        cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a) 
-       c-map : {g : Obj Grph} {c : Obj (Cart {c₁} {c₁} {c₁})} {A B : Objs g}
+       c-map :  {g : Obj (Grph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)} )} {c : Obj Cart} {A B : Objs g}
            → (f : Hom Grph g (FObj UX c) ) → (p : Hom (pl g) A B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B)
        c-map {g} {c} {atom a} {atom x} f y = {!!}
-       c-map {g} {c} {⊤} {atom x} f y = {!!}
-       c-map {g} {c} {a ∧ b} {atom x} f y = {!!}
+       c-map {g} {c} {⊤} {atom x} f (iv f1 y) = {!!}
+       c-map {g} {c} {a ∧ b} {atom x} f (iv f1 y) = {!!}
        c-map {g} {c} {b <= a} {atom x} f y = {!!}
        c-map {g} {c} {a} {⊤} f x = CCC.○ (ccc c) (cobj f a)
        c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f {!!}) (c-map f {!!})
        c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f {!!})
-       solution : {g : Obj (Grph {c₁} {c₁})} {c : Obj (Cart {c₁} {c₁} {c₁})} → Hom Grph g (FObj UX c) → Hom (Cart  {suc c₁} {c₁} {c₁}) {!!} {!!}
-       solution {g} {c} f = record { cmap = record { FObj = λ x → {!!} ; FMap = {!!} ; isFunctor = {!!} } ; ccf = {!!} }
+       solution : {g : Obj (Grph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)})} {c : Obj (Cart )} → Hom Grph g (FObj UX c) → Hom (Cart ) {!!} {!!}
+       solution  {g} {c} f = {!!} -- record { cmap = record { FObj = λ x → {!!} ; FMap = {!!} ; isFunctor = {!!} } ; ccf = {!!} }
 
 
--- a/README.txt	Tue May 05 08:23:54 2020 +0900
+++ b/README.txt	Sun May 10 16:36:42 2020 +0900
@@ -61,6 +61,13 @@
     applicative.agda              -- Applicative functor is a monoidal functor
     monad→monoidal.agda
 
+-- Cartesian Closed Category
+
+    deductive.agda                -- deduction theorem
+    CCC.agda
+    CCChom.agda
+    CCCGraph.agda                 -- CCC generated from graph
+
 -- no yet finished
 
 -- repositories