Mercurial > hg > Members > kono > Proof > category
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 １ ( 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 @@ -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