changeset 815:bb9fd483f560

simpler proof of CCC from graph
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 27 Apr 2019 12:17:49 +0900
parents e4986625ddd7
children 4e48b331020a
files CCChom.agda
diffstat 1 files changed, 27 insertions(+), 81 deletions(-) [+]
line wrap: on
line diff
--- a/CCChom.agda	Sat Apr 27 10:10:40 2019 +0900
+++ b/CCChom.agda	Sat Apr 27 12:17:49 2019 +0900
@@ -62,6 +62,15 @@
                     (IsoS.≅← (ccc-2 ) (A [ k o (proj₁ ( IsoS.≅→ ccc-2  (id1 A (c *  b)))) ] ,
                         (proj₂ ( IsoS.≅→ ccc-2  (id1 A (c *  b) ))))) ] ≈ IsoS.≅→ (ccc-3 ) k ]
 
+--------
+--  CCC satisfies   hom natural iso
+--
+--   ccc-1 : Hom A a 1 ≅ {*}
+--   ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b )
+--   ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c
+--
+--------
+
 open import CCC
 
         
@@ -239,6 +248,10 @@
                  < ( g o π ) , π' > o < ( f o π ) , π' > 
              ∎ where open ≈-Reasoning A
 
+-------
+--- U_b and F_b is an adjunction Functor
+-------
+
 CCCtoAdj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (  ccc : CCC A ) → (b : Obj A ) → coUniversalMapping A A (F_b A ccc b)
 CCCtoAdj  A ccc b = record {
         U  = λ a → a <= b 
@@ -279,9 +292,11 @@
              ∎ where open ≈-Reasoning A
 
 
-
+----------
+--- Hom A 1 ( c ^ b ) ≅ Hom A b c
+----------
 
-c^b=b<=c : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( ccc : CCC A ) → {a b c : Obj A} →  -- Hom A 1 ( c ^ b ) ≅ Hom A b c
+c^b=b<=c : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( ccc : CCC A ) → {a b c : Obj A} →  
                           IsoS A A  (CCC.1 ccc ) (CCC._<=_ ccc  c b) b c
 c^b=b<=c A ccc {a} {b} {c} = record {
            ≅→ = λ f → A [ CCC.ε ccc o  CCC.<_,_> ccc ( A [ f o CCC.○ ccc b ] ) ( id1 A b )  ] ---   g ’   (g : 1 → b ^ a) of
@@ -511,6 +526,8 @@
 
 open import Category.Sets
 
+-- Sets is a CCC
+
 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
 data One' {l : Level}  : Set l where
@@ -643,6 +660,10 @@
    fmap {G} {a} {a} (id a) = λ z → z
    fmap {G} {a} {b} (next x f ) = Sets [ amap {G} x o fmap f ]
 
+   --   CS is a map from Positive logic to Sets
+   --    Sets is CCC, so we have a cartesian closed category generated by a graph
+   --       as a sub category of Sets
+
    CS : (G : SM ) → Functor (DX G) (Sets {Level.zero})
    FObj (CS G) a  = fobj a
    FMap (CS G) {a} {b} f = fmap {G} {a} {b} f
@@ -650,86 +671,11 @@
        _++_ = Category._o_ (DX G)
        ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) )
        distr : {a b c : Obj (DX G)}  { f : Hom (DX G) a b } { g : Hom (DX G) b c } → (z : fobj {G} a ) → fmap (g ++ f) z ≡ fmap g (fmap f z)
-       distr {a} {b} {e ∧ e1} {f} {next {b} {d} {e ∧ e1} < x , y > g} z = begin
-            fmap (next < x , y > g ++ f) z
-          ≡⟨⟩
-             amap x (fmap (g ++ f) z) , amap y (fmap (g ++ f) z)
-          ≡⟨  cong ( λ k → ( amap x k , amap y k )) (distr {a} {b} {d} {f} {g} z) ⟩
-             amap x (fmap g (fmap f z)) , amap y (fmap g (fmap f z))
-          ≡⟨⟩
-            fmap (next < x , y > g) (fmap f z)
-          ∎  where open ≡-Reasoning
-       distr {a} {b} {c <= d} {f} {next {b} {e} {c <= d} (x *) g} z = begin
-             fmap (next (x *) g ++ f) z
-          ≡⟨⟩
-             (λ y → amap x (fmap (g ++ f) z , y) )
-          ≡⟨  extensionality Sets ( λ y →  cong ( λ k →  (amap x (k , y )) ) (distr {a} {b} {e} {f} {g} z) ) ⟩
-             (λ y → amap x (fmap g (fmap f z) , y))
-          ≡⟨⟩
-             fmap (next (x *) g) (fmap f z)
-          ∎  where open ≡-Reasoning
-       distr {a} {b} {c} {f} {next {.b} {.c ∧ x} {.c} π g} z =  begin
-             fmap (DX G [ next π g o f ]) z
-          ≡⟨⟩
-             fmap {G} {a} {c} (next {PL G} {a} {c ∧ x} {c} π ( g ++ f)) z
-          ≡⟨⟩
-             proj₁ ( fmap {G} {a} {c ∧ x} (g ++ f ) z ) 
-          ≡⟨ cong ( λ k → proj₁ k ) ( distr {a} {b} {(c ∧ x)} {f} {g} z )  ⟩
-             proj₁ ( fmap g ( fmap f z ))
-          ≡⟨⟩
-             (Sets [ fmap (next π g) o fmap f ]) z
-          ∎  where open ≡-Reasoning 
-       distr {a} {b} {c} {f} {next {b} {x ∧ c} π' g} z =   begin
-             fmap (DX G [ next π' g o f ]) z
-          ≡⟨⟩
-             fmap (next π' (g ++ f)) z
-          ≡⟨⟩
-             proj₂ (fmap (g ++ f) z)
-          ≡⟨ cong ( λ k → proj₂ k ) ( distr {a} {b} {x ∧ c} {f} {g}  z )  ⟩
-             ( Sets [ fmap (next π' g) o fmap f ] ) z
-          ∎  where open ≡-Reasoning 
-       distr {a} {b} {c} {f} {next {b} {(c <= x) ∧ x} {c} ε g} z =  begin
-             fmap (DX G [ next ε g o f ] ) z
-          ≡⟨⟩
-              fmap (next ε (g ++ f)) z
-          ≡⟨⟩
-             proj₁ (fmap (g ++ f)  z) (  proj₂ (fmap (g ++ f) z) ) 
-          ≡⟨  cong ( λ k → proj₁ k (  proj₂ k)) (distr {a} {b} {(c <= x) ∧ x} {f} {g} z)   ⟩
-             proj₁ (fmap g (fmap f z)) ( proj₂ (fmap g (fmap f z)))
-          ≡⟨⟩
-             fmap (next ε g) (fmap f z) 
-          ≡⟨⟩
-             ( Sets [ fmap (next ε g) o fmap f ] ) z
-          ∎  where open ≡-Reasoning 
-       distr {a} {.a} {.a} {id a} {id .a} z =  refl
-       distr {a} {.a} {c} {id a} {next {a} {b} x g} z = begin
-             fmap (DX G [ next x g o Chain.id a ]) z
-          ≡⟨⟩
-             fmap ( next x ( g ++ (Chain.id a))) z
-          ≡⟨ cong ( λ k → fmap ( next x k ) z ) ( ++idR {a} {b} {g} ) ⟩
-             fmap ( next x  g ) z
-          ≡⟨ refl ⟩
-             ( Sets [ fmap (next x g) o fmap (Chain.id a) ] ) z
-          ∎  where open ≡-Reasoning 
+       distr {a} {b} {c} {f} {next {b} {d} {c} x g} z = adistr (distr {a} {b} {d} {f} {g} z ) x where
+          adistr : fmap (g ++ f) z ≡ fmap g (fmap f z) →
+              ( x : Arrow (graph G) d c ) → fmap ( next x (g ++ f) ) z  ≡ fmap ( next x g ) (fmap f z )
+          adistr eq x = cong ( λ k → amap x k ) eq
        distr {a} {b} {b} {f} {id b} z =  refl
-       distr {a} {b} {atom z} {f} {next {.b} {atom y} {atom z} (arrow x) g} w =  begin
-             fmap (DX G [ next (arrow x) g o f ]) w
-          ≡⟨⟩
-             fmap ( next (arrow x) (g ++ f ) ) w
-          ≡⟨⟩
-             smap G x ( fmap (g ++ f) w )   
-          ≡⟨ cong ( λ k → smap G x k ) (distr {a} {b} {atom y} {f} {g} w) ⟩
-             smap G x (fmap g (fmap f w))
-          ≡⟨⟩
-             fmap (next (arrow x) g) ( fmap f w )
-          ≡⟨⟩
-             (Sets [ fmap (next (arrow x) g) o fmap f ]) w
-          ∎  where open ≡-Reasoning 
-       distr {a} {b} {.⊤} {f} {next (○ a₁) g} z = begin
-             fmap (DX G [ next (○ a₁) g o f ]) z
-          ≡⟨⟩
-             (Sets [ fmap (next (○ a₁) g) o fmap f ]) z
-          ∎  where open ≡-Reasoning 
        isf : IsFunctor (DX G) Sets fobj fmap 
        IsFunctor.identity isf = extensionality Sets ( λ x → refl )
        IsFunctor.≈-cong isf refl = refl