Mercurial > hg > Members > kono > Proof > category
changeset 991:e7848ad0c6f9
remove suc level in CCCGraph
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 06 Mar 2021 11:42:01 +0900 |
| parents | ac4db33b466f |
| children | c1576827404e |
| files | src/CCCGraph.agda src/yoneda.agda |
| diffstat | 2 files changed, 65 insertions(+), 70 deletions(-) [+] |
line wrap: on
line diff
--- a/src/CCCGraph.agda Fri Mar 05 22:49:03 2021 +0900 +++ b/src/CCCGraph.agda Sat Mar 06 11:42:01 2021 +0900 @@ -115,15 +115,19 @@ open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) open Graph - data Objs : Set (suc c₁) where - atom : (vertex G) → Objs + V = vertex G + E : V → V → Set c₂ + E = edge G + + data Objs : Set c₁ where + atom : V → Objs ⊤ : Objs - _∧_ : Objs → Objs → Objs + _∧_ : Objs → Objs → Objs _<=_ : Objs → Objs → Objs - data Arrows : (b c : Objs ) → Set (suc c₁ ⊔ c₂) - data Arrow : Objs → Objs → Set (suc c₁ ⊔ c₂) where --- case i - arrow : {a b : vertex G} → (edge G) a b → Arrow (atom a) (atom b) + data Arrows : (b c : Objs ) → Set (c₁ ⊔ c₂) + data Arrow : Objs → Objs → Set (c₁ ⊔ c₂) where --- case i + arrow : {a b : V} → E a b → Arrow (atom a) (atom b) π : {a b : Objs } → Arrow ( a ∧ b ) a π' : {a b : Objs } → Arrow ( a ∧ b ) b ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a @@ -159,7 +163,7 @@ assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h ) -- positive intutionistic calculus - PL : Category (suc c₁) (suc c₁ ⊔ c₂) (suc c₁ ⊔ c₂) + PL : Category c₁ (c₁ ⊔ c₂) (c₁ ⊔ c₂) PL = record { Obj = Objs; Hom = λ a b → Arrows a b ; @@ -353,9 +357,9 @@ --- Forgetful functor -module forgetful {c₁ c₂ : Level} where +module forgetful {c₁ : Level} where - ≃-cong : {c₁ c₂ ℓ : Level} (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B } + ≃-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' @@ -370,53 +374,36 @@ ∎ ) -- Grph does not allow morph on different level graphs - -- simply assumes we have iso to the another level. This may means same axiom on CCCs results the same CCCs. - postulate - g21 : Graph {suc c₁} {c₁ ⊔ c₂} → Graph {c₁} {c₂} - m21 : (g : Graph {suc c₁ } {c₁ ⊔ c₂} ) → GMap {suc c₁ } {c₁ ⊔ c₂} {c₁} {c₂} g (g21 g) - m12 : (g : Graph {suc c₁ } {c₁ ⊔ c₂} ) → GMap {c₁} {c₂} {suc c₁ } {c₁ ⊔ c₂} (g21 g) g - giso→ : { g : Graph {suc c₁ } {c₁ ⊔ c₂} } - → {a b : vertex g } → (m12 g & m21 g) =m= id1 Grph g - giso← : { g : Graph {suc c₁ } {c₁ ⊔ c₂} } - → {a b : vertex (g21 g) } → (m21 g & m12 g ) =m= id1 Grph (g21 g) - -- Grph [ Grph [ m21 g o m12 g ] ≈ id1 Grph (g21 g) ] + -- simply assumes c₁ and c₂ has the same - uobj : Obj (Cart {suc c₁ } {c₁ ⊔ c₂} {c₁ ⊔ c₂}) → Obj Grph + uobj : Obj (Cart {c₁ } {c₁} {c₁}) → Obj Grph uobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) } - umap : {a b : Obj (Cart {suc c₁ } {c₁ ⊔ c₂} {c₁ ⊔ c₂} ) } → Hom (Cart ) a b → Hom (Grph {c₁} {c₂}) (g21 ( uobj a )) (g21 ( uobj b )) + umap : {a b : Obj (Cart {c₁ } {c₁} {c₁} ) } → Hom (Cart ) a b → Hom (Grph {c₁} {c₁}) (( uobj a )) (( uobj b )) umap {a} {b} f = record { - vmap = λ e → vmap (m21 (uobj b)) (FObj (cmap f) (vmap (m12 (uobj a)) e )) - ; emap = λ e → emap (m21 (uobj b)) (FMap (cmap f) (emap (m12 (uobj a)) e )) } + vmap = λ e → FObj (cmap f) e + ; emap = λ e → FMap (cmap f) e } - UX : Functor (Cart {suc c₁} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (Grph {c₁} {c₂}) - FObj UX a = g21 (uobj a) + UX : Functor (Cart {c₁} {c₁} {c₁}) (Grph {c₁} {c₁}) + FObj UX a = (uobj a) FMap UX f = umap f isFunctor UX = isf where - isf : IsFunctor Cart Grph (λ z → g21 (uobj z)) umap + isf : IsFunctor Cart Grph (λ z → (uobj z)) umap IsFunctor.identity isf {a} {b} {f} = begin umap (id1 Cart a) ≈⟨⟩ umap {a} {a} (record { cmap = identityFunctor ; ccf = λ x → x }) ≈⟨⟩ - record { vmap = λ e → vmap (m21 (uobj a)) (vmap (m12 (uobj a)) e ) ; emap = λ e → emap (m21 (uobj a)) (emap (m12 (uobj a)) e )} - ≈⟨ giso← {uobj a} {f} {f} ⟩ record { vmap = λ y → y ; emap = λ f → f } ≈⟨⟩ - id1 Grph (g21 (uobj a)) + id1 Grph ((uobj a)) ∎ where open ≈-Reasoning Grph IsFunctor.distr isf {a} {b} {c} {f} {g} = begin umap ( Cart [ g o f ] ) ≈⟨⟩ - ( m21 (uobj c) & ( record { vmap = λ e → FObj (cmap (( Cart [ g o f ] ))) e ; emap = λ e → FMap (cmap (( Cart [ g o f ] ))) e} & m12 (uobj a) ) ) + record { vmap = {!!} ; emap = {!!} } ≈⟨ {!!} ⟩ --- ( m21 (uobj c) & (record { vmap = λ e → FObj (cmap g) (FObj (cmap f) e) ; emap = λ e → FMap (cmap g) (FMap (cmap f) e) } --- & m12 (uobj a))) --- ≈⟨ cdr (cdr (car (giso← {uobj b} ))) ⟩ --- ( m21 (uobj c) & (record { vmap = λ e → FObj (cmap g) e ; emap = λ e → FMap (cmap g) e} --- & ((m12 (uobj b) --- & (m21 (uobj b))) & (record { vmap = λ e → FObj (cmap f) e ; emap = λ e → FMap (cmap f) e} --- & (m12 (uobj a) ))))) --- ≈⟨⟩ + record { vmap = {!!} ; emap = {!!} } + ≈⟨⟩ Grph [ umap g o umap f ] ∎ where open ≈-Reasoning Grph IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = {!!} where -- lemma ( (extensionality Sets ( λ z → lemma4 ( @@ -440,7 +427,7 @@ open ccc-from-graph g - FCat : Obj (Cart {suc c₁} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) + FCat : Obj (Cart {c₁} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) FCat = record { cat = record { Obj = Obj PL ; Hom = λ a b → Hom B (FObj CS a) (FObj CS b) @@ -466,8 +453,8 @@ fcat-eq : {a b : Obj (cat FCat) } → (f : Hom (cat FCat) a b ) → FMap CS (fcat-pl f) ≡ f -ccc-graph-univ : {c₁ c₂ : Level} → UniversalMapping (Grph {c₁} {c₂}) (Cart {suc c₁ } {c₁ ⊔ c₂} {c₁ ⊔ c₂}) forgetful.UX -ccc-graph-univ {c₁} {c₂} = record { +ccc-graph-univ : {c₁ : Level} → UniversalMapping (Grph {c₁} {c₁}) (Cart {c₁ } {c₁} {c₁}) forgetful.UX +ccc-graph-univ {c₁} = record { F = F ; η = η ; _* = solution ; @@ -490,33 +477,33 @@ -- ↓ | -- Sets ((z : vertx g) → C z x) ----> ((z : vertx g) → C z y) = h : Hom Sets (fobj (atom x)) (fobj (atom y)) -- - F : Obj (Grph {c₁} {c₂}) → Obj (Cart {suc c₁} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) + F : Obj (Grph {c₁} {c₁}) → Obj (Cart {c₁} {c₁} {c₁}) F g = FCat where open fcat g - η : (a : Obj (Grph {c₁} {c₂}) ) → Hom Grph a (FObj UX (F a)) - η a = record { vmap = λ y → vm y ; emap = λ f → em f } where - fo : Graph {suc c₁ } {c₁ ⊔ c₂} - fo = uobj {c₁} {c₂} (F a) - vm : (y : vertex a ) → vertex (g21 fo) - vm y = vmap (m21 fo) (atom y) - em : { x y : vertex a } (f : edge a x y ) → edge (FObj UX (F a)) (vm x) (vm y) - em {x} {y} f = emap (m21 fo) (fmap a (iv (arrow f) (id _))) - pl : {c₁ c₂ : Level} → (g : Graph {c₁} {c₂} ) → Category _ _ _ + η : (a : Obj (Grph {c₁} {c₁}) ) → Hom Grph a (FObj UX (F a)) + η a = record { vmap = λ y → {!!} ; emap = λ f → em f } where + fo : Graph {c₁ } {c₁} + fo = uobj {c₁} (F a) + vm : (y : vertex a ) → vertex {!!} + vm y = {!!} -- vmap (m21 fo) (atom y) + em : { x y : vertex a } (f : edge a x y ) → edge (FObj UX (F a)) {!!} {!!} + em {x} {y} f = {!!} -- emap (m21 fo) (fmap a (iv (arrow f) (id _))) + pl : {c₁ c₁ : Level} → (g : Graph {c₁} {c₁} ) → Category _ _ _ pl g = PL g - cobj : {g : Obj (Grph {c₁} {c₂} ) } {c : Obj Cart} → Hom Grph g (FObj UX c) → Objs g → Obj (cat c) - cobj {g} {c} f (atom x) = vmap (m12 (uobj {c₁} {c₂} c)) (vmap f x) + cobj : {g : Obj (Grph {c₁} {c₁} ) } {c : Obj Cart} → Hom Grph g (FObj UX c) → Objs g → Obj (cat c) + cobj {g} {c} f (atom x) = vmap {!!} (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} {A B : Objs g} → (f : Hom Grph g (FObj UX c) ) → (fobj g A → fobj g B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B) - c-map {g} {c} {a} {atom b} f y with fcat.fcat-pl {c₁} {c₂} g {a} {atom b} y + c-map {g} {c} {a} {atom b} f y with fcat.fcat-pl {c₁} {c₁} g {a} {atom b} y c-map {g} {c} {atom b} {atom b} f y | id (atom b) = id1 (cat c) _ c-map {g} {c} {a} {atom b} f y | iv {_} {_} {d} (arrow x) t = {!!} - -- (cat c) [ emap (m12 (uobj {c₁} {c₂} c)) ( emap f x) o c-map {g} {c} {a} {d} f (fmap g t) ] + -- (cat c) [ emap (m12 (uobj {c₁} {c₁} c)) ( emap f x) o c-map {g} {c} {a} {d} f (fmap g t) ] c-map {g} {c} {a} {atom b} f y | iv {_} {_} {d} π t = {!!} --(cat c) [ CCC.π (ccc c) o c-map {g} {c} {a} {d} f (fmap g t)] c-map {g} {c} {a} {atom b} f y | iv {_} {_} {d} π' t = {!!} -- (cat c) [ CCC.π' (ccc c) o c-map {g} {c} {a} {d} f (fmap g t) ] c-map {g} {c} {a} {atom b} f y | iv {_} {_} {d} ε t = {!!} -- (cat c) [ CCC.ε (ccc c) o c-map {g} {c} {a} {d} f (fmap g t) ] - -- with emap (m12 (uobj {c₁} {c₂} c)) ( emap f {!!} ) + -- with emap (m12 (uobj {c₁} {c₁} c)) ( emap f {!!} ) 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 (λ k → proj₁ (z k))) (c-map f (λ k → proj₂ (z k))) c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f (λ k → x (proj₁ k) (proj₂ k)))
--- a/src/yoneda.agda Fri Mar 05 22:49:03 2021 +0900 +++ b/src/yoneda.agda Sat Mar 06 11:42:01 2021 +0900 @@ -294,6 +294,10 @@ domF : (y : Obj SetsAop) → {x : Obj (Category.op A)} → FObj y x → Obj A domF y {x} z = x +-- +-- f onto +-- + YondaLemma2 : {a a' b : Obj A } (f : Hom A a a' ) → NTrans (Category.op A) Sets (FObj YonedaFunctor a) (FObj YonedaFunctor a') YondaLemma2 f = FMap YonedaFunctor f @@ -303,6 +307,10 @@ -- YondaLemma4 : {a a' b : Obj A } → (f : Hom A a a' ) → Hom ? (id1 A b) f -- YondaLemma4 {a} {a'} {b} f = Hom A b a → Hom A b a' +-- +-- f ∈ FMap (FObj YonedaFunctor a') a +-- + _^ : {a a' b : Obj A } → (f : Hom A a a' ) → Hom A b a → Hom A b a' _^ {a} {a'} {b} f g = (FMap (FObj YonedaFunctor a') g) f @@ -324,10 +332,12 @@ Yoneda-injective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop y (FObj YonedaFunctor a)) (f : Hom A a b ) → SetsAop [ SetsAop [ FMap YonedaFunctor f o g ] ≈ SetsAop [ FMap YonedaFunctor f o h ] ] → SetsAop [ g ≈ h ] -Yoneda-injective {a} {b} {x} {y} g h f yg=yh = extensionality A (λ z → begin - TMap g _ z ≡⟨ eqHom1 (cong (λ k → k z ) yg=yh ) ⟩ - TMap h _ z ∎ ) where - open ≡-Reasoning +Yoneda-injective {a} {b} {x} {y} g h f yg=yh = extensionality A (λ z → ≈-≡ ( begin + TMap g _ z ≈⟨ {!!} ⟩ + A [ id1 A _ o TMap g _ z ] ≈⟨ {!!} ⟩ + ( Sets [ id1 Sets _ o TMap g _ ] ) z ≈⟨ {!!} ⟩ + TMap h _ z ∎ ) ) where + open ≈-Reasoning A ylem11 : {x : Obj A} (z : FObj y x) → A [ f o TMap g _ z ] ≡ A [ f o TMap h _ z ] ylem11 z = (cong (λ k → k z ) yg=yh ) @@ -335,18 +345,16 @@ Yoneda-surjective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop (FObj YonedaFunctor b) y) (f : Hom A a b ) → SetsAop [ SetsAop [ g o FMap YonedaFunctor f ] ≈ SetsAop [ h o FMap YonedaFunctor f ] ] → SetsAop [ g ≈ h ] -Yoneda-surjective {a} {b} {x} {y} g h f yg=yh = extensionality A (λ z → begin - TMap g _ z ≡⟨ {!!} ⟩ - ( Sets [ Sets [ FMap y {!!} o FMap y f ] o TMap g _ ] ) (id1 A _) ≡⟨ {!!} ⟩ - ( Sets [ FMap y {!!} o Sets [ FMap y f o TMap g _ ] ] ) (id1 A _) ≡⟨ {!!} ⟩ - ( Sets [ FMap y {!!} o Sets [ TMap g _ o FMap (FObj YonedaFunctor _) f ] ] ) (id1 A _) ≡⟨ {!!} ⟩ - ( Sets [ FMap y {!!} o Sets [ TMap h _ o FMap (FObj YonedaFunctor _) f ] ] ) (id1 A _) ≡⟨ {!!} ⟩ +Yoneda-surjective {a} {b} {x} {y} g h f yg=yh = extensionality A (λ z → ( begin + TMap g _ z ≡⟨ {!!} ⟩ + TMap g _ (A [ id1 A _ o z ] ) ≡⟨⟩ + ( Sets [ TMap g _ o FMap (FObj YonedaFunctor b) z ]) (id1 A _) ≡⟨ {!!} ⟩ + TMap g _ (A [ f o A [ {!!} o z ] ] ) ≡⟨ {!!} ⟩ ( Sets [ FMap y z o TMap g _ ] ) (id1 A _) ≡⟨ {!!} ⟩ - ( Sets [ TMap g _ o FMap (FObj YonedaFunctor _) z ]) (id1 A _) ≡⟨ {!!} ⟩ - TMap h _ z ∎ ) where + TMap h _ z ∎ ) ) where open ≡-Reasoning - ylem12 : {y : Obj A} → TMap g y f ≡ TMap h y f - ylem12 = yg=yh + ylem12 : {y : Obj A} → { z : Hom A y a } → TMap g y (A [ f o z ]) ≡ TMap h y (A [ f o z ]) + ylem12 {y} {z} = cong (λ k → k z ) (yg=yh {y} ) ylem10 : {y : Obj A} → (λ z → TMap g y (A [ f o z ])) ≡ (λ z → TMap h y (A [ f o z ] )) ylem10 = yg=yh