Members/kono/Proof/category: CCChom.agda comparison

comparison CCChom.agda @ 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

comparison

equal deleted inserted replaced

-:e4986625ddd7
+:bb9fd483f560
 nat-2 : {a b c  : Obj A} → {f : Hom A (b * c) (b * c) } → {g : Hom A a (b * c) }
 → (A × A) [ (A × A) [ IsoS.≅→ ccc-2 f o (g , g) ] ≈  IsoS.≅→ ccc-2 ( A [ f o g ] ) ]
 nat-3 : {a b c : Obj A} → { k : Hom A c (a ^ b ) } → A [ A [  IsoS.≅→ (ccc-3) (id1 A (a ^ b)) o
 (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
 record CCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
 < ( g o π )  o < ( f o π ) , π' > , π'  o < ( f o π ) , π' > >
 ≈↑⟨ IsCCC.distr-π isc ⟩
 < ( 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
 ;    ε  = ε'
 ;    _*'  = solution
 ≈⟨ IsCCC.e4b isc  ⟩
 g
 ∎ where open ≈-Reasoning A
+----------
+--- Hom A １ ( 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 １ ( 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.１ 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
 ;   ≅← =  λ f → CCC._* ccc ( A [ f o  CCC.π' ccc  ] )                                  --- ┌ f ┐   name of (f : b ^a → 1 )
 ;   iso→  = iso→
 ∎ where open ≈-Reasoning A
 *-cong  : {a b c : Obj A} {f f' : Hom A (a ∧ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ]
 *-cong eq = cong← ( ccc-3 (isCCChom h )) eq
 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
 OneObj' : One'   -- () in Haskell ( or any one object set )
 amap {G} {a} {.(_ <= _)} (f *) x = λ y → amap f ( x , y )
 fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
 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
 isFunctor (CS G) = isf where
 _++_ = 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
+distr {a} {b} {c} {f} {next {b} {d} {c} x g} z = adistr (distr {a} {b} {d} {f} {g} z ) x where
-fmap (next < x , y > g ++ f) z
+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 )
-amap x (fmap (g ++ f) z) , amap y (fmap (g ++ f) z)
+adistr eq x = cong ( λ k → amap x k ) eq
-≡⟨  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} {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
 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z )

Mercurial > hg > Members > kono > Proof > category

comparison CCChom.agda @ 815:bb9fd483f560