# HG changeset patch # User Shinji KONO # Date 1589448488 -32400 # Node ID cce9e539486ec04dcad2966d29dadce108557ecf # Parent e702aa8be9dd1b558ec9c10c0be572d2380dc012 workaround on forget functor level diff -r e702aa8be9dd -r cce9e539486e CCCGraph.agda --- a/CCCGraph.agda Thu May 14 10:48:52 2020 +0900 +++ b/CCCGraph.agda Thu May 14 18:28:08 2020 +0900 @@ -222,32 +222,6 @@ IsFunctor.≈-cong isf refl = refl IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) - pccc : CCC PL -- this does not work because of ≡ , if we define another equality, o-resp-≈ may trouble - pccc = record { - １ = ⊤ - ; ○ = λ _ → ○ _ - ; _∧_ = _∧_ - ; <_,_> = λ f g → < f , g > - ; π = iv π (id _) - ; π' = iv π' (id _) - ; _<=_ = _<=_ - ; _* = λ f → iv (f *) (id _) - ; ε = iv ε (id _) - ; isCCC = isCCC - } where - open graphtocat.Chain - isCCC : CCC.IsCCC PL ⊤ ○ _∧_ <_,_> (iv π (id _)) (iv π' (id _)) _<=_ (λ f → iv (f *) (id _)) (iv ε (id _)) - isCCC = record { - e2 = {!!} --e2 - ; e3a = {!!} --λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g} - ; e3b = {!!} --λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g} - ; e3c = {!!} --e3c - ; π-cong = {!!} --π-cong - ; e4a = {!!} --e4a - ; e4b = {!!} --e4b - ; *-cong = {!!} --*-cong - } - --- --- SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap --- @@ -313,7 +287,7 @@ → (F G : GMap C D) → Set (c₁ ⊔ c₂ ⊔ 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 -_&_ : {c₁ c₂ : Level} {x y z : Graph {c₁} {c₂} } ( f : GMap y z ) ( g : GMap x y ) → GMap x z +_&_ : {c₁ c₂ c₁' c₂' c₁'' c₂'' : Level} {x : Graph {c₁} {c₂}} {y : Graph {c₁'} {c₂'}} {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 : {c₁ c₂ : Level} → Category (suc (c₁ ⊔ c₂)) (c₁ ⊔ c₂) (c₁ ⊔ c₂) @@ -354,7 +328,7 @@ --- Forgetful functor -module forgetful where +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 } @@ -369,26 +343,40 @@ ≈⟨ g=g' ⟩ g' ∎ ) - - fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ}) → Obj Grph - fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) } - fmap : {c₁ c₂ ℓ : Level} {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart ) a b → Hom (Grph ) ( fobj a ) ( fobj b ) - fmap f = record { vmap = FObj (cmap f) ; emap = FMap (cmap f) } - UX : {c₁ c₂ : Level} → Functor (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (Grph {c₁} {c₂}) - FObj UX a = {!!} -- fobj a - FMap UX f = {!!} -- fmap f - isFunctor UX = {!!} where -- 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 + -- 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₁ ⊔ c₂} → Graph {c₁} {c₂} + m21 : (g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} ) → GMap {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁} {c₂} g (g21 g) + m12 : (g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} ) → GMap {c₁} {c₂} {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} (g21 g) g + giso→ : { g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} } + → {a b : vertex g } → {e : edge g a b } → (m12 g & m21 g) =m= id1 Grph g + giso← : { g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} } + → {a b : vertex (g21 g) } → {e : edge (g21 g) a b } → (m21 g & m12 g ) =m= id1 Grph (g21 g) + -- Grph [ Grph [ m21 g o m12 g ] ≈ id1 Grph (g21 g) ] + + fobj : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) → Obj Grph + 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 {c₁} {c₂}) (g21 ( fobj a )) (g21 ( fobj b )) + fmap {a} {b} f = record { + vmap = λ e → vmap (m21 (fobj b)) (FObj (cmap f) (vmap (m12 (fobj a)) e )) + ; emap = λ e → emap (m21 (fobj b)) (FMap (cmap f) (emap (m12 (fobj a)) e )) } + + UX : Functor (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (Grph {c₁} {c₂}) + FObj UX a = g21 (fobj a) + FMap UX f = fmap f + isFunctor UX = isf where + isf : IsFunctor Cart Grph (λ z → g21 (fobj z)) fmap + IsFunctor.identity isf {a} {b} {f} e = {!!} + IsFunctor.distr isf {a} {b} {c} f = {!!} + IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = {!!} where -- 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) + -- lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ g21 (fobj b)] emap (fmap f) {!!} == emap (fmap g) {!!} + -- lemma = {!!} -- refl (refl eqv) = mrefl (≡←≈ b eqv) open ccc-from-graph.Objs @@ -416,7 +404,7 @@ FO : (a : Obj (Grph {c₁} {c₂}) ) → Graph {(c₁ ⊔ c₂)} {(c₁ ⊔ c₂)} FO a = FObj UX (F a) η : (a : Obj (Grph {c₁} {c₂}) ) → Hom Grph a (FObj UX (F a)) - η a = record { vmap = λ y → {!!} ; emap = λ f x → {!!} } + η a = record { vmap = λ y → {!!} ; emap = λ f → {!!} } csc : Graph → Obj Cart csc g = record { cat = Sets {c₁ ⊔ c₂} ; ccc = sets ; ≡←≈ = λ eq → eq } cs : {c₁ c₂ : Level} → (g : Graph {c₁} {c₂} ) → Functor (ccc-from-graph.PL g) (Sets {_})